Theorem 4ipval3 8296

Description: Four times the inner product value ipval3 8293, 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

Step	Hyp	Ref	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)
7	1, 2, 3, 4, 5, 6	ipval3 8293	. . 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))
8	7	opreq2d 3961	. 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 5243	. . . 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 5339	. . . . 5 |- ((((N` (AGB))^2) e. CC /\ ((N` (AMB))^2) e. CC) -> (((N` (AGB))^2) - ((N` (AMB))^2)) e. CC)
11	1, 2, 3, 4, 5	ipval2lem3 8289	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AGB))^2) e. RR)
12	11	recnd 5287	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AGB))^2) e. CC)
13	1, 2, 3, 4, 5, 6	ipval2lem6 8295	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AMB))^2) e. RR)
14	13	recnd 5287	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AMB))^2) e. CC)
15	10, 12, 14	sylanc 471	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((N` (AGB))^2) - ((N` (AMB))^2)) e. CC)
16		subclt 5339	. . . . . 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 5242	. . . . . . . 8 |- i e. CC
18	1, 2, 3, 4, 5	ipval2lem2 8288	. . . . . . . 8 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ i e. CC) -> ((N` (AG(iSB)))^2) e. RR)
19	17, 18	mpan2 694	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(iSB)))^2) e. RR)
20	19	recnd 5287	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(iSB)))^2) e. CC)
21	1, 2, 3, 4, 5, 6	ipval2lem5 8294	. . . . . . . 8 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ i e. CC) -> ((N` (AM(iSB)))^2) e. RR)
22	17, 21	mpan2 694	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AM(iSB)))^2) e. RR)
23	22	recnd 5287	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AM(iSB)))^2) e. CC)
24	16, 20, 23	sylanc 471	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)) e. CC)
25		axmulcl 5245	. . . . . 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)
26	17, 25	mpan 693	. . . . 5 |- ((((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2)) e. CC -> (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2))) e. CC)
27	24, 26	syl 10	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (i x. (((N` (AG(iSB)))^2) - ((N` (AM(iSB)))^2))) e. CC)
28	9, 15, 27	sylanc 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 5929	. . . . 5 |- 4 e. RR
30	29	recn 5286	. . . 4 |- 4 e. CC
31		4pos 5939	. . . . 5 |- 0 < 4
32	29, 31	gt0ne0i 5591	. . . 4 |- 4 =/= 0
33		divcan2t 5690	. . . 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)))))
34	30, 32, 33	mp3an13 904	. . 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)))))
35	28, 34	syl 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)))))
36	8, 35	eqtrd 1499	1 |- ((U e. NrmCVec /\