Theorem isphg 8472

Description: The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is G, the scalar product is S, and the norm is N. An inner product space is also called a pre-Hilbert space.

Hypothesis

Ref	Expression
isphg.1	|- X = ran G

Assertion

Ref	Expression
isphg	|- ((G e. A /\ S e. B /\ N e. C) -> (<.<.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))))))

Distinct variable groups:   x,y,G   x,N,y   x,S,y   x,X,y

Proof of Theorem isphg

Step	Hyp	Ref	Expression
1		rneq 3345	. . . . . 6 |- (g = G -> ran g = ran G)
2		isphg.1	. . . . . 6 |- X = ran G
3	1, 2	syl6eqr 1528	. . . . 5 |- (g = G -> ran g = X)
4		opreq 3973	. . . . . . . . . 10 |- (g = G -> (xgy) = (xGy))
5	4	fveq2d 3734	. . . . . . . . 9 |- (g = G -> (n` (xgy)) = (n` (xGy)))
6	5	opreq1d 3981	. . . . . . . 8 |- (g = G -> ((n` (xgy))^2) = ((n` (xGy))^2))
7		opreq 3973	. . . . . . . . . 10 |- (g = G -> (xg(-u1sy)) = (xG(-u1sy)))
8	7	fveq2d 3734	. . . . . . . . 9 |- (g = G -> (n` (xg(-u1sy))) = (n` (xG(-u1sy))))
9	8	opreq1d 3981	. . . . . . . 8 |- (g = G -> ((n` (xg(-u1sy)))^2) = ((n` (xG(-u1sy)))^2))
10	6, 9	opreq12d 3984	. . . . . . 7 |- (g = G -> (((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)))
11	10	eqeq1d 1486	. . . . . 6 |- (g = G -> ((((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> (((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))))
12	3, 11	raleq12d 1797	. . . . 5 |- (g = G -> (A.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> A.y e. X (((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))))
13	3, 12	raleq12d 1797	. . . 4 |- (g = G -> (A.x e. ran gA.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> A.x e. X A.y e. X (((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))))
14		opreq 3973	. . . . . . . . . 10 |- (s = S -> (-u1sy) = (-u1Sy))
15	14	opreq2d 3982	. . . . . . . . 9 |- (s = S -> (xG(-u1sy)) = (xG(-u1Sy)))
16	15	fveq2d 3734	. . . . . . . 8 |- (s = S -> (n` (xG(-u1sy))) = (n` (xG(-u1Sy))))
17	16	opreq1d 3981	. . . . . . 7 |- (s = S -> ((n` (xG(-u1sy)))^2) = ((n` (xG(-u1Sy)))^2))
18	17	opreq2d 3982	. . . . . 6 |- (s = S -> (((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)) = (((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)))
19	18	eqeq1d 1486	. . . . 5 |- (s = S -> ((((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> (((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))))
20	19	2ralbidv 1683	. . . 4 |- (s = S -> (A.x e. X A.y e. X (((n` (xGy))^2) + ((n` (xG(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> A.x e. X A.y e. X (((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))))
21		fveq1 3729	. . . . . . . . 9 |- (n = N -> (n` (xGy)) = (N` (xGy)))
22	21	opreq1d 3981	. . . . . . . 8 |- (n = N -> ((n` (xGy))^2) = ((N` (xGy))^2))
23		fveq1 3729	. . . . . . . . 9 |- (n = N -> (n` (xG(-u1Sy))) = (N` (xG(-u1Sy))))
24	23	opreq1d 3981	. . . . . . . 8 |- (n = N -> ((n` (xG(-u1Sy)))^2) = ((N` (xG(-u1Sy)))^2))
25	22, 24	opreq12d 3984	. . . . . . 7 |- (n = N -> (((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)) = (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)))
26		fveq1 3729	. . . . . . . . . 10 |- (n = N -> (n` x) = (N` x))
27	26	opreq1d 3981	. . . . . . . . 9 |- (n = N -> ((n` x)^2) = ((N` x)^2))
28		fveq1 3729	. . . . . . . . . 10 |- (n = N -> (n` y) = (N` y))
29	28	opreq1d 3981	. . . . . . . . 9 |- (n = N -> ((n` y)^2) = ((N` y)^2))
30	27, 29	opreq12d 3984	. . . . . . . 8 |- (n = N -> (((n` x)^2) + ((n` y)^2)) = (((N` x)^2) + ((N` y)^2)))
31	30	opreq2d 3982	. . . . . . 7 |- (n = N -> (2 x. (((n` x)^2) + ((n` y)^2))) = (2 x. (((N` x)^2) + ((N` y)^2))))
32	25, 31	eqeq12d 1492	. . . . . 6 |- (n = N -> ((((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
33	32	ralbidv 1666	. . . . 5 |- (n = N -> (A.y e. X (((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
34	33	ralbidv 1666	. . . 4 |- (n = N -> (A.x e. X A.y e. X (((n` (xGy))^2) + ((n` (xG(-u1Sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2))) <-> A.x e. X A.y e. X (((N` (xGy))^2) + ((N` (xG(-u1Sy)))^2)) = (2 x. (((N` x)^2) + ((N` y)^2)))))
35	13, 20, 34	eloprabg 4013	. . 3 |- ((G e. A