This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sraassaOLD

Description: Obsolete version of sraassa as of 21-Mar-2025. (Contributed by Mario Carneiro, 6-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sraassa.a 
|- A = ( ( subringAlg ` W ) ` S )
Assertion sraassaOLD 
|- ( ( 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 16 adantr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> W e. Ring )
24 5 adantr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> S C_ ( Base ` W ) )
25 simpr1 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. S )
26 24 25 sseldd 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
27 simpr2 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
28 simpr3 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> z e. ( Base ` W ) )
29 eqid 
 |-  ( .r ` W ) = ( .r ` W )
30 3 29 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 ) ) )
31 23 26 27 28 30 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 ) ) )
32 eqid 
 |-  ( mulGrp ` W ) = ( mulGrp ` W )
33 32 crngmgp 
 |-  ( W e. CRing -> ( mulGrp ` W ) e. CMnd )
34 33 ad2antrr 
 |-  ( ( ( W e. CRing /\ S e. ( SubRing ` W ) ) /\ ( x e. S /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( mulGrp ` W ) e. CMnd )
35 32 3 mgpbas 
 |-  ( Base ` W ) = ( Base ` ( mulGrp ` W ) )
36 32 29 mgpplusg 
 |-  ( .r ` W ) = ( +g ` ( mulGrp ` W ) )
37 35 36 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 ) ) )
38 34 27 26 28 37 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 ) ) )
39 6 7 10 11 12 14 22 31 38 isassad 
 |-  ( ( W e. CRing /\ S e. ( SubRing ` W ) ) -> A e. AssAlg )