Metamath Proof Explorer

Theorem sralmod

Description: The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypothesis sralmod.a 
|- A = ( ( subringAlg ` W ) ` S )
Assertion sralmod 
|- ( S e. ( SubRing ` W ) -> A e. LMod )

Proof

Step Hyp Ref Expression
1 sralmod.a 
 |-  A = ( ( subringAlg ` W ) ` S )
2 1 a1i 
 |-  ( S e. ( SubRing ` W ) -> A = ( ( subringAlg ` W ) ` S ) )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 3 subrgss 
 |-  ( S e. ( SubRing ` W ) -> S C_ ( Base ` W ) )
5 2 4 srabase 
 |-  ( S e. ( SubRing ` W ) -> ( Base ` W ) = ( Base ` A ) )
6 2 4 sraaddg 
 |-  ( S e. ( SubRing ` W ) -> ( +g ` W ) = ( +g ` A ) )
7 2 4 srasca 
 |-  ( S e. ( SubRing ` W ) -> ( W |`s S ) = ( Scalar ` A ) )
8 2 4 sravsca 
 |-  ( S e. ( SubRing ` W ) -> ( .r ` W ) = ( .s ` A ) )
9 eqid 
 |-  ( W |`s S ) = ( W |`s S )
10 9 3 ressbas 
 |-  ( S e. ( SubRing ` W ) -> ( S i^i ( Base ` W ) ) = ( Base ` ( W |`s S ) ) )
11 eqid 
 |-  ( +g ` W ) = ( +g ` W )
12 9 11 ressplusg 
 |-  ( S e. ( SubRing ` W ) -> ( +g ` W ) = ( +g ` ( W |`s S ) ) )
13 eqid 
 |-  ( .r ` W ) = ( .r ` W )
14 9 13 ressmulr 
 |-  ( S e. ( SubRing ` W ) -> ( .r ` W ) = ( .r ` ( W |`s S ) ) )
15 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
16 9 15 subrg1 
 |-  ( S e. ( SubRing ` W ) -> ( 1r ` W ) = ( 1r ` ( W |`s S ) ) )
17 9 subrgring 
 |-  ( S e. ( SubRing ` W ) -> ( W |`s S ) e. Ring )
18 subrgrcl 
 |-  ( S e. ( SubRing ` W ) -> W e. Ring )
19 ringgrp 
 |-  ( W e. Ring -> W e. Grp )
20 18 19 syl 
 |-  ( S e. ( SubRing ` W ) -> W e. Grp )
21 eqidd 
 |-  ( S e. ( SubRing ` W ) -> ( Base ` W ) = ( Base ` W ) )
22 6 oveqdr 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` A ) y ) )
23 21 5 22 grppropd 
 |-  ( S e. ( SubRing ` W ) -> ( W e. Grp <-> A e. Grp ) )
24 20 23 mpbid 
 |-  ( S e. ( SubRing ` W ) -> A e. Grp )
25 18 3ad2ant1 
 |-  ( ( S e. ( SubRing ` W ) /\ x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> W e. Ring )
26 elinel2 
 |-  ( x e. ( S i^i ( Base ` W ) ) -> x e. ( Base ` W ) )
27 26 3ad2ant2 
 |-  ( ( S e. ( SubRing ` W ) /\ x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> x e. ( Base ` W ) )
28 simp3 
 |-  ( ( S e. ( SubRing ` W ) /\ x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> y e. ( Base ` W ) )
29 3 13 ringcl 
 |-  ( ( W e. Ring /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ( .r ` W ) y ) e. ( Base ` W ) )
30 25 27 28 29 syl3anc 
 |-  ( ( S e. ( SubRing ` W ) /\ x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> ( x ( .r ` W ) y ) e. ( Base ` W ) )
31 18 adantr 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> W e. Ring )
32 simpr1 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. ( S i^i ( Base ` W ) ) )
33 32 elin2d 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
34 simpr2 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
35 simpr3 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> z e. ( Base ` W ) )
36 3 11 13 ringdi 
 |-  ( ( W e. Ring /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( x ( .r ` W ) ( y ( +g ` W ) z ) ) = ( ( x ( .r ` W ) y ) ( +g ` W ) ( x ( .r ` W ) z ) ) )
37 31 33 34 35 36 syl13anc 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( x ( .r ` W ) ( y ( +g ` W ) z ) ) = ( ( x ( .r ` W ) y ) ( +g ` W ) ( x ( .r ` W ) z ) ) )
38 18 adantr 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> W e. Ring )
39 simpr1 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> x e. ( S i^i ( Base ` W ) ) )
40 39 elin2d 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
41 simpr2 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> y e. ( S i^i ( Base ` W ) ) )
42 41 elin2d 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
43 simpr3 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> z e. ( Base ` W ) )
44 3 11 13 ringdir 
 |-  ( ( W e. Ring /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( +g ` W ) y ) ( .r ` W ) z ) = ( ( x ( .r ` W ) z ) ( +g ` W ) ( y ( .r ` W ) z ) ) )
45 38 40 42 43 44 syl13anc 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( +g ` W ) y ) ( .r ` W ) z ) = ( ( x ( .r ` W ) z ) ( +g ` W ) ( y ( .r ` W ) z ) ) )
46 3 13 ringass 
 |-  ( ( W e. Ring /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .r ` W ) y ) ( .r ` W ) z ) = ( x ( .r ` W ) ( y ( .r ` W ) z ) ) )
47 38 40 42 43 46 syl13anc 
 |-  ( ( S e. ( SubRing ` W ) /\ ( x e. ( S i^i ( Base ` W ) ) /\ y e. ( S i^i ( Base ` W ) ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .r ` W ) y ) ( .r ` W ) z ) = ( x ( .r ` W ) ( y ( .r ` W ) z ) ) )
48 3 13 15 ringlidm 
 |-  ( ( W e. Ring /\ x e. ( Base ` W ) ) -> ( ( 1r ` W ) ( .r ` W ) x ) = x )
49 18 48 sylan 
 |-  ( ( S e. ( SubRing ` W ) /\ x e. ( Base ` W ) ) -> ( ( 1r ` W ) ( .r ` W ) x ) = x )
50 5 6 7 8 10 12 14 16 17 24 30 37 45 47 49 islmodd 
 |-  ( S e. ( SubRing ` W ) -> A e. LMod )