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 \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	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$
24	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}$
25		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$
26	24 25	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}$
27		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}$
28		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}$
29		eqid	$⊢ \cdot_{W} = \cdot_{W}$
30	3 29	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)$
31	23 26 27 28 30	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)$
32		eqid	$⊢ {mulGrp}_{W} = {mulGrp}_{W}$
33	32	crngmgp	$⊢ W \in CRing \to {mulGrp}_{W} \in CMnd$
34	33	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$
35	32 3	mgpbas	$⊢ {Base}_{W} = {Base}_{{mulGrp}_{W}}$
36	32 29	mgpplusg	$⊢ \cdot_{W} = +_{{mulGrp}_{W}}$
37	35 36	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)$
38	34 27 26 28 37	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)$
39	6 7 10 11 12 14 22 31 38	isassad	$⊢ (W \in CRing \land S \in SubRing (W)) \to A \in AssAlg$

Metamath Proof Explorer

Theorem sraassaOLD

Proof