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	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
Assertion	cnlmod	$$⊢W\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		cnlmod.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
2		0cn	$$⊢0\in ℂ$$
3	1	cnlmodlem1	$$⊢{\mathrm{Base}}_W=ℂ$$
4	3	eqcomi	$$⊢ℂ={\mathrm{Base}}_W$$
5	4	a1i	$$⊢0\in ℂ\to ℂ={\mathrm{Base}}_W$$
6	1	cnlmodlem2	$$⊢{+}_W=+$$
7	6	eqcomi	$$⊢+={+}_W$$
8	7	a1i	$$⊢0\in ℂ\to +={+}_W$$
9		addcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+y\in ℂ$$
10	9	3adant1	$$⊢\left(0\in ℂ\wedge x\in ℂ\wedge y\in ℂ\right)\to x+y\in ℂ$$
11		addass	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to x+y+z=x+y+z$$
12	11	adantl	$$⊢\left(0\in ℂ\wedge \left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\right)\to x+y+z=x+y+z$$
13		id	$$⊢0\in ℂ\to 0\in ℂ$$
14		addlid	$$⊢x\in ℂ\to 0+x=x$$
15	14	adantl	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to 0+x=x$$
16		negcl	$$⊢x\in ℂ\to -x\in ℂ$$
17	16	adantl	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to -x\in ℂ$$
18		id	$$⊢x\in ℂ\to x\in ℂ$$
19	16 18	addcomd	$$⊢x\in ℂ\to -x+x=x+\left(-x\right)$$
20	19	adantl	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to -x+x=x+\left(-x\right)$$
21		negid	$$⊢x\in ℂ\to x+\left(-x\right)=0$$
22	21	adantl	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to x+\left(-x\right)=0$$
23	20 22	eqtrd	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to -x+x=0$$
24	5 8 10 12 13 15 17 23	isgrpd	$$⊢0\in ℂ\to W\in \mathrm{Grp}$$
25	4	a1i	$$⊢W\in \mathrm{Grp}\to ℂ={\mathrm{Base}}_W$$
26	7	a1i	$$⊢W\in \mathrm{Grp}\to +={+}_W$$
27	1	cnlmodlem3	$$⊢\mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}$$
28	27	eqcomi	$$⊢{ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(W\right)$$
29	28	a1i	$$⊢W\in \mathrm{Grp}\to {ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(W\right)$$
30	1	cnlmod4	$$⊢{\cdot }_W=\times$$
31	30	eqcomi	$$⊢\times ={\cdot }_W$$
32	31	a1i	$$⊢W\in \mathrm{Grp}\to \times ={\cdot }_W$$
33		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
34	33	a1i	$$⊢W\in \mathrm{Grp}\to ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
35		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
36	35	a1i	$$⊢W\in \mathrm{Grp}\to +={+}_{{ℂ}_{\mathrm{fld}}}$$
37		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
38	37	a1i	$$⊢W\in \mathrm{Grp}\to \times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
39		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
40	39	a1i	$$⊢W\in \mathrm{Grp}\to 1=1_{{ℂ}_{\mathrm{fld}}}$$
41		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
42	41	a1i	$$⊢W\in \mathrm{Grp}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
43		id	$$⊢W\in \mathrm{Grp}\to W\in \mathrm{Grp}$$
44		mulcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
45	44	3adant1	$$⊢\left(W\in \mathrm{Grp}\wedge x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
46		adddi	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to x\left(y+z\right)=xy+xz$$
47	46	adantl	$$⊢\left(W\in \mathrm{Grp}\wedge \left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\right)\to x\left(y+z\right)=xy+xz$$
48		adddir	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to \left(x+y\right)z=xz+yz$$
49	48	adantl	$$⊢\left(W\in \mathrm{Grp}\wedge \left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\right)\to \left(x+y\right)z=xz+yz$$
50		mulass	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to xyz=xyz$$
51	50	adantl	$$⊢\left(W\in \mathrm{Grp}\wedge \left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\right)\to xyz=xyz$$
52		mullid	$$⊢x\in ℂ\to 1x=x$$
53	52	adantl	$$⊢\left(W\in \mathrm{Grp}\wedge x\in ℂ\right)\to 1x=x$$
54	25 26 29 32 34 36 38 40 42 43 45 47 49 51 53	islmodd	$$⊢W\in \mathrm{Grp}\to W\in \mathrm{LMod}$$
55	2 24 54	mp2b	$$⊢W\in \mathrm{LMod}$$