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

Metamath Proof Explorer

Theorem cnlmod

Description: The set of complex numbers is a left module over itself. The vector operation is + , and the scalar product is x. . (Contributed by AV, 20-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 cnlmod.w ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
2 0cn ⊢ 0 ∈ ℂ
3 1 cnlmodlem1 ⊢ ( Base ‘ 𝑊 ) = ℂ
4 3 eqcomi ⊢ ℂ = ( Base ‘ 𝑊 )
5 4 a1i ⊢ ( 0 ∈ ℂ → ℂ = ( Base ‘ 𝑊 ) )
6 1 cnlmodlem2 ⊢ ( +g ‘ 𝑊 ) = +
7 6 eqcomi ⊢ + = ( +g ‘ 𝑊 )
8 7 a1i ⊢ ( 0 ∈ ℂ → + = ( +g ‘ 𝑊 ) )
9 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
10 9 3adant1 ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
11 addass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
12 11 adantl ⊢ ( ( 0 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
13 id ⊢ ( 0 ∈ ℂ → 0 ∈ ℂ )
14 addlid ⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
15 14 adantl ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 + 𝑥 ) = 𝑥 )
16 negcl ⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
17 16 adantl ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → - 𝑥 ∈ ℂ )
18 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
19 16 18 addcomd ⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
20 19 adantl ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
21 negid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = 0 )
22 21 adantl ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 + - 𝑥 ) = 0 )
23 20 22 eqtrd ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - 𝑥 + 𝑥 ) = 0 )
24 5 8 10 12 13 15 17 23 isgrpd ⊢ ( 0 ∈ ℂ → 𝑊 ∈ Grp )
25 4 a1i ⊢ ( 𝑊 ∈ Grp → ℂ = ( Base ‘ 𝑊 ) )
26 7 a1i ⊢ ( 𝑊 ∈ Grp → + = ( +g ‘ 𝑊 ) )
27 1 cnlmodlem3 ⊢ ( Scalar ‘ 𝑊 ) = ℂfld
28 27 eqcomi ⊢ ℂfld = ( Scalar ‘ 𝑊 )
29 28 a1i ⊢ ( 𝑊 ∈ Grp → ℂfld = ( Scalar ‘ 𝑊 ) )
30 1 cnlmod4 ⊢ ( ·𝑠 ‘ 𝑊 ) = ·
31 30 eqcomi ⊢ · = ( ·𝑠 ‘ 𝑊 )
32 31 a1i ⊢ ( 𝑊 ∈ Grp → · = ( ·𝑠 ‘ 𝑊 ) )
33 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
34 33 a1i ⊢ ( 𝑊 ∈ Grp → ℂ = ( Base ‘ ℂfld ) )
35 cnfldadd ⊢ + = ( +g ‘ ℂfld )
36 35 a1i ⊢ ( 𝑊 ∈ Grp → + = ( +g ‘ ℂfld ) )
37 cnfldmul ⊢ · = ( .r ‘ ℂfld )
38 37 a1i ⊢ ( 𝑊 ∈ Grp → · = ( .r ‘ ℂfld ) )
39 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
40 39 a1i ⊢ ( 𝑊 ∈ Grp → 1 = ( 1r ‘ ℂfld ) )
41 cnring ⊢ ℂfld ∈ Ring
42 41 a1i ⊢ ( 𝑊 ∈ Grp → ℂfld ∈ Ring )
43 id ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ Grp )
44 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
45 44 3adant1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
46 adddi ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
47 46 adantl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
48 adddir ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
49 48 adantl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
50 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
51 50 adantl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
52 mullid ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
53 52 adantl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑥 ∈ ℂ ) → ( 1 · 𝑥 ) = 𝑥 )
54 25 26 29 32 34 36 38 40 42 43 45 47 49 51 53 islmodd ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ LMod )
55 2 24 54 mp2b ⊢ 𝑊 ∈ LMod