Metamath Proof Explorer

Theorem lmodn0

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

		Ref	Expression
	Assertion	lmodn0	$⊢ LMod \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ i \in V$
2		vex	$⊢ z \in V$
3	1 2	pm3.2i	$⊢ (i \in V \land z \in V)$
4		eqid	$⊢ \{⟨{Base}_{ndx}, \{z\}⟩, ⟨+_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩\} = \{⟨{Base}_{ndx}, \{z\}⟩, ⟨+_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩\}$
5		eqid	$⊢ \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩, ⟨Scalar (ndx), \{⟨{Base}_{ndx}, \{z\}⟩, ⟨+_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩\}⟩\} \cup \{⟨\cdot_{ndx}, \{⟨⟨z, i⟩, i⟩\}⟩\} = \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩, ⟨Scalar (ndx), \{⟨{Base}_{ndx}, \{z\}⟩, ⟨+_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩\}⟩\} \cup \{⟨\cdot_{ndx}, \{⟨⟨z, i⟩, i⟩\}⟩\}$
6	4 5	lmod1zr	$⊢ (i \in V \land z \in V) \to \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩, ⟨Scalar (ndx), \{⟨{Base}_{ndx}, \{z\}⟩, ⟨+_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩\}⟩\} \cup \{⟨\cdot_{ndx}, \{⟨⟨z, i⟩, i⟩\}⟩\} \in LMod$
7		ne0i	$⊢ \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩, ⟨Scalar (ndx), \{⟨{Base}_{ndx}, \{z\}⟩, ⟨+_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨z, z⟩, z⟩\}⟩\}⟩\} \cup \{⟨\cdot_{ndx}, \{⟨⟨z, i⟩, i⟩\}⟩\} \in LMod \to LMod \neq \emptyset$
8	3 6 7	mp2b	$⊢ LMod \neq \emptyset$