Metamath Proof Explorer


Theorem nvvop

Description: The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvvop.1 𝑊 = ( 1st𝑈 )
nvvop.2 𝐺 = ( +𝑣𝑈 )
nvvop.4 𝑆 = ( ·𝑠OLD𝑈 )
Assertion nvvop ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ 𝐺 , 𝑆 ⟩ )

Proof

Step Hyp Ref Expression
1 nvvop.1 𝑊 = ( 1st𝑈 )
2 nvvop.2 𝐺 = ( +𝑣𝑈 )
3 nvvop.4 𝑆 = ( ·𝑠OLD𝑈 )
4 vcrel Rel CVecOLD
5 nvss NrmCVec ⊆ ( CVecOLD × V )
6 eqid ( normCV𝑈 ) = ( normCV𝑈 )
7 1 6 nvop2 ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ 𝑊 , ( normCV𝑈 ) ⟩ )
8 7 eleq1d ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ NrmCVec ↔ ⟨ 𝑊 , ( normCV𝑈 ) ⟩ ∈ NrmCVec ) )
9 8 ibi ( 𝑈 ∈ NrmCVec → ⟨ 𝑊 , ( normCV𝑈 ) ⟩ ∈ NrmCVec )
10 5 9 sselid ( 𝑈 ∈ NrmCVec → ⟨ 𝑊 , ( normCV𝑈 ) ⟩ ∈ ( CVecOLD × V ) )
11 opelxp1 ( ⟨ 𝑊 , ( normCV𝑈 ) ⟩ ∈ ( CVecOLD × V ) → 𝑊 ∈ CVecOLD )
12 10 11 syl ( 𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD )
13 1st2nd ( ( Rel CVecOLD𝑊 ∈ CVecOLD ) → 𝑊 = ⟨ ( 1st𝑊 ) , ( 2nd𝑊 ) ⟩ )
14 4 12 13 sylancr ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ ( 1st𝑊 ) , ( 2nd𝑊 ) ⟩ )
15 2 vafval 𝐺 = ( 1st ‘ ( 1st𝑈 ) )
16 1 fveq2i ( 1st𝑊 ) = ( 1st ‘ ( 1st𝑈 ) )
17 15 16 eqtr4i 𝐺 = ( 1st𝑊 )
18 3 smfval 𝑆 = ( 2nd ‘ ( 1st𝑈 ) )
19 1 fveq2i ( 2nd𝑊 ) = ( 2nd ‘ ( 1st𝑈 ) )
20 18 19 eqtr4i 𝑆 = ( 2nd𝑊 )
21 17 20 opeq12i 𝐺 , 𝑆 ⟩ = ⟨ ( 1st𝑊 ) , ( 2nd𝑊 ) ⟩
22 14 21 eqtr4di ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ 𝐺 , 𝑆 ⟩ )