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

Proof

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

Metamath Proof Explorer

Theorem cnlmod

Proof