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 ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
Assertion sraassa ( ( 𝑊 ∈ 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 8 subrgcrng ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑊 ↾s 𝑆 ) ∈ CRing )
24 16 adantr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
25 5 adantr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
26 simpr1 ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ 𝑆 )
27 25 26 sseldd ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
28 simpr2 ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
29 simpr3 ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
30 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
31 3 30 ringass ⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
32 24 27 28 29 31 syl13anc ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
33 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
34 33 crngmgp ⊢ ( 𝑊 ∈ CRing → ( mulGrp ‘ 𝑊 ) ∈ CMnd )
35 34 ad2antrr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( mulGrp ‘ 𝑊 ) ∈ CMnd )
36 33 3 mgpbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
37 33 30 mgpplusg ⊢ ( .r ‘ 𝑊 ) = ( +g ‘ ( mulGrp ‘ 𝑊 ) )
38 36 37 cmn12 ⊢ ( ( ( mulGrp ‘ 𝑊 ) ∈ CMnd ∧ ( 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
39 35 28 27 29 38 syl13anc ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
40 6 7 10 11 12 14 22 23 32 39 isassad ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )