Metamath Proof Explorer

Theorem sraassa

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

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 eqid 
 |-  ( Base ` W ) = ( Base ` W )
3 2 subrgss 
 |-  ( S e. ( SubRing ` W ) -> S C_ ( Base ` W ) )
4 3 adantl 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> S C_ ( Base ` W ) )
5 eqid 
 |-  ( Cntr ` ( mulGrp ` W ) ) = ( Cntr ` ( mulGrp ` W ) )
6 2 5 crngbascntr 
 |-  ( W e. CRing -> ( Base ` W ) = ( Cntr ` ( mulGrp ` W ) ) )
7 6 adantr 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Cntr ` ( mulGrp ` W ) ) )
8 4 7 sseqtrd 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> S C_ ( Cntr ` ( mulGrp ` W ) ) )
9 crngring 
 |-  ( W e. CRing -> W e. Ring )
10 9 adantr 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> W e. Ring )
11 simpr 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> S e. ( SubRing ` W ) )
12 1 5 10 11 sraassab 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> ( A e. AssAlg <-> S C_ ( Cntr ` ( mulGrp ` W ) ) ) )
13 8 12 mpbird 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> A e. AssAlg )