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

Metamath Proof Explorer

Theorem cnlmodlem2

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

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

Proof

Step Hyp Ref Expression
1 cnlmod.w ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ℂfld ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
2 addex ⊢ + ∈ 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 lmodplusg ⊢ ( + ∈ V → + = ( +g ‘ 𝑊 ) )
6 5 eqcomd ⊢ ( + ∈ V → ( +g ‘ 𝑊 ) = + )
7 2 6 ax-mp ⊢ ( +g ‘ 𝑊 ) = +