This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ·𝑠 ‘ 𝑊 ) = ·