Metamath Proof Explorer


Theorem cnlmod4

Description: Lemma 4 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 cnlmod4
|- ( .s ` W ) = x.

Proof

Step Hyp Ref Expression
1 cnlmod.w
 |-  W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
2 mulex
 |-  x. 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 lmodvsca
 |-  ( x. e. _V -> x. = ( .s ` W ) )
6 5 eqcomd
 |-  ( x. e. _V -> ( .s ` W ) = x. )
7 2 6 ax-mp
 |-  ( .s ` W ) = x.