cnlmod4

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

Step	Hyp	Ref	Expression
1		cnlmod.w	$⊢ W = \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩\} \cup \{⟨Scalar (ndx), ℂ_{fld}⟩, ⟨\cdot_{ndx} \times⟩\}$
2		mulex	$⊢ \times \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	lmodvsca	$⊢ \times \in V \to \times = \cdot_{W}$
6	5	eqcomd	$⊢ \times \in V \to \cdot_{W} = \times$
7	2 6	ax-mp	$⊢ \cdot_{W} = \times$

Metamath Proof Explorer