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

Metamath Proof Explorer

Theorem cncvs

Description: The complex left module 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, 21-Sep-2021)

Ref Expression
Hypothesis cnrlmod.c ⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion cncvs 𝐶 ∈ ℂVec

Proof

Step Hyp Ref Expression
1 cnrlmod.c ⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2 1 cnrlmod ⊢ 𝐶 ∈ 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 rlmsca ⊢ ( ℂfld ∈ V → ℂfld = ( Scalar ‘ ( ringLMod ‘ ℂfld ) ) )
15 3 14 ax-mp ⊢ ℂfld = ( Scalar ‘ ( ringLMod ‘ ℂfld ) )
16 1 eqcomi ⊢ ( ringLMod ‘ ℂfld ) = 𝐶
17 16 fveq2i ⊢ ( Scalar ‘ ( ringLMod ‘ ℂfld ) ) = ( Scalar ‘ 𝐶 )
18 15 17 eqtri ⊢ ℂfld = ( Scalar ‘ 𝐶 )
19 18 isclmi ⊢ ( ( 𝐶 ∈ LMod ∧ ℂfld = ( ℂfld ↾s ℂ ) ∧ ℂ ∈ ( SubRing ‘ ℂfld ) ) → 𝐶 ∈ ℂMod )
20 2 7 13 19 mp3an ⊢ 𝐶 ∈ ℂMod
21 1 cnrlvec ⊢ 𝐶 ∈ LVec
22 20 21 elini ⊢ 𝐶 ∈ ( ℂMod ∩ LVec )
23 df-cvs ⊢ ℂVec = ( ℂMod ∩ LVec )
24 22 23 eleqtrri ⊢ 𝐶 ∈ ℂVec