# 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 )`