This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isph

Description: The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isph.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
isph.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
isph.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
isph.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion isph ( 𝑈 ∈ CPreHilOLD ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isph.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 isph.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 isph.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4 isph.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
5 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
6 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
7 2 6 4 nvop ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ )
8 eleq1 ⊢ ( 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ → ( 𝑈 ∈ CPreHilOLD ↔ ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ) )
9 2 fvexi ⊢ 𝐺 ∈ V
10 fvex ⊢ ( ·𝑠OLD ‘ 𝑈 ) ∈ V
11 4 fvexi ⊢ 𝑁 ∈ V
12 1 2 bafval ⊢ 𝑋 = ran 𝐺
13 12 isphg ⊢ ( ( 𝐺 ∈ V ∧ ( ·𝑠OLD ‘ 𝑈 ) ∈ V ∧ 𝑁 ∈ V ) → ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
14 9 10 11 13 mp3an ⊢ ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
15 1 2 6 3 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) )
16 15 3expa ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) )
17 16 fveq2d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) )
18 17 oveq1d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) )
19 18 oveq2d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) )
20 19 eqeq1d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
21 20 ralbidva ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
22 21 ralbidva ⊢ ( 𝑈 ∈ NrmCVec → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
23 22 pm5.32i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
24 eleq1 ⊢ ( 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ → ( 𝑈 ∈ NrmCVec ↔ ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ NrmCVec ) )
25 24 anbi1d ⊢ ( 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ → ( ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ↔ ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
26 23 25 bitr2id ⊢ ( 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ → ( ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
27 14 26 bitrid ⊢ ( 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ → ( ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
28 8 27 bitrd ⊢ ( 𝑈 = ⟨ ⟨ 𝐺 , ( ·𝑠OLD ‘ 𝑈 ) ⟩ , 𝑁 ⟩ → ( 𝑈 ∈ CPreHilOLD ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
29 7 28 syl ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ CPreHilOLD ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
30 29 bianabs ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ CPreHilOLD ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
31 5 30 biadanii ⊢ ( 𝑈 ∈ CPreHilOLD ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )