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

Metamath Proof Explorer

Theorem cvsi

Description: The properties of a subcomplex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. (Contributed by NM, 3-Nov-2006) (Revised by AV, 21-Sep-2021)

Ref Expression
Hypotheses cvsi.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
cvsi.a ⊢ + = ( +g ‘ 𝑊 )
cvsi.s ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
cvsi.m ⊢ ∙ = ( ·sf ‘ 𝑊 )
cvsi.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion cvsi ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ Abel ∧ ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cvsi.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
2 cvsi.a ⊢ + = ( +g ‘ 𝑊 )
3 cvsi.s ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
4 cvsi.m ⊢ ∙ = ( ·sf ‘ 𝑊 )
5 cvsi.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 df-cvs ⊢ ℂVec = ( ℂMod ∩ LVec )
7 6 elin2 ⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) )
8 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
10 8 9 syl ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ Abel )
11 10 adantl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → 𝑊 ∈ Abel )
12 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13 12 3 clmsscn ⊢ ( 𝑊 ∈ ℂMod → 𝑆 ⊆ ℂ )
14 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
15 1 12 3 4 lmodscaf ⊢ ( 𝑊 ∈ LMod → ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 )
16 14 15 syl ⊢ ( 𝑊 ∈ ℂMod → ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 )
17 13 16 jca ⊢ ( 𝑊 ∈ ℂMod → ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) )
18 17 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) )
19 1 5 clmvs1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → ( 1 · 𝑥 ) = 𝑥 )
20 14 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → 𝑊 ∈ LMod )
21 20 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑊 ∈ LMod )
22 simplr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑦 ∈ 𝑆 )
23 simpllr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
24 simpr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
25 1 2 12 5 3 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
26 21 22 23 24 25 syl13anc ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
27 26 ralrimiva ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
28 12 clmadd ⊢ ( 𝑊 ∈ ℂMod → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
29 28 ad2antrr ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
30 29 oveqdr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 + 𝑧 ) = ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) )
31 30 oveq1d ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) )
32 20 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑊 ∈ LMod )
33 simplr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
34 simpr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
35 simpllr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
36 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
37 1 2 12 5 3 36 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
38 32 33 34 35 37 syl13anc ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
39 31 38 eqtrd ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
40 12 clmmul ⊢ ( 𝑊 ∈ ℂMod → · = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
41 40 ad2antrr ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → · = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
42 41 oveqdr ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 · 𝑧 ) = ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) )
43 42 oveq1d ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) )
44 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
45 1 12 5 3 44 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
46 32 33 34 35 45 syl13anc ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
47 43 46 eqtrd ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
48 39 47 jca ⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) )
49 48 ralrimiva ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) )
50 27 49 jca ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) )
51 50 ralrimiva ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) )
52 19 51 jca ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) )
53 52 ralrimiva ⊢ ( 𝑊 ∈ ℂMod → ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) )
54 53 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) )
55 11 18 54 3jca ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → ( 𝑊 ∈ Abel ∧ ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) ) )
56 7 55 sylbi ⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ Abel ∧ ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) ) )