# 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}=\mathrm{subringAlg}\left({W}\right)\left({S}\right)$
Assertion sraassa ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {A}\in \mathrm{AssAlg}$

### Proof

Step Hyp Ref Expression
1 sraassa.a ${⊢}{A}=\mathrm{subringAlg}\left({W}\right)\left({S}\right)$
2 1 a1i ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {A}=\mathrm{subringAlg}\left({W}\right)\left({S}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
4 3 subrgss ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {S}\subseteq {\mathrm{Base}}_{{W}}$
5 4 adantl ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {S}\subseteq {\mathrm{Base}}_{{W}}$
6 2 5 srabase ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{A}}$
7 2 5 srasca ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {W}{↾}_{𝑠}{S}=\mathrm{Scalar}\left({A}\right)$
8 eqid ${⊢}{W}{↾}_{𝑠}{S}={W}{↾}_{𝑠}{S}$
9 8 subrgbas ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {S}={\mathrm{Base}}_{\left({W}{↾}_{𝑠}{S}\right)}$
10 9 adantl ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {S}={\mathrm{Base}}_{\left({W}{↾}_{𝑠}{S}\right)}$
11 2 5 sravsca ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {\cdot }_{{W}}={\cdot }_{{A}}$
12 2 5 sramulr ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {\cdot }_{{W}}={\cdot }_{{A}}$
13 1 sralmod ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {A}\in \mathrm{LMod}$
14 13 adantl ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {A}\in \mathrm{LMod}$
15 crngring ${⊢}{W}\in \mathrm{CRing}\to {W}\in \mathrm{Ring}$
16 15 adantr ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {W}\in \mathrm{Ring}$
17 eqidd ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
18 2 5 sraaddg ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {+}_{{W}}={+}_{{A}}$
19 18 oveqdr ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {x}{+}_{{W}}{y}={x}{+}_{{A}}{y}$
20 12 oveqdr ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {x}{\cdot }_{{W}}{y}={x}{\cdot }_{{A}}{y}$
21 17 6 19 20 ringpropd ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to \left({W}\in \mathrm{Ring}↔{A}\in \mathrm{Ring}\right)$
22 16 21 mpbid ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {A}\in \mathrm{Ring}$
23 8 subrgcrng ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {W}{↾}_{𝑠}{S}\in \mathrm{CRing}$
24 16 adantr ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {W}\in \mathrm{Ring}$
25 5 adantr ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {S}\subseteq {\mathrm{Base}}_{{W}}$
26 simpr1 ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {x}\in {S}$
27 25 26 sseldd ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {x}\in {\mathrm{Base}}_{{W}}$
28 simpr2 ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {y}\in {\mathrm{Base}}_{{W}}$
29 simpr3 ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {z}\in {\mathrm{Base}}_{{W}}$
30 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
31 3 30 ringass ${⊢}\left({W}\in \mathrm{Ring}\wedge \left({x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({x}{\cdot }_{{W}}{y}\right){\cdot }_{{W}}{z}={x}{\cdot }_{{W}}\left({y}{\cdot }_{{W}}{z}\right)$
32 24 27 28 29 31 syl13anc ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({x}{\cdot }_{{W}}{y}\right){\cdot }_{{W}}{z}={x}{\cdot }_{{W}}\left({y}{\cdot }_{{W}}{z}\right)$
33 eqid ${⊢}{\mathrm{mulGrp}}_{{W}}={\mathrm{mulGrp}}_{{W}}$
34 33 crngmgp ${⊢}{W}\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{{W}}\in \mathrm{CMnd}$
35 34 ad2antrr ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {\mathrm{mulGrp}}_{{W}}\in \mathrm{CMnd}$
36 33 3 mgpbas ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{W}}}$
37 33 30 mgpplusg ${⊢}{\cdot }_{{W}}={+}_{{\mathrm{mulGrp}}_{{W}}}$
38 36 37 cmn12 ${⊢}\left({\mathrm{mulGrp}}_{{W}}\in \mathrm{CMnd}\wedge \left({y}\in {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {y}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{z}\right)={x}{\cdot }_{{W}}\left({y}{\cdot }_{{W}}{z}\right)$
39 35 28 27 29 38 syl13anc ${⊢}\left(\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to {y}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{z}\right)={x}{\cdot }_{{W}}\left({y}{\cdot }_{{W}}{z}\right)$
40 6 7 10 11 12 14 22 23 32 39 isassad ${⊢}\left({W}\in \mathrm{CRing}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\right)\to {A}\in \mathrm{AssAlg}$