Metamath Proof Explorer

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