ip1ilem

Description: Lemma for ip1i . (Contributed by NM, 21-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	\|- X = ( BaseSet ` U )
	ip1i.2	\|- G = ( +v ` U )
	ip1i.4	\|- S = ( .sOLD ` U )
	ip1i.7	\|- P = ( .iOLD ` U )
	ip1i.9	\|- U e. CPreHilOLD
	ip1i.a	\|- A e. X
	ip1i.b	\|- B e. X
	ip1i.c	\|- C e. X
	ip1i.6	\|- N = ( normCV ` U )
	ip0i.j	\|- J e. CC
Assertion	ip1ilem	\|- ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) = ( 2 x. ( A P C ) )

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	\|- X = ( BaseSet ` U )
2		ip1i.2	\|- G = ( +v ` U )
3		ip1i.4	\|- S = ( .sOLD ` U )
4		ip1i.7	\|- P = ( .iOLD ` U )
5		ip1i.9	\|- U e. CPreHilOLD
6		ip1i.a	\|- A e. X
7		ip1i.b	\|- B e. X
8		ip1i.c	\|- C e. X
9		ip1i.6	\|- N = ( normCV ` U )
10		ip0i.j	\|- J e. CC
11	5	phnvi	\|- U e. NrmCVec
12	1 2 3 9 4	4ipval2	\|- ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( 4 x. ( A P C ) ) = ( ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
13	11 6 8 12	mp3an	\|- ( 4 x. ( A P C ) ) = ( ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) )
14	13	oveq2i	\|- ( 2 x. ( 4 x. ( A P C ) ) ) = ( 2 x. ( ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
15		2cn	\|- 2 e. CC
16		4cn	\|- 4 e. CC
17	1 4	dipcl	\|- ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( A P C ) e. CC )
18	11 6 8 17	mp3an	\|- ( A P C ) e. CC
19	15 16 18	mul12i	\|- ( 2 x. ( 4 x. ( A P C ) ) ) = ( 4 x. ( 2 x. ( A P C ) ) )
20	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( A G C ) e. X )
21	11 6 8 20	mp3an	\|- ( A G C ) e. X
22	1 9 11 21	nvcli	\|- ( N ` ( A G C ) ) e. RR
23	22	resqcli	\|- ( ( N ` ( A G C ) ) ^ 2 ) e. RR
24	23	recni	\|- ( ( N ` ( A G C ) ) ^ 2 ) e. CC
25		ax-1cn	\|- 1 e. CC
26	25	negcli	\|- -u 1 e. CC
27	1 3	nvscl	\|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ C e. X ) -> ( -u 1 S C ) e. X )
28	11 26 8 27	mp3an	\|- ( -u 1 S C ) e. X
29	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S C ) e. X ) -> ( A G ( -u 1 S C ) ) e. X )
30	11 6 28 29	mp3an	\|- ( A G ( -u 1 S C ) ) e. X
31	1 9 11 30	nvcli	\|- ( N ` ( A G ( -u 1 S C ) ) ) e. RR
32	31	resqcli	\|- ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) e. RR
33	32	recni	\|- ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) e. CC
34	24 33	subcli	\|- ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) e. CC
35		ax-icn	\|- _i e. CC
36	1 3	nvscl	\|- ( ( U e. NrmCVec /\ _i e. CC /\ C e. X ) -> ( _i S C ) e. X )
37	11 35 8 36	mp3an	\|- ( _i S C ) e. X
38	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ A e. X /\ ( _i S C ) e. X ) -> ( A G ( _i S C ) ) e. X )
39	11 6 37 38	mp3an	\|- ( A G ( _i S C ) ) e. X
40	1 9 11 39	nvcli	\|- ( N ` ( A G ( _i S C ) ) ) e. RR
41	40	resqcli	\|- ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) e. RR
42	41	recni	\|- ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) e. CC
43	35	negcli	\|- -u _i e. CC
44	1 3	nvscl	\|- ( ( U e. NrmCVec /\ -u _i e. CC /\ C e. X ) -> ( -u _i S C ) e. X )
45	11 43 8 44	mp3an	\|- ( -u _i S C ) e. X
46	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ A e. X /\ ( -u _i S C ) e. X ) -> ( A G ( -u _i S C ) ) e. X )
47	11 6 45 46	mp3an	\|- ( A G ( -u _i S C ) ) e. X
48	1 9 11 47	nvcli	\|- ( N ` ( A G ( -u _i S C ) ) ) e. RR
49	48	resqcli	\|- ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) e. RR
50	49	recni	\|- ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) e. CC
51	42 50	subcli	\|- ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) e. CC
52	35 51	mulcli	\|- ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) e. CC
53	15 34 52	adddii	\|- ( 2 x. ( ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) ) = ( ( 2 x. ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) ) + ( 2 x. ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
54	1 2 3 4 5 6 7 8 9 25	ip0i	\|- ( ( ( ( N ` ( ( A G B ) G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) )
55	1 3	nvsid	\|- ( ( U e. NrmCVec /\ C e. X ) -> ( 1 S C ) = C )
56	11 8 55	mp2an	\|- ( 1 S C ) = C
57	56	oveq2i	\|- ( ( A G B ) G ( 1 S C ) ) = ( ( A G B ) G C )
58	57	fveq2i	\|- ( N ` ( ( A G B ) G ( 1 S C ) ) ) = ( N ` ( ( A G B ) G C ) )
59	58	oveq1i	\|- ( ( N ` ( ( A G B ) G ( 1 S C ) ) ) ^ 2 ) = ( ( N ` ( ( A G B ) G C ) ) ^ 2 )
60	59	oveq1i	\|- ( ( ( N ` ( ( A G B ) G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) = ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) )
61	56	oveq2i	\|- ( ( A G ( -u 1 S B ) ) G ( 1 S C ) ) = ( ( A G ( -u 1 S B ) ) G C )
62	61	fveq2i	\|- ( N ` ( ( A G ( -u 1 S B ) ) G ( 1 S C ) ) ) = ( N ` ( ( A G ( -u 1 S B ) ) G C ) )
63	62	oveq1i	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( 1 S C ) ) ) ^ 2 ) = ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 )
64	63	oveq1i	\|- ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) = ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) )
65	60 64	oveq12i	\|- ( ( ( ( N ` ( ( A G B ) G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) ) = ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) )
66	56	oveq2i	\|- ( A G ( 1 S C ) ) = ( A G C )
67	66	fveq2i	\|- ( N ` ( A G ( 1 S C ) ) ) = ( N ` ( A G C ) )
68	67	oveq1i	\|- ( ( N ` ( A G ( 1 S C ) ) ) ^ 2 ) = ( ( N ` ( A G C ) ) ^ 2 )
69	68	oveq1i	\|- ( ( ( N ` ( A G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) = ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) )
70	69	oveq2i	\|- ( 2 x. ( ( ( N ` ( A G ( 1 S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) )
71	54 65 70	3eqtr3i	\|- ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) )
72	1 2 3 4 5 6 7 8 9 35	ip0i	\|- ( ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) )
73	72	oveq2i	\|- ( _i x. ( ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) = ( _i x. ( 2 x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) )
74	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
75	11 6 7 74	mp3an	\|- ( A G B ) e. X
76	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G B ) e. X /\ ( _i S C ) e. X ) -> ( ( A G B ) G ( _i S C ) ) e. X )
77	11 75 37 76	mp3an	\|- ( ( A G B ) G ( _i S C ) ) e. X
78	1 9 11 77	nvcli	\|- ( N ` ( ( A G B ) G ( _i S C ) ) ) e. RR
79	78	resqcli	\|- ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) e. RR
80	79	recni	\|- ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) e. CC
81	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G B ) e. X /\ ( -u _i S C ) e. X ) -> ( ( A G B ) G ( -u _i S C ) ) e. X )
82	11 75 45 81	mp3an	\|- ( ( A G B ) G ( -u _i S C ) ) e. X
83	1 9 11 82	nvcli	\|- ( N ` ( ( A G B ) G ( -u _i S C ) ) ) e. RR
84	83	resqcli	\|- ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) e. RR
85	84	recni	\|- ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) e. CC
86	80 85	subcli	\|- ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) e. CC
87	1 3	nvscl	\|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X )
88	11 26 7 87	mp3an	\|- ( -u 1 S B ) e. X
89	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) e. X )
90	11 6 88 89	mp3an	\|- ( A G ( -u 1 S B ) ) e. X
91	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ ( _i S C ) e. X ) -> ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) e. X )
92	11 90 37 91	mp3an	\|- ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) e. X
93	1 9 11 92	nvcli	\|- ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) e. RR
94	93	resqcli	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) e. RR
95	94	recni	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) e. CC
96	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ ( -u _i S C ) e. X ) -> ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) e. X )
97	11 90 45 96	mp3an	\|- ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) e. X
98	1 9 11 97	nvcli	\|- ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) e. RR
99	98	resqcli	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) e. RR
100	99	recni	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) e. CC
101	95 100	subcli	\|- ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) e. CC
102	35 86 101	adddii	\|- ( _i x. ( ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) = ( ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) )
103	35 15 51	mul12i	\|- ( _i x. ( 2 x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) = ( 2 x. ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) )
104	73 102 103	3eqtr3i	\|- ( ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) = ( 2 x. ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) )
105	71 104	oveq12i	\|- ( ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) ) + ( ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) ) = ( ( 2 x. ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) ) + ( 2 x. ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
106	53 105	eqtr4i	\|- ( 2 x. ( ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) ) = ( ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) ) + ( ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
107	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G B ) e. X /\ C e. X ) -> ( ( A G B ) G C ) e. X )
108	11 75 8 107	mp3an	\|- ( ( A G B ) G C ) e. X
109	1 9 11 108	nvcli	\|- ( N ` ( ( A G B ) G C ) ) e. RR
110	109	resqcli	\|- ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) e. RR
111	110	recni	\|- ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) e. CC
112	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G B ) e. X /\ ( -u 1 S C ) e. X ) -> ( ( A G B ) G ( -u 1 S C ) ) e. X )
113	11 75 28 112	mp3an	\|- ( ( A G B ) G ( -u 1 S C ) ) e. X
114	1 9 11 113	nvcli	\|- ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) e. RR
115	114	resqcli	\|- ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) e. RR
116	115	recni	\|- ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) e. CC
117	111 116	subcli	\|- ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) e. CC
118	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ C e. X ) -> ( ( A G ( -u 1 S B ) ) G C ) e. X )
119	11 90 8 118	mp3an	\|- ( ( A G ( -u 1 S B ) ) G C ) e. X
120	1 9 11 119	nvcli	\|- ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) e. RR
121	120	resqcli	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) e. RR
122	121	recni	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) e. CC
123	1 2	nvgcl	\|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ ( -u 1 S C ) e. X ) -> ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) e. X )
124	11 90 28 123	mp3an	\|- ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) e. X
125	1 9 11 124	nvcli	\|- ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) e. RR
126	125	resqcli	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) e. RR
127	126	recni	\|- ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) e. CC
128	122 127	subcli	\|- ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) e. CC
129	35 86	mulcli	\|- ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) e. CC
130	35 101	mulcli	\|- ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) e. CC
131	117 128 129 130	add4i	\|- ( ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) ) + ( ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) ) = ( ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) + ( ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
132	1 4	dipcl	\|- ( ( U e. NrmCVec /\ ( A G B ) e. X /\ C e. X ) -> ( ( A G B ) P C ) e. CC )
133	11 75 8 132	mp3an	\|- ( ( A G B ) P C ) e. CC
134	1 4	dipcl	\|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ C e. X ) -> ( ( A G ( -u 1 S B ) ) P C ) e. CC )
135	11 90 8 134	mp3an	\|- ( ( A G ( -u 1 S B ) ) P C ) e. CC
136	16 133 135	adddii	\|- ( 4 x. ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) ) = ( ( 4 x. ( ( A G B ) P C ) ) + ( 4 x. ( ( A G ( -u 1 S B ) ) P C ) ) )
137	1 2 3 9 4	4ipval2	\|- ( ( U e. NrmCVec /\ ( A G B ) e. X /\ C e. X ) -> ( 4 x. ( ( A G B ) P C ) ) = ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
138	11 75 8 137	mp3an	\|- ( 4 x. ( ( A G B ) P C ) ) = ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) )
139	1 2 3 9 4	4ipval2	\|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ C e. X ) -> ( 4 x. ( ( A G ( -u 1 S B ) ) P C ) ) = ( ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
140	11 90 8 139	mp3an	\|- ( 4 x. ( ( A G ( -u 1 S B ) ) P C ) ) = ( ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) )
141	138 140	oveq12i	\|- ( ( 4 x. ( ( A G B ) P C ) ) + ( 4 x. ( ( A G ( -u 1 S B ) ) P C ) ) ) = ( ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) + ( ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) )
142	136 141	eqtr2i	\|- ( ( ( ( ( N ` ( ( A G B ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G B ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) + ( ( ( ( N ` ( ( A G ( -u 1 S B ) ) G C ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u _i S C ) ) ) ^ 2 ) ) ) ) ) = ( 4 x. ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) )
143	106 131 142	3eqtri	\|- ( 2 x. ( ( ( ( N ` ( A G C ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S C ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S C ) ) ) ^ 2 ) ) ) ) ) = ( 4 x. ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) )
144	14 19 143	3eqtr3ri	\|- ( 4 x. ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) ) = ( 4 x. ( 2 x. ( A P C ) ) )
145	144	oveq1i	\|- ( ( 4 x. ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) ) / 4 ) = ( ( 4 x. ( 2 x. ( A P C ) ) ) / 4 )
146	133 135	addcli	\|- ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) e. CC
147		4ne0	\|- 4 =/= 0
148	146 16 147	divcan3i	\|- ( ( 4 x. ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) ) / 4 ) = ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) )
149	15 18	mulcli	\|- ( 2 x. ( A P C ) ) e. CC
150	149 16 147	divcan3i	\|- ( ( 4 x. ( 2 x. ( A P C ) ) ) / 4 ) = ( 2 x. ( A P C ) )
151	145 148 150	3eqtr3i	\|- ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) = ( 2 x. ( A P C ) )

Metamath Proof Explorer

Theorem ip1ilem

Proof