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

Metamath Proof Explorer

Theorem cnstrcvs

Description: The set of complex numbers is a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by NM, 5-Nov-2006) (Revised by AV, 20-Sep-2021)

Ref Expression
Hypothesis cnlmod.w ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
Assertion cnstrcvs 𝑊 ∈ ℂVec

Proof

Step Hyp Ref Expression
1 cnlmod.w ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
2 1 cnlmod ⊢ 𝑊 ∈ LMod
3 cnfldex ⊢ ℂfld ∈ V
4 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
5 4 ressid ⊢ ( ℂfld ∈ V → ( ℂfld ↾s ℂ ) = ℂfld )
6 3 5 ax-mp ⊢ ( ℂfld ↾s ℂ ) = ℂfld
7 6 eqcomi ⊢ ℂfld = ( ℂfld ↾s ℂ )
8 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
9 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
10 negcl ⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
11 ax-1cn ⊢ 1 ∈ ℂ
12 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
13 8 9 10 11 12 cnsubrglem ⊢ ℂ ∈ ( SubRing ‘ ℂfld )
14 qdass ⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
15 1 14 eqtri ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
16 15 lmodsca ⊢ ( ℂfld ∈ V → ℂfld = ( Scalar ‘ 𝑊 ) )
17 3 16 ax-mp ⊢ ℂfld = ( Scalar ‘ 𝑊 )
18 17 isclmi ⊢ ( ( 𝑊 ∈ LMod ∧ ℂfld = ( ℂfld ↾s ℂ ) ∧ ℂ ∈ ( SubRing ‘ ℂfld ) ) → 𝑊 ∈ ℂMod )
19 2 7 13 18 mp3an ⊢ 𝑊 ∈ ℂMod
20 cndrng ⊢ ℂfld ∈ DivRing
21 17 islvec ⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ ℂfld ∈ DivRing ) )
22 2 20 21 mpbir2an ⊢ 𝑊 ∈ LVec
23 19 22 elini ⊢ 𝑊 ∈ ( ℂMod ∩ LVec )
24 df-cvs ⊢ ℂVec = ( ℂMod ∩ LVec )
25 23 24 eleqtrri ⊢ 𝑊 ∈ ℂVec