Theorem ip1ilem 8485

Description: Lemma for ip1i 8486.

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
ip1ilem	|- (((AGB)PC) + ((AG(-u1SB))PC)) = (2 x. (APC))

Proof of Theorem ip1ilem

Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . 7 |- U e. CPreHil
2	1	phnvi 8475	. . . . . 6 |- U e. NrmCVec
3		ip1i.a	. . . . . 6 |- A e. X
4		ip1i.c	. . . . . 6 |- C e. X
5		ip1i.1	. . . . . . 7 |- X = (Base` U)
6		ip1i.2	. . . . . . 7 |- G = (+v` U)
7		ip1i.4	. . . . . . 7 |- S = (.s` U)
8		ip1i.6	. . . . . . 7 |- N = (norm` U)
9		ip1i.7	. . . . . . 7 |- P = (.i` U)
10	5, 6, 7, 8, 9	4ipval2 8358	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ C e. X) -> (4 x. (APC)) = ((((N` (AGC))^2) - ((N` (AG(-u1SC)))^2)) + (i x. (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2)))))
11	2, 3, 4, 10	mp3an 916	. . . . 5 |- (4 x. (APC)) = ((((N` (AGC))^2) - ((N` (AG(-u1SC)))^2)) + (i x. (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2))))
12	11	opreq2i 3972	. . . 4 |- (2 x. (4 x. (APC))) = (2 x. ((((N` (AGC))^2) - ((N` (AG(-u1SC)))^2)) + (i x. (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2)))))
13		2cn 5980	. . . . 5 |- 2 e. CC
14		4re 5982	. . . . . 6 |- 4 e. RR
15	14	recn 5314	. . . . 5 |- 4 e. CC
16	5, 9	ipcl 8365	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ C e. X) -> (APC) e. CC)
17	2, 3, 4, 16	mp3an 916	. . . . 5 |- (APC) e. CC
18	13, 15, 17	mul12 5423	. . . 4 |- (2 x. (4 x. (APC))) = (4 x. (2 x. (APC)))
19	5, 6	nvgcl 8239	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X /\ C e. X) -> (AGC) e. X)
20	2, 3, 4, 19	mp3an 916	. . . . . . . . . . 11 |- (AGC) e. X
21	5, 8, 2, 20	nvcli 8288	. . . . . . . . . 10 |- (N` (AGC)) e. RR
22	21	resqcl 6623	. . . . . . . . 9 |- ((N` (AGC))^2) e. RR
23	22	recn 5314	. . . . . . . 8 |- ((N` (AGC))^2) e. CC
24		ax1cn 5269	. . . . . . . . . . . . . 14 |- 1 e. CC
25	24	negcl 5369	. . . . . . . . . . . . 13 |- -u1 e. CC
26	5, 7	nvscl 8247	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ -u1 e. CC /\ C e. X) -> (-u1SC) e. X)
27	2, 25, 4, 26	mp3an 916	. . . . . . . . . . . 12 |- (-u1SC) e. X
28	5, 6	nvgcl 8239	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X /\ (-u1SC) e. X) -> (AG(-u1SC)) e. X)
29	2, 3, 27, 28	mp3an 916	. . . . . . . . . . 11 |- (AG(-u1SC)) e. X
30	5, 8, 2, 29	nvcli 8288	. . . . . . . . . 10 |- (N` (AG(-u1SC))) e. RR
31	30	resqcl 6623	. . . . . . . . 9 |- ((N` (AG(-u1SC)))^2) e. RR
32	31	recn 5314	. . . . . . . 8 |- ((N` (AG(-u1SC)))^2) e. CC
33	23, 32	subcl 5366	. . . . . . 7 |- (((N` (AGC))^2) - ((N` (AG(-u1SC)))^2)) e. CC
34		axicn 5270	. . . . . . . 8 |- i e. CC
35	5, 7	nvscl 8247	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ i e. CC /\ C e. X) -> (iSC) e. X)
36	2, 34, 4, 35	mp3an 916	. . . . . . . . . . . . 13 |- (iSC) e. X
37	5, 6	nvgcl 8239	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X /\ (iSC) e. X) -> (AG(iSC)) e. X)
38	2, 3, 36, 37	mp3an 916	. . . . . . . . . . . 12 |- (AG(iSC)) e. X
39	5, 8, 2, 38	nvcli 8288	. . . . . . . . . . 11 |- (N` (AG(iSC))) e. RR
40	39	resqcl 6623	. . . . . . . . . 10 |- ((N` (AG(iSC)))^2) e. RR
41	40	recn 5314	. . . . . . . . 9 |- ((N` (AG(iSC)))^2) e. CC
42	34	negcl 5369	. . . . . . . . . . . . . 14 |- -ui e. CC
43	5, 7	nvscl 8247	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ -ui e. CC /\ C e. X) -> (-uiSC) e. X)
44	2, 42, 4, 43	mp3an 916	. . . . . . . . . . . . 13 |- (-uiSC) e. X
45	5, 6	nvgcl 8239	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X /\ (-uiSC) e. X) -> (AG(-uiSC)) e. X)
46	2, 3, 44, 45	mp3an 916	. . . . . . . . . . . 12 |- (AG(-uiSC)) e. X
47	5, 8, 2, 46	nvcli 8288	. . . . . . . . . . 11 |- (N` (AG(-uiSC))) e. RR
48	47	resqcl 6623	. . . . . . . . . 10 |- ((N` (AG(-uiSC)))^2) e. RR
49	48	recn 5314	. . . . . . . . 9 |- ((N` (AG(-uiSC)))^2) e. CC
50	41, 49	subcl 5366	. . . . . . . 8 |- (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2)) e. CC
51	34, 50	mulcl 5321	. . . . . . 7 |- (i x. (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2))) e. CC
52	13, 33, 51	adddi 5326	. . . . . 6 |- (2 x. ((((N` (AGC))^2) - ((N` (AG(-u1SC)))^2)) + (i x. (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2))))) = ((2 x. (((N` (AGC))^2) - ((N` (AG(-u1SC)))^2))) + (2 x. (i x. (((N` (AG(iSC)))^2) - ((N` (AG(-uiSC)))^2)))))
53		ip1i.b	. . . . . . . . 9 |- B e. X
54	5, 6, 7, 9, 1, 3, 53, 4, 8, 24	ip0i 8484	. . . . . . . 8 |- ((((N` ((AGB)G(1SC)))^2) - ((N` ((AGB)G(-u1SC)))^2)) + (((N` ((AG(-u1SB))G(1SC)))^2) - ((N` ((AG(-u1SB))G(-u1SC)))^2))) = (2 x. (((N` (AG(1SC)))^2) - ((N` (AG(-u1SC)))^2)))
55	5, 7	nvsid 8248	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ C e. X) -> (1SC) = C)
56	2, 4, 55	mp2an 697	. . . . . . . . . . . . 13 |- (1SC) = C
57	56	opreq2i 3972	. . . . . . . . . . . 12 |- ((AGB)G(1SC)) = ((AGB)GC)
58	57	fveq2i 3727	. . . . . . . . . . 11 |- (N` ((AGB)G(1SC))) = (N` ((AGB)GC))
59	58	opreq1i 3971	. . . . . . . . . 10 |- ((N` ((AGB)G(1SC)))^2) = ((N` ((AGB)GC))^2)
60	59	opreq1i 3971	. . . . . . . . 9 |- (((N` ((AGB)G(1SC)))^2) - ((N` ((AGB)G(-u1SC)))^2)) = (((N` ((AGB)GC))^2) - ((N` ((AGB)G(-u1SC)))^2))
61	56	opreq2i 3972	. . . . . . . . . . . 12 |- ((AG(-u1SB))G(1SC)) = ((AG(-u1SB))GC)
62	61	fveq2i 3727	. . . . . . . . . . 11 |- (N` ((AG(-u1SB))G(1SC))) = (N` ((AG(-u1SB))GC))
63	62	opreq1i 3971	. . . . . . . . . 10 |- ((N` ((AG(-u1SB))G(1SC)))^2) = ((N` ((AG(-u1SB))GC))^2)
64	63	opreq1i 3971	. . . . . . . . 9 |- (((N` ((AG(-u1SB))G(1SC)))^2) - ((N` ((AG(-u1SB))G(-u1SC)))^2)) = (((N` ((AG(-u1SB))GC))^2) - ((N` ((AG(-u1SB))G(-u1SC)))^2))
65	60, 64	opreq12i 3973	. . . . . . . 8 |- ((((N` ((AGB)G(1SC)))^2) - ((N` ((AGB)G(-u1SC)))^2)) + (((N` ((AG(-u1SB))G(1SC)))^2) - ((N` ((AG(-u1SB))G(-u1SC)))^2))) = ((((N` (