Theorem 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	⊢ 𝑋 = ran 𝐺
Assertion	isphg	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶 ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isphg.1	⊢ 𝑋 = ran 𝐺
2		df-ph	⊢ CPreHilOLD = ( NrmCVec ∩ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } )
3	2	elin2	⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } ) )
4		rneq	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
5	4 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
6		oveq	⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
7	6	fveq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) )
8	7	oveq1d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) = ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) )
9		oveq	⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) = ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) )
10	9	fveq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) = ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) )
11	10	oveq1d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) )
12	8 11	oveq12d	⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) )
13	12	eqeq1d	⊢ ( 𝑔 = 𝐺 → ( ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
14	5 13	raleqbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
15	5 14	raleqbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
16		oveq	⊢ ( 𝑠 = 𝑆 → ( - 1 𝑠 𝑦 ) = ( - 1 𝑆 𝑦 ) )
17	16	oveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) = ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) )
18	17	fveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) = ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
19	18	oveq1d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) )
20	19	oveq2d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
21	20	eqeq1d	⊢ ( 𝑠 = 𝑆 → ( ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
22	21	2ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
23		fveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) )
24	23	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) )
25		fveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
26	25	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) )
27	24 26	oveq12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
28		fveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) )
29	28	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) )
30		fveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
31	30	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) )
32	29 31	oveq12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) )
33	32	oveq2d	⊢ ( 𝑛 = 𝑁 → ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
34	27 33	eqeq12d	⊢ ( 𝑛 = 𝑁 → ( ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
35	34	2ralbidv	⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
36	15 22 35	eloprabg	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶 ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
37	36	anbi2d	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶 ) → ( ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } ) ↔ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
38	3 37	bitrid	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶 ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )