Theorem isph 8481

Description: The predicate "is an inner product space."

Hypotheses

Ref	Expression
isph.1	|- X = (Base` U)
isph.2	|- G = (+v` U)
isph.3	|- M = (-v` U)
isph.6	|- N = (norm` U)

Assertion

Ref	Expression
isph	|- (U e. CPreHil <-> (U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))

Distinct variable groups:   x,y,G   x,M,y   x,N,y   x,U,y   x,X,y

Proof of Theorem isph

Step	Hyp	Ref	Expression
1		phnv 8473	. . 3 |- (U e. CPreHil -> U e. NrmCVec)
2	1	pm4.71ri 638	. 2 |- (U e. CPreHil <-> (U e. NrmCVec /\ U e. CPreHil))
3		isph.2	. . . . . 6 |- G = (+v` U)
4		eqid 1475	. . . . . 6 |- (.s` U) = (.s` U)
5		isph.6	. . . . . 6 |- N = (norm` U)
6	3, 4, 5	nvop 8305	. . . . 5 |- (U e. NrmCVec -> U = <.<.G, (.s` U)>., N>.)
7		eleq1 1534	. . . . . 6 |- (U = <.<.G, (.s` U)>., N>. -> (U e. CPreHil <-> <.<.G, (.s` U)>., N>. e. CPreHil))
8		eleq1 1534	. . . . . . . . 9 |- (U = <.<.G, (.s` U)>., N>. -> (U e. NrmCVec <-> <.<.G, (.s` U)>., N>. e. NrmCVec))
9	8	anbi1d 617	. . . . . . . 8 |- (U = <.<.G, (.s` U)>., N>. -> ((U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))) <-> (<.<.G, (.s` U)>., N>. e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
10		isph.1	. . . . . . . . . . . . . . . . 17 |- X = (Base` U)
11		isph.3	. . . . . . . . . . . . . . . . 17 |- M = (-v` U)
12	10, 3, 4, 11	nvmval 8263	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ x e. X /\ y e. X) -> (xMy) = (xG(-u1(.s` U)y)))
13	12	3expa 833	. . . . . . . . . . . . . . 15 |- (((U e. NrmCVec /\ x e. X) /\ y e. X) -> (xMy) = (xG(-u1(.s` U)y)))
14	13	fveq2d 3728	. . . . . . . . . . . . . 14 |- (((U e. NrmCVec /\ x e. X) /\ y e. X) -> (N` (xMy)) = (N` (xG(-u1(.s` U)y))))
15	14	opreq1d 3975	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ x e. X) /\ y e. X) -> ((N` (xMy))^2) = ((N` (xG(-u1(.s` U)y)))^2))
16	15	opreq2d 3976	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ x e. X) /\ y e. X) -> (((N` (xGy))^2) + ((N` (xMy))^2)) = (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)))
17	16	eqeq1d 1483	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ x e. X) /\ y e. X) -> ((((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))) <-> (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
18	17	ralbidva 1659	. . . . . . . . . 10 |- ((U e. NrmCVec /\ x e. X) -> (A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))) <-> A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
19	18	ralbidva 1659	. . . . . . . . 9 |- (U e. NrmCVec -> (A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))) <-> A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
20	19	pm5.32i 645	. . . . . . . 8 |- ((U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))) <-> (U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
21	9, 20	syl5rbb 533	. . . . . . 7 |- (U = <.<.G, (.s` U)>., N>. -> ((<.<.G, (.s` U)>., N>. e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))) <-> (U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
22		fvex 3732	. . . . . . . . 9 |- (+v` U) e. V
23	3, 22	eqeltr 1544	. . . . . . . 8 |- G e. V
24		fvex 3732	. . . . . . . . 9 |- (.s` U) e. V
25	4, 24	eqeltr 1544	. . . . . . . 8 |- (.s` U) e. V
26		fvex 3732	. . . . . . . . 9 |- (norm` U) e. V
27	5, 26	eqeltr 1544	. . . . . . . 8 |- N e. V
28	10, 3	bafval 8223	. . . . . . . . 9 |- X = ran G
29	28	isphg 8476	. . . . . . . 8 |- ((G e. V /\ (.s` U) e. V /\ N e. V) -> (<.<.G, (.s` U)>., N>. e. CPreHil <-> (<.<.G, (.s` U)>., N>. e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
30	23, 25, 27, 29	mp3an 916	. . . . . . 7 |- (<.<.G, (.s` U)>., N>. e. CPreHil <-> (<.<.G, (.s` U)>., N>. e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1(.s` U)y)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
31	21, 30	syl5bb 532	. . . . . 6 |- (U = <.<.G, (.s` U)>., N>. -> (<.<.G, (.s` U)>., N>. e. CPreHil <-> (U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
32	7, 31	bitrd 528	. . . . 5 |- (U = <.<.G, (.s` U)>., N>. -> (U e. CPreHil <-> (U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
33	6, 32	syl 10	. . . 4 |- (U e. NrmCVec -> (U e. CPreHil <-> (U e. NrmCVec /\ A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2))))))
34	33	bianabs 653	. . 3 |- (U e. NrmCVec -> (U e. CPreHil <-> A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xMy))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
35	34	pm5.32i 645	. 2 |- ((U e. NrmCVec /\ U e. CPreHil) <-> (U