Metamath Proof Explorer

Theorem lmodring

Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypothesis lmodring.1 
|- F = ( Scalar ` W )
Assertion lmodring 
|- ( W e. LMod -> F e. Ring )

Proof

Step Hyp Ref Expression
1 lmodring.1 
 |-  F = ( Scalar ` W )
2 eqid 
 |-  ( Base ` W ) = ( Base ` W )
3 eqid 
 |-  ( +g ` W ) = ( +g ` W )
4 eqid 
 |-  ( .s ` W ) = ( .s ` W )
5 eqid 
 |-  ( Base ` F ) = ( Base ` F )
6 eqid 
 |-  ( +g ` F ) = ( +g ` F )
7 eqid 
 |-  ( .r ` F ) = ( .r ` F )
8 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
9 2 3 4 1 5 6 7 8 islmod 
 |-  ( W e. LMod <-> ( W e. Grp /\ F e. Ring /\ A. q e. ( Base ` F ) A. r e. ( Base ` F ) A. x e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) x ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) x ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` F ) ( .s ` W ) w ) = w ) ) ) )
10 9 simp2bi 
 |-  ( W e. LMod -> F e. Ring )