Theorem phpar 8483

Description: The parallelogram law for an inner product space.

Hypotheses

Ref	Expression
phpar.1	|- X = (Base` U)
phpar.2	|- G = (+v` U)
phpar.4	|- S = (.s` U)
phpar.6	|- N = (norm` U)

Assertion

Ref	Expression
phpar	|- ((U e. CPreHil /\ A e. X /\ B e. X) -> (((N` (AGB))^2) + ((N` (AG(-u1SB)))^2)) = (2 x. (((N` A)^2) + ((N` B)^2))))

Proof of Theorem phpar

Step	Hyp	Ref	Expression
1		phpar.1	. . . . . . 7 |- X = (Base` U)
2		phpar.2	. . . . . . 7 |- G = (+v` U)
3	1, 2	bafval 8223	. . . . . 6 |- X = ran G
4	3	isphg 8476	. . . . 5 |- ((G e. V /\ S e. V /\ N e. V) -> (<.<.G, S>., N>. e. CPreHil <-> (<.<.G, S>., N>. e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
5	4	pm3.27bda 421	. . . 4 |- (((G e. V /\ S e. V /\ N e. V) /\ <.<.G, S>., N>. e. CPreHil) -> A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))
6	2	vafval 8222	. . . . . . 7 |- G = (1st` (1st` U))
7		fvex 3732	. . . . . . 7 |- (1st` (1st` U)) e. V
8	6, 7	eqeltr 1544	. . . . . 6 |- G e. V
9		phpar.4	. . . . . . . 8 |- S = (.s` U)
10	9	smfval 8224	. . . . . . 7 |- S = (2nd` (1st` U))
11		fvex 3732	. . . . . . 7 |- (2nd` (1st` U)) e. V
12	10, 11	eqeltr 1544	. . . . . 6 |- S e. V
13		phpar.6	. . . . . . . 8 |- N = (norm` U)
14	13	nmfval 8226	. . . . . . 7 |- N = (2nd` U)
15		fvex 3732	. . . . . . 7 |- (2nd` U) e. V
16	14, 15	eqeltr 1544	. . . . . 6 |- N e. V
17	8, 12, 16	3pm3.2i 818	. . . . 5 |- (G e. V /\ S e. V /\ N e. V)
18	17	a1i 8	. . . 4 |- (U e. CPreHil -> (G e. V /\ S e. V /\ N e. V))
19	2, 9, 13	phop 8477	. . . . . 6 |- (U e. CPreHil -> U = <.<.G, S>., N>.)
20	19	eleq1d 1540	. . . . 5 |- (U e. CPreHil -> (U e. CPreHil <-> <.<.G, S>., N>. e. CPreHil))
21	20	ibi 592	. . . 4 |- (U e. CPreHil -> <.<.G, S>., N>. e. CPreHil)
22	5, 18, 21	sylanc 471	. . 3 |- (U e. CPreHil -> A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))
23	22	3ad2ant1 800	. 2 |- ((U e. CPreHil /\ A e. X /\ B e. X) -> A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))
24		opreq1 3968	. . . . . . . 8 |- (x = A -> (xGy) = (AGy))
25	24	fveq2d 3728	. . . . . . 7 |- (x = A -> (N` (xGy)) = (N` (AGy)))
26	25	opreq1d 3975	. . . . . 6 |- (x = A -> ((N` (xGy))^2) = ((N` (AGy))^2))
27		opreq1 3968	. . . . . . . 8 |- (x = A -> (xG(-u1Sy)) = (AG(-u1Sy)))
28	27	fveq2d 3728	. . . . . . 7 |- (x = A -> (N` (xG(-u1Sy))) = (N` (AG(-u1Sy))))
29	28	opreq1d 3975	. . . . . 6 |- (x = A -> ((N` (xG(-u1Sy)))^2) = ((N` (AG(-u1Sy)))^2))
30	26, 29	opreq12d 3978	. . . . 5 |- (x = A -> (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (((N` (AGy))^2) + ((N` (AG(-u1Sy)))^2)))
31		fveq2 3724	. . . . . . . 8 |- (x = A -> (N` x) = (N` A))
32	31	opreq1d 3975	. . . . . . 7 |- (x = A -> ((N` x)^2) = ((N` A)^2))
33	32	opreq1d 3975	. . . . . 6 |- (x = A -> (((N` x)^2) + ((N` y)^2)) = (((N` A)^2) + ((N` y)^2)))
34	33	opreq2d 3976	. . . . 5 |- (x = A -> (2 x. (((N` x)^2) + ((N` y)^2))) = (2 x. (((N` A)^2) + ((N` y)^2))))
35	30, 34	eqeq12d 1489	. . . 4 |- (x = A -> ((((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))) <-> (((N` (AGy))^2) + ((N` (AG(-u1Sy)))^2)) = (2 x. (((N` A)^2) + ((N` y)^2)))))
36		opreq2 3969	. . . . . . . 8 |- (y = B -> (AGy) = (AGB))
37	36	fveq2d 3728	. . . . . . 7 |- (y = B -> (N` (AGy)) = (N` (AGB)))
38	37	opreq1d 3975	. . . . . 6 |- (y = B -> ((N` (AGy))^2) = ((N` (AGB))^2))
39		opreq2 3969	. . . . . . . . 9 |- (y = B -> (-u1Sy) = (-u1SB))
40	39	opreq2d 3976	. . . . . . . 8 |- (y = B -> (AG(-u1Sy)) = (AG(-u1SB)))
41	40	fveq2d 3728	. . . . . . 7 |- (y = B -> (N` (AG(-u1Sy))) = (N` (AG(-u1SB))))
42	41	opreq1d 3975	. . . . . 6 |- (y = B -> ((N` (AG(-u1Sy)))^2) = ((N` (AG(-u1SB)))^2))
43	38, 42	opreq12d 3978	. . . . 5 |- (y = B -> (((N` (AGy))^2) + ((N` (AG(-u1Sy)))^2)) = (((N` (AGB))^2) + ((N` (AG(-u1SB)))^2)))
44		fveq2 3724	. . . . . . . 8 |- (y = B -> (N` y) = (N` B))
45	44	opreq1d 3975	. . . . . . 7 |- (y = B -> ((N` y)^2) = ((N` B)^2))
46	45	opreq2d 3976	. . . . . 6 |- (y = B -> (((N` A)^2) + ((N` y)^2)) = (((N` A)^2) + ((N` B)^2)))
47	46	opreq2d 3976	. . . . 5 |- (y = B -> (2 x. (((N` A)^2) + ((N` y)^2))) = (2 x. (((N` A)^2) + ((N` B)^2))))
48	43, 47	eqeq12d 1489	. . . 4 |- (y = B -> ((((N` (AGy))^2) + ((N` (AG(-u1Sy)))^2)) = (2 x. (((N` A)^2) + ((N` y)^2))) <-> (((N` (AGB))^2) + ((N` (AG(-u1SB)))^2)) = (2 x. (((N` A)^2) + ((N` B)^2)))))
49	35, 48	rcla42v 1880	. . 3 |- ((A e. X /\ B e. X) -> (A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))) -> (((N` (AGB))^2) + ((N` (AG(-u1SB)))^2)) = (2 x. (((N` A)^2) + ((N` B)^2)))))
50	49	3adant1 797	. 2 |- ((U e. CPreHil /\ A e. X /\ B e. X) -> (A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))) -> (((N` (AGB))^2) + ((N` (AG(-u1SB)))^2)) = (2 x. (((N` A)^2) + ((N` B)^2)))))
51	23, 50	mpd 26	1 |- ((U e. CPreHil /\