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