Metamath Proof Explorer

Theorem sraassa

Description: The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypothesis sraassa.a 
|- A = ( ( subringAlg ` W ) ` S )
Assertion sraassa 
|- ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> A e. AssAlg )

Proof

Step Hyp Ref Expression
1 sraassa.a 
 |-  A = ( ( subringAlg ` W ) ` S )
2 1 a1i 
 |-  ( ( W e. CRing /\ 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 4 adantl 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> S C_ ( Base ` W ) )
6 2 5 srabase 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Base ` A ) )
7 2 5 srasca 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( W |`s S ) = ( Scalar ` A ) )
8 eqid 
 |-  ( W |`s S ) = ( W |`s S )
9 8 subrgbas 
 |-  ( S e. ( SubRing ` W ) -> S = ( Base ` ( W |`s S ) ) )
10 9 adantl 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> S = ( Base ` ( W |`s S ) ) )
11 2 5 sravsca 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( .r ` W ) = ( .s ` A ) )
12 2 5 sramulr 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( .r ` W ) = ( .r ` A ) )
13 1 sralmod 
 |-  ( S e. ( SubRing ` W ) -> A e. LMod )
14 13 adantl 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> A e. LMod )
15 crngring 
 |-  ( W e. CRing -> W e. Ring )
16 15 adantr 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> W e. Ring )
17 eqidd 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Base ` W ) )
18 2 5 sraaddg 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( +g ` W ) = ( +g ` A ) )
19 18 oveqdr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` A ) y ) )
20 12 oveqdr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( .r ` W ) y ) = ( x ( .r ` A ) y ) )
21 17 6 19 20 ringpropd 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( W e. Ring <-> A e. Ring ) )
22 16 21 mpbid 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> A e. Ring )
23 8 subrgcrng 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( W |`s S ) e. CRing )
24 16 adantr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> W e. Ring )
25 5 adantr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> S C_ ( Base ` W ) )
26 simpr1 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. S )
27 25 26 sseldd 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
28 simpr2 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
29 simpr3 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> z e. ( Base ` W ) )
30 eqid 
 |-  ( .r ` W ) = ( .r ` W )
31 3 30 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 ) ) )
32 24 27 28 29 31 syl13anc 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .r ` W ) y ) ( .r ` W ) z ) = ( x ( .r ` W ) ( y ( .r ` W ) z ) ) )
33 eqid 
 |-  ( mulGrp ` W ) = ( mulGrp ` W )
34 33 crngmgp 
 |-  ( W e. CRing -> ( mulGrp ` W ) e. CMnd )
35 34 ad2antrr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( mulGrp ` W ) e. CMnd )
36 33 3 mgpbas 
 |-  ( Base ` W ) = ( Base ` ( mulGrp ` W ) )
37 33 30 mgpplusg 
 |-  ( .r ` W ) = ( +g ` ( mulGrp ` W ) )
38 36 37 cmn12 
 |-  ( ( ( mulGrp ` W ) e. CMnd /\ ( y e. ( Base ` W ) /\ x e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( y ( .r ` W ) ( x ( .r ` W ) z ) ) = ( x ( .r ` W ) ( y ( .r ` W ) z ) ) )
39 35 28 27 29 38 syl13anc 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( y ( .r ` W ) ( x ( .r ` W ) z ) ) = ( x ( .r ` W ) ( y ( .r ` W ) z ) ) )
40 6 7 10 11 12 14 22 23 32 39 isassad 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> A e. AssAlg )