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 = subringAlg (W) (S)$
	Assertion	sraassa	$⊢ (W \in CRing \land S \in SubRing (W)) \to A \in AssAlg$

Proof

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

Metamath Proof Explorer

Theorem sraassa

Proof