HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 4ipval3 8309
Description: Four times the inner product value ipval3 8306, useful for simplifying certain proofs.
Hypotheses
Ref Expression
ipfval.1 |- X = (Base` U)
ipfval.2 |- G = (+v` U)
ipfval.4 |- S = (.s` U)
ipfval.6 |- N = (norm` U)
ipfval.7 |- P = (.i` U)
ipval3.3 |- M = (-v` U)
Assertion
Ref Expression
4ipval3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (4 x. (APB)) = ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))))
Proof of Theorem 4ipval3
StepHypRef Expression
1 ipfval.1 . . . 4 |- X = (Base` U)
2 ipfval.2 . . . 4 |- G = (+v` U)
3 ipfval.4 . . . 4 |- S = (.s` U)
4 ipfval.6 . . . 4 |- N = (norm` U)
5 ipfval.7 . . . 4 |- P = (.i` U)
6 ipval3.3 . . . 4 |- M = (-v` U)
71, 2, 3, 4, 5, 6ipval3 8306 . . 3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) = (((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) / 4))
87opreq2d 3967 . 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (4 x. (APB)) = (4 x. (((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) / 4)))
9 axaddcl 5251 . . . 4 |- (((((N` (AGB))^2) - ((N` (AMB))^2)) e. CC /\ (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2))) e. CC) -> ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) e. CC)
10 subclt 5347 . . . . 5 |- ((((N` (AGB))^2) e. CC /\ ((N` (AMB))^2) e. CC) -> (((N` (AGB))^2) - ((N` (AMB))^2)) e. CC)
111, 2, 3, 4, 5ipval2lem3 8302 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AGB))^2) e. RR)
1211recnd 5295 . . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AGB))^2) e. CC)
131, 2, 3, 4, 5, 6ipval2lem6 8308 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AMB))^2) e. RR)
1413recnd 5295 . . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AMB))^2) e. CC)
1510, 12, 14sylanc 471 . . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((N` (AGB))^2) - ((N` (AMB))^2)) e. CC)
16 subclt 5347 . . . . . 6 |- ((((N` (AG(iSB)))^2) e. CC /\ ((N` (AM(iSB)))^2) e. CC) -> (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)) e. CC)
17 axicn 5250 . . . . . . . 8 |- i e. CC
181, 2, 3, 4, 5ipval2lem2 8301 . . . . . . . 8 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ i e. CC) -> ((N` (AG(iSB)))^2) e. RR)
1917, 18mpan2 695 . . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(iSB)))^2) e. RR)
2019recnd 5295 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(iSB)))^2) e. CC)
211, 2, 3, 4, 5, 6ipval2lem5 8307 . . . . . . . 8 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ i e. CC) -> ((N` (AM(iSB)))^2) e. RR)
2217, 21mpan2 695 . . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AM(iSB)))^2) e. RR)
2322recnd 5295 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AM(iSB)))^2) e. CC)
2416, 20, 23sylanc 471 . . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)) e. CC)
25 axmulcl 5253 . . . . . 6 |- ((i e. CC /\ (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)) e. CC) -> (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2))) e. CC)
2617, 25mpan 694 . . . . 5 |- ((((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)) e. CC -> (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2))) e. CC)
2724, 26syl 10 . . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2))) e. CC)
289, 15, 27sylanc 471 . . 3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) e. CC)
29 4re 5937 . . . . 5 |- 4 e. RR
3029recn 5294 . . . 4 |- 4 e. CC
31 4pos 5947 . . . . 5 |- 0 < 4
3229, 31gt0ne0i 5599 . . . 4 |- 4 =/= 0
33 divcan2t 5698 . . . 4 |- ((4 e. CC /\ ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) e. CC /\ 4 =/= 0) -> (4 x. (((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) / 4)) = ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))))
3430, 32, 33mp3an13 905 . . 3 |- (((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) e. CC -> (4 x. (((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) / 4)) = ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))))
3528, 34syl 10 . 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (4 x. (((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))) / 4)) = ((((N` (AGB))^2) - ((N` (AMB))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)))))
368, 35eqtrd 1504 1 |- ((U e. NrmCVec /\