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