cnlmodlem2

		Ref	Expression
	Hypothesis	cnlmod.w	$⊢ W = \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩\} \cup \{⟨Scalar (ndx), ℂ_{fld}⟩, ⟨\cdot_{ndx} \times⟩\}$
	Assertion	cnlmodlem2	$⊢ +_{W} = +$

Step	Hyp	Ref	Expression
1		cnlmod.w	$⊢ W = \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩\} \cup \{⟨Scalar (ndx), ℂ_{fld}⟩, ⟨\cdot_{ndx} \times⟩\}$
2		addex	$⊢ + \in V$
3		qdass	$⊢ \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩\} \cup \{⟨Scalar (ndx), ℂ_{fld}⟩, ⟨\cdot_{ndx} \times⟩\} = \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨Scalar (ndx), ℂ_{fld}⟩\} \cup \{⟨\cdot_{ndx} \times⟩\}$
4	1 3	eqtri	$⊢ W = \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨Scalar (ndx), ℂ_{fld}⟩\} \cup \{⟨\cdot_{ndx} \times⟩\}$
5	4	lmodplusg	$⊢ + \in V \to + = +_{W}$
6	5	eqcomd	$⊢ + \in V \to +_{W} = +$
7	2 6	ax-mp	$⊢ +_{W} = +$

Metamath Proof Explorer