Theorem cnlmodlem3

Description: Lemma 3 for cnlmod . (Contributed by AV, 20-Sep-2021)

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

Proof

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