Theorem ip0i 8484

Description: A slight variant of Equation 6.46 of [Ponnusamy] p. 362, where J is either 1 or -1 to represent +-1.

Hypotheses

Ref	Expression
ip1i.1	|- X = (Base` U)
ip1i.2	|- G = (+v` U)
ip1i.4	|- S = (.s` U)
ip1i.7	|- P = (.i` U)
ip1i.9	|- U e. CPreHil
ip1i.a	|- A e. X
ip1i.b	|- B e. X
ip1i.c	|- C e. X
ip1i.6	|- N = (norm` U)
ip0i.j	|- J e. CC

Assertion

Ref	Expression
ip0i	|- ((((N` ((AGB)G(JSC)))^2) - ((N` ((AGB)G(-uJSC)))^2)) + (((N` ((AG(-u1SB))G(JSC)))^2) - ((N` ((AG(-u1SB))G(-uJSC)))^2))) = (2 x. (((N` (AG(JSC)))^2) - ((N` (AG(-uJSC)))^2)))

Proof of Theorem ip0i

Step	Hyp	Ref	Expression
1		2cn 5980	. . . 4 |- 2 e. CC
2		ip1i.1	. . . . . . 7 |- X = (Base` U)
3		ip1i.6	. . . . . . 7 |- N = (norm` U)
4		ip1i.9	. . . . . . . 8 |- U e. CPreHil
5	4	phnvi 8475	. . . . . . 7 |- U e. NrmCVec
6		ip1i.a	. . . . . . . 8 |- A e. X
7		ip0i.j	. . . . . . . . 9 |- J e. CC
8		ip1i.c	. . . . . . . . 9 |- C e. X
9		ip1i.4	. . . . . . . . . 10 |- S = (.s` U)
10	2, 9	nvscl 8247	. . . . . . . . 9 |- ((U e. NrmCVec /\ J e. CC /\ C e. X) -> (JSC) e. X)
11	5, 7, 8, 10	mp3an 916	. . . . . . . 8 |- (JSC) e. X
12		ip1i.2	. . . . . . . . 9 |- G = (+v` U)
13	2, 12	nvgcl 8239	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ (JSC) e. X) -> (AG(JSC)) e. X)
14	5, 6, 11, 13	mp3an 916	. . . . . . 7 |- (AG(JSC)) e. X
15	2, 3, 5, 14	nvcli 8288	. . . . . 6 |- (N` (AG(JSC))) e. RR
16	15	recn 5314	. . . . 5 |- (N` (AG(JSC))) e. CC
17	16	sqcl 6615	. . . 4 |- ((N` (AG(JSC)))^2) e. CC
18	7	negcl 5369	. . . . . . . . 9 |- -uJ e. CC
19	2, 9	nvscl 8247	. . . . . . . . 9 |- ((U e. NrmCVec /\ -uJ e. CC /\ C e. X) -> (-uJSC) e. X)
20	5, 18, 8, 19	mp3an 916	. . . . . . . 8 |- (-uJSC) e. X
21	2, 12	nvgcl 8239	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ (-uJSC) e. X) -> (AG(-uJSC)) e. X)
22	5, 6, 20, 21	mp3an 916	. . . . . . 7 |- (AG(-uJSC)) e. X
23	2, 3, 5, 22	nvcli 8288	. . . . . 6 |- (N` (AG(-uJSC))) e. RR
24	23	recn 5314	. . . . 5 |- (N` (AG(-uJSC))) e. CC
25	24	sqcl 6615	. . . 4 |- ((N` (AG(-uJSC)))^2) e. CC
26	1, 17, 25	subdi 5429	. . 3 |- (2 x. (((N` (AG(JSC)))^2) - ((N` (AG(-uJSC)))^2))) = ((2 x. ((N` (AG(JSC)))^2)) - (2 x. ((N` (AG(-uJSC)))^2)))
27	1, 17	mulcl 5321	. . . 4 |- (2 x. ((N` (AG(JSC)))^2)) e. CC
28	1, 25	mulcl 5321	. . . 4 |- (2 x. ((N` (AG(-uJSC)))^2)) e. CC
29		ip1i.b	. . . . . . . 8 |- B e. X
30	2, 3, 5, 29	nvcli 8288	. . . . . . 7 |- (N` B) e. RR
31	30	recn 5314	. . . . . 6 |- (N` B) e. CC
32	31	sqcl 6615	. . . . 5 |- ((N` B)^2) e. CC
33	1, 32	mulcl 5321	. . . 4 |- (2 x. ((N` B)^2)) e. CC
34		pnpcan2t 5479	. . . 4 |- (((2 x. ((N` (AG(JSC)))^2)) e. CC /\ (2 x. ((N` (AG(-uJSC)))^2)) e. CC /\ (2 x. ((N` B)^2)) e. CC) -> (((2 x. ((N` (AG(JSC)))^2)) + (2 x. ((N` B)^2))) - ((2 x. ((N` (AG(-uJSC)))^2)) + (2 x. ((N` B)^2)))) = ((2 x. ((N` (AG(JSC)))^2)) - (2 x. ((N` (AG(-uJSC)))^2))))
35	27, 28, 33, 34	mp3an 916	. . 3 |- (((2 x. ((N` (AG(JSC)))^2)) + (2 x. ((N` B)^2))) - ((2 x. ((N` (AG(-uJSC)))^2)) + (2 x. ((N` B)^2)))) = ((2 x. ((N` (AG(JSC)))^2)) - (2 x. ((N` (AG(-uJSC)))^2)))
36	26, 35	eqtr4 1498	. 2 |- (2 x. (((N` (AG(JSC)))^2) - ((N` (AG(-uJSC)))^2))) = (((2 x. ((N` (AG(JSC)))^2)) + (2 x. ((N` B)^2))) - ((2 x. ((N` (AG(-uJSC)))^2)) + (2 x. ((N` B)^2))))
37		eqid 1475	. . . . . . . . . . 11 |- (1st` U) = (1st` U)
38	37	nvvc 8234	. . . . . . . . . 10 |- (U e. NrmCVec -> (1st` U) e. CVec)
39	5, 38	ax-mp 7	. . . . . . . . 9 |- (1st` U) e. CVec
40	12	vafval 8222	. . . . . . . . . 10 |- G = (1st` (1st` U))
41	40	vcabl 8176	. . . . . . . . 9 |- ((1st` U) e. CVec -> G e. Abel)
42	39, 41	ax-mp 7	. . . . . . . 8 |- G e. Abel
43	6, 29, 11	3pm3.2i 818	. . . . . . . 8 |- (A e. X /\ B e. X /\ (JSC) e. X)
44	2, 12	bafval 8223	. . . . . . . . 9 |- X = ran G
45	44	abl23 8104	. . . . . . . 8 |- ((G e. Abel /\ (A e. X /\ B e. X /\ (JSC) e. X)) -> ((AGB)G(JSC)) = ((AG(JSC))GB))
46	42, 43, 45	mp2an 697	. . . . . . 7 |- ((AGB)G(JSC)) = ((AG(JSC))GB)
47	46	fveq2i 3727	. . . . . 6 |- (N` ((AGB)G(JSC))) = (N` ((AG(JSC))GB))
48	47	opreq1i 3971	. . . . 5 |- ((N` ((AGB)G(JSC)))^2) = ((N` ((AG(JSC))GB))^2)
49		ax1cn 5269	. . . . . . . . . . 11 |- 1 e. CC
50	49	negcl 5369	. . . . . . . . . 10 |- -u1 e. CC
51	2, 9	nvscl 8247	. . . . . . . . . 10 |- ((U e. NrmCVec /\ -u1 e. CC /\ B e. X) -> (-u1SB) e. X)
52	5, 50, 29, 51	mp3an 916	. . . . . . . . 9 |- (-u1SB) e. X
53	6, 52, 11	3pm3.2i 818	. . . . . . . 8 |- (A e. X /\ (-u1SB) e. X /\ (JSC) e. X)
54	44	abl23 8104	. . . . . . . 8 |- ((G e. Abel /\ (A e. X /\ (-u1SB) e. X /\ (JSC) e. X)) -> ((AG(-u1SB))G(JSC)) = ((AG(JSC))G(-u1SB)))
55	42, 53, 54	mp2an 697	. . . . . . 7 |- ((AG(-u1SB))G(JSC)) = ((AG(JSC))G(-u1SB))
56	55	fveq2i 3727	. . . . . 6 |- (N` ((AG(-u1SB))G(JSC))) = (N` ((AG(JSC))G(-u1SB)))
57	56	opreq1i 3971	. . . . 5 |- ((N` ((AG(-u1SB))G(JSC)))^2) = ((N` ((AG(JSC))G(-u1SB)))^2)
58	48, 57	opreq12i 3973	. . . 4 |- (((N` ((AGB)G(JSC)))^2) + ((N` ((AG(-u1SB))G(JSC)))^2)) = (((N` ((AG(JSC))GB))^2) + ((N` ((AG(JSC))G(-u1SB)))^2))
59	2, 12, 9, 3	phpar 8483	. . . . 5 |- ((U e. CPreHil /\ (AG(JSC)) e. X /\ B e. X) -> (((N` ((AG(JSC))GB))^2) + ((N` ((AG(JSC))G(-u1SB)))^2)) = (2 x. (((N` (AG(JSC)))^2) + ((N` B)^2))))
60	4, 14, 29, 59	mp3an 916	. . . 4 |- (((N` ((AG(JSC))GB))^2) + ((N` ((AG(JSC))G(-u1SB)))^2)) = (2 x. (((N` (AG(JSC)))^2) + ((N` B)^2)))
61	1, 17, 32	adddi 5326	. . . 4 |- (2 x. (((N` (AG(JSC)))^2) + ((N` B)^2))) = ((2 x. ((N` (AG(JSC)))^2)) + (2 x. ((N` B)^2)))
62	58, 60, 61	3eqtr 1499	. . 3 |- (