Metamath Proof Explorer

Theorem lmodslmd

Description: Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion lmodslmd 
|- ( W e. LMod -> W e. SLMod )

Proof

Step Hyp Ref Expression
1 lmodcmn 
 |-  ( W e. LMod -> W e. CMnd )
2 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
3 2 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
4 ringsrg 
 |-  ( ( Scalar ` W ) e. Ring -> ( Scalar ` W ) e. SRing )
5 3 4 syl 
 |-  ( W e. LMod -> ( Scalar ` W ) e. SRing )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( +g ` W ) = ( +g ` W )
8 eqid 
 |-  ( .s ` W ) = ( .s ` W )
9 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
10 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
11 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
12 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
13 6 7 8 2 9 10 11 12 islmod 
 |-  ( W e. LMod <-> ( W e. Grp /\ ( Scalar ` W ) e. Ring /\ A. q e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
14 13 simp3bi 
 |-  ( W e. LMod -> A. q e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
15 14 r19.21bi 
 |-  ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) -> A. r e. ( Base ` ( Scalar ` W ) ) 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
16 15 r19.21bi 
 |-  ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) -> 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
17 16 r19.21bi 
 |-  ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
18 17 r19.21bi 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
19 18 simpld 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) )
20 18 simprd 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ w e. ( Base ` W ) ) -> ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) )
21 20 simpld 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ w e. ( Base ` W ) ) -> ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) )
22 20 simprd 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ w e. ( Base ` W ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w )
23 simp-4l 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ w e. ( Base ` W ) ) -> W e. LMod )
24 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
25 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
26 6 2 8 24 25 lmod0vs 
 |-  ( ( W e. LMod /\ w e. ( Base ` W ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) )
27 23 26 sylancom 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ w e. ( Base ` W ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) )
28 21 22 27 3jca 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ w e. ( Base ` W ) ) -> ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) )
29 19 28 jca 
 |-  ( ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) /\ 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) ) )
30 29 ralrimiva 
 |-  ( ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) ) )
31 30 ralrimiva 
 |-  ( ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ r e. ( Base ` ( Scalar ` W ) ) ) -> 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) ) )
32 31 ralrimiva 
 |-  ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) ) -> A. r e. ( Base ` ( Scalar ` W ) ) 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) ) )
33 32 ralrimiva 
 |-  ( W e. LMod -> A. q e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) ) )
34 6 7 8 25 2 9 10 11 12 24 isslmd 
 |-  ( W e. SLMod <-> ( W e. CMnd /\ ( Scalar ` W ) e. SRing /\ A. q e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) 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 ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( q ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( q ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) w ) = ( 0g ` W ) ) ) ) )
35 1 5 33 34 syl3anbrc 
 |-  ( W e. LMod -> W e. SLMod )