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 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
Assertion sraassaOLD ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 sraassa.a 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
2 1 a1i ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
3 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 3 subrgss ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
5 4 adantl ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
6 2 5 srabase ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
7 2 5 srasca ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑊s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
8 eqid ( 𝑊s 𝑆 ) = ( 𝑊s 𝑆 )
9 8 subrgbas ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 = ( Base ‘ ( 𝑊s 𝑆 ) ) )
10 9 adantl ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 = ( Base ‘ ( 𝑊s 𝑆 ) ) )
11 2 5 sravsca ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( .r𝑊 ) = ( ·𝑠𝐴 ) )
12 2 5 sramulr ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( .r𝑊 ) = ( .r𝐴 ) )
13 1 sralmod ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ∈ LMod )
14 13 adantl ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ LMod )
15 crngring ( 𝑊 ∈ CRing → 𝑊 ∈ Ring )
16 15 adantr ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑊 ∈ Ring )
17 eqidd ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
18 2 5 sraaddg ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( +g𝑊 ) = ( +g𝐴 ) )
19 18 oveqdr ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g𝑊 ) 𝑦 ) = ( 𝑥 ( +g𝐴 ) 𝑦 ) )
20 12 oveqdr ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r𝑊 ) 𝑦 ) = ( 𝑥 ( .r𝐴 ) 𝑦 ) )
21 17 6 19 20 ringpropd ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑊 ∈ Ring ↔ 𝐴 ∈ Ring ) )
22 16 21 mpbid ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ Ring )
23 16 adantr ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
24 5 adantr ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
25 simpr1 ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥𝑆 )
26 24 25 sseldd ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
27 simpr2 ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
28 simpr3 ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
29 eqid ( .r𝑊 ) = ( .r𝑊 )
30 3 29 ringass ( ( 𝑊 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r𝑊 ) 𝑦 ) ( .r𝑊 ) 𝑧 ) = ( 𝑥 ( .r𝑊 ) ( 𝑦 ( .r𝑊 ) 𝑧 ) ) )
31 23 26 27 28 30 syl13anc ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r𝑊 ) 𝑦 ) ( .r𝑊 ) 𝑧 ) = ( 𝑥 ( .r𝑊 ) ( 𝑦 ( .r𝑊 ) 𝑧 ) ) )
32 eqid ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
33 32 crngmgp ( 𝑊 ∈ CRing → ( mulGrp ‘ 𝑊 ) ∈ CMnd )
34 33 ad2antrr ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( mulGrp ‘ 𝑊 ) ∈ CMnd )
35 32 3 mgpbas ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
36 32 29 mgpplusg ( .r𝑊 ) = ( +g ‘ ( mulGrp ‘ 𝑊 ) )
37 35 36 cmn12 ( ( ( mulGrp ‘ 𝑊 ) ∈ CMnd ∧ ( 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r𝑊 ) ( 𝑥 ( .r𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r𝑊 ) ( 𝑦 ( .r𝑊 ) 𝑧 ) ) )
38 34 27 26 28 37 syl13anc ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥𝑆𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r𝑊 ) ( 𝑥 ( .r𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r𝑊 ) ( 𝑦 ( .r𝑊 ) 𝑧 ) ) )
39 6 7 10 11 12 14 22 31 38 isassad ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )