Metamath Proof Explorer


Theorem nvop

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

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

Proof

Step Hyp Ref Expression
1 nvop.2 𝐺 = ( +𝑣𝑈 )
2 nvop.4 𝑆 = ( ·𝑠OLD𝑈 )
3 nvop.6 𝑁 = ( normCV𝑈 )
4 nvrel Rel NrmCVec
5 1st2nd ( ( Rel NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝑈 = ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩ )
6 4 5 mpan ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩ )
7 3 nmcvfval 𝑁 = ( 2nd𝑈 )
8 7 opeq2i ⟨ ( 1st𝑈 ) , 𝑁 ⟩ = ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩
9 eqid ( 1st𝑈 ) = ( 1st𝑈 )
10 9 1 2 nvvop ( 𝑈 ∈ NrmCVec → ( 1st𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
11 10 opeq1d ( 𝑈 ∈ NrmCVec → ⟨ ( 1st𝑈 ) , 𝑁 ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
12 8 11 eqtr3id ( 𝑈 ∈ NrmCVec → ⟨ ( 1st𝑈 ) , ( 2nd𝑈 ) ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
13 6 12 eqtrd ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )