Theorem lmodn0

Description: Left modules exist. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Assertion	lmodn0	$$⊢\mathrm{LMod}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢i\in \mathrm{V}$$
2		vex	$$⊢z\in \mathrm{V}$$
3	1 2	pm3.2i	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)$$
4		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}$$
5		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}$$
6	4 5	lmod1zr	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LMod}$$
7		ne0i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LMod}\to \mathrm{LMod}\ne \varnothing$$
8	3 6 7	mp2b	$$⊢\mathrm{LMod}\ne \varnothing$$