Metamath Proof Explorer


Theorem phop

Description: A complex inner product space in terms of ordered pair components. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses phop.2 𝐺 = ( +𝑣𝑈 )
phop.4 𝑆 = ( ·𝑠OLD𝑈 )
phop.6 𝑁 = ( normCV𝑈 )
Assertion phop ( 𝑈 ∈ CPreHilOLD𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )

Proof

Step Hyp Ref Expression
1 phop.2 𝐺 = ( +𝑣𝑈 )
2 phop.4 𝑆 = ( ·𝑠OLD𝑈 )
3 phop.6 𝑁 = ( normCV𝑈 )
4 phrel Rel CPreHilOLD
5 1st2nd ( ( Rel CPreHilOLD𝑈 ∈ CPreHilOLD ) → 𝑈 = ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩ )
6 4 5 mpan ( 𝑈 ∈ CPreHilOLD𝑈 = ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩ )
7 3 nmcvfval 𝑁 = ( 2nd𝑈 )
8 7 opeq2i ⟨ ( 1st𝑈 ) , 𝑁 ⟩ = ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩
9 phnv ( 𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec )
10 eqid ( 1st𝑈 ) = ( 1st𝑈 )
11 10 nvvc ( 𝑈 ∈ NrmCVec → ( 1st𝑈 ) ∈ CVecOLD )
12 vcrel Rel CVecOLD
13 1st2nd ( ( Rel CVecOLD ∧ ( 1st𝑈 ) ∈ CVecOLD ) → ( 1st𝑈 ) = ⟨ ( 1st ‘ ( 1st𝑈 ) ) , ( 2nd ‘ ( 1st𝑈 ) ) ⟩ )
14 12 13 mpan ( ( 1st𝑈 ) ∈ CVecOLD → ( 1st𝑈 ) = ⟨ ( 1st ‘ ( 1st𝑈 ) ) , ( 2nd ‘ ( 1st𝑈 ) ) ⟩ )
15 1 vafval 𝐺 = ( 1st ‘ ( 1st𝑈 ) )
16 2 smfval 𝑆 = ( 2nd ‘ ( 1st𝑈 ) )
17 15 16 opeq12i 𝐺 , 𝑆 ⟩ = ⟨ ( 1st ‘ ( 1st𝑈 ) ) , ( 2nd ‘ ( 1st𝑈 ) ) ⟩
18 14 17 eqtr4di ( ( 1st𝑈 ) ∈ CVecOLD → ( 1st𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
19 9 11 18 3syl ( 𝑈 ∈ CPreHilOLD → ( 1st𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
20 19 opeq1d ( 𝑈 ∈ CPreHilOLD → ⟨ ( 1st𝑈 ) , 𝑁 ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
21 8 20 eqtr3id ( 𝑈 ∈ CPreHilOLD → ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
22 6 21 eqtrd ( 𝑈 ∈ CPreHilOLD𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )