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 
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
Assertion cnlmodlem2 
|- ( +g ` W ) = +

Proof

Step Hyp Ref Expression
1 cnlmod.w 
 |-  W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
2 addex 
 |-  + e. _V
3 qdass 
 |-  ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } ) = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( Scalar ` ndx ) , CCfld >. } u. { <. ( .s ` ndx ) , x. >. } )
4 1 3 eqtri 
 |-  W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( Scalar ` ndx ) , CCfld >. } u. { <. ( .s ` ndx ) , x. >. } )
5 4 lmodplusg 
 |-  ( + e. _V -> + = ( +g ` W ) )
6 5 eqcomd 
 |-  ( + e. _V -> ( +g ` W ) = + )
7 2 6 ax-mp 
 |-  ( +g ` W ) = +