Theorem cnlmod4

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

	Ref	Expression
Hypothesis	cnlmod.w	⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
Assertion	cnlmod4	⊢ ( ·𝑠 ‘ 𝑊 ) = ·

Proof

Step	Hyp	Ref	Expression
1		cnlmod.w	⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
2		mulex	⊢ · ∈ V
3		qdass	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
4	1 3	eqtri	⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
5	4	lmodvsca	⊢ ( · ∈ V → · = ( ·𝑠 ‘ 𝑊 ) )
6	5	eqcomd	⊢ ( · ∈ V → ( ·𝑠 ‘ 𝑊 ) = · )
7	2 6	ax-mp	⊢ ( ·𝑠 ‘ 𝑊 ) = ·