isphg

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. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	isphg.1	$⊢ X = ran G$
	Assertion	isphg	$⊢ (G \in A \land S \in B \land N \in C) \to (⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨G, S⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$

Proof

Step	Hyp	Ref	Expression
1		isphg.1	$⊢ X = ran G$
2		df-ph	$⊢ {CPreHil}_{OLD} = NrmCVec \cap \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\}$
3	2	elin2	$⊢ ⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨G, S⟩, N⟩ \in NrmCVec \land ⟨⟨G, S⟩, N⟩ \in \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\})$
4		rneq	$⊢ g = G \to ran g = ran G$
5	4 1	eqtr4di	$⊢ g = G \to ran g = X$
6		oveq	$⊢ g = G \to x g y = x G y$
7	6	fveq2d	$⊢ g = G \to n (x g y) = n (x G y)$
8	7	oveq1d	$⊢ g = G \to {n (x g y)}^{2} = {n (x G y)}^{2}$
9		oveq	$⊢ g = G \to x g (-1 s y) = x G (-1 s y)$
10	9	fveq2d	$⊢ g = G \to n (x g (-1 s y)) = n (x G (-1 s y))$
11	10	oveq1d	$⊢ g = G \to {n (x g (-1 s y))}^{2} = {n (x G (-1 s y))}^{2}$
12	8 11	oveq12d	$⊢ g = G \to {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = {n (x G y)}^{2} + {n (x G (-1 s y))}^{2}$
13	12	eqeq1d	$⊢ g = G \to ({n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow {n (x G y)}^{2} + {n (x G (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}))$
14	5 13	raleqbidv	$⊢ g = G \to (\forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow \forall y \in X {n (x G y)}^{2} + {n (x G (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}))$
15	5 14	raleqbidv	$⊢ g = G \to (\forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow \forall x \in X \forall y \in X {n (x G y)}^{2} + {n (x G (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}))$
16		oveq	$⊢ s = S \to -1 s y = -1 S y$
17	16	oveq2d	$⊢ s = S \to x G (-1 s y) = x G (-1 S y)$
18	17	fveq2d	$⊢ s = S \to n (x G (-1 s y)) = n (x G (-1 S y))$
19	18	oveq1d	$⊢ s = S \to {n (x G (-1 s y))}^{2} = {n (x G (-1 S y))}^{2}$
20	19	oveq2d	$⊢ s = S \to {n (x G y)}^{2} + {n (x G (-1 s y))}^{2} = {n (x G y)}^{2} + {n (x G (-1 S y))}^{2}$
21	20	eqeq1d	$⊢ s = S \to ({n (x G y)}^{2} + {n (x G (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow {n (x G y)}^{2} + {n (x G (-1 S y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}))$
22	21	2ralbidv	$⊢ s = S \to (\forall x \in X \forall y \in X {n (x G y)}^{2} + {n (x G (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow \forall x \in X \forall y \in X {n (x G y)}^{2} + {n (x G (-1 S y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}))$
23		fveq1	$⊢ n = N \to n (x G y) = N (x G y)$
24	23	oveq1d	$⊢ n = N \to {n (x G y)}^{2} = {N (x G y)}^{2}$
25		fveq1	$⊢ n = N \to n (x G (-1 S y)) = N (x G (-1 S y))$
26	25	oveq1d	$⊢ n = N \to {n (x G (-1 S y))}^{2} = {N (x G (-1 S y))}^{2}$
27	24 26	oveq12d	$⊢ n = N \to {n (x G y)}^{2} + {n (x G (-1 S y))}^{2} = {N (x G y)}^{2} + {N (x G (-1 S y))}^{2}$
28		fveq1	$⊢ n = N \to n (x) = N (x)$
29	28	oveq1d	$⊢ n = N \to {n (x)}^{2} = {N (x)}^{2}$
30		fveq1	$⊢ n = N \to n (y) = N (y)$
31	30	oveq1d	$⊢ n = N \to {n (y)}^{2} = {N (y)}^{2}$
32	29 31	oveq12d	$⊢ n = N \to {n (x)}^{2} + {n (y)}^{2} = {N (x)}^{2} + {N (y)}^{2}$
33	32	oveq2d	$⊢ n = N \to 2 ({n (x)}^{2} + {n (y)}^{2}) = 2 ({N (x)}^{2} + {N (y)}^{2})$
34	27 33	eqeq12d	$⊢ n = N \to ({n (x G y)}^{2} + {n (x G (-1 S y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
35	34	2ralbidv	$⊢ n = N \to (\forall x \in X \forall y \in X {n (x G y)}^{2} + {n (x G (-1 S y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2}) \leftrightarrow \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
36	15 22 35	eloprabg	$⊢ (G \in A \land S \in B \land N \in C) \to (⟨⟨G, S⟩, N⟩ \in \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\} \leftrightarrow \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
37	36	anbi2d	$⊢ (G \in A \land S \in B \land N \in C) \to ((⟨⟨G, S⟩, N⟩ \in NrmCVec \land ⟨⟨G, S⟩, N⟩ \in \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\}) \leftrightarrow (⟨⟨G, S⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
38	3 37	bitrid	$⊢ (G \in A \land S \in B \land N \in C) \to (⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨G, S⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$

Metamath Proof Explorer

Theorem isphg

Proof