sraassab

Description: A subring algebra is an associative algebra if and only if the subring is included in the ring's center. (Contributed by SN, 21-Mar-2025)

	Ref	Expression
Hypotheses	sraassab.a	$⊢ A = subringAlg (W) (S)$
	sraassab.z	$⊢ Z = Cntr ({mulGrp}_{W})$
	sraassab.w	$⊢ φ \to W \in Ring$
	sraassab.s	$⊢ φ \to S \in SubRing (W)$
Assertion	sraassab	$⊢ φ \to (A \in AssAlg \leftrightarrow S \subseteq Z)$

Proof

Step	Hyp	Ref	Expression
1		sraassab.a	$⊢ A = subringAlg (W) (S)$
2		sraassab.z	$⊢ Z = Cntr ({mulGrp}_{W})$
3		sraassab.w	$⊢ φ \to W \in Ring$
4		sraassab.s	$⊢ φ \to S \in SubRing (W)$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6	5	subrgss	$⊢ S \in SubRing (W) \to S \subseteq {Base}_{W}$
7	4 6	syl	$⊢ φ \to S \subseteq {Base}_{W}$
8	7	adantr	$⊢ (φ \land A \in AssAlg) \to S \subseteq {Base}_{W}$
9	8	sselda	$⊢ ((φ \land A \in AssAlg) \land y \in S) \to y \in {Base}_{W}$
10		simpllr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to A \in AssAlg$
11		eqid	$⊢ W ↾_{𝑠} S = W ↾_{𝑠} S$
12	11	subrgbas	$⊢ S \in SubRing (W) \to S = {Base}_{(W ↾_{𝑠} S)}$
13	4 12	syl	$⊢ φ \to S = {Base}_{(W ↾_{𝑠} S)}$
14	1	a1i	$⊢ φ \to A = subringAlg (W) (S)$
15	14 7	srasca	$⊢ φ \to W ↾_{𝑠} S = Scalar (A)$
16	15	fveq2d	$⊢ φ \to {Base}_{(W ↾_{𝑠} S)} = {Base}_{Scalar (A)}$
17	13 16	eqtrd	$⊢ φ \to S = {Base}_{Scalar (A)}$
18	17	eqimssd	$⊢ φ \to S \subseteq {Base}_{Scalar (A)}$
19	18	sselda	$⊢ (φ \land y \in S) \to y \in {Base}_{Scalar (A)}$
20	19	ad4ant13	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \in {Base}_{Scalar (A)}$
21	14 7	srabase	$⊢ φ \to {Base}_{W} = {Base}_{A}$
22	21	eqimssd	$⊢ φ \to {Base}_{W} \subseteq {Base}_{A}$
23	22	ad2antrr	$⊢ ((φ \land A \in AssAlg) \land y \in S) \to {Base}_{W} \subseteq {Base}_{A}$
24	23	sselda	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \in {Base}_{A}$
25		eqid	$⊢ 1_{W} = 1_{W}$
26	5 25	ringidcl	$⊢ W \in Ring \to 1_{W} \in {Base}_{W}$
27	3 26	syl	$⊢ φ \to 1_{W} \in {Base}_{W}$
28	27 21	eleqtrd	$⊢ φ \to 1_{W} \in {Base}_{A}$
29	28	ad3antrrr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to 1_{W} \in {Base}_{A}$
30		eqid	$⊢ {Base}_{A} = {Base}_{A}$
31		eqid	$⊢ Scalar (A) = Scalar (A)$
32		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
33		eqid	$⊢ \cdot_{A} = \cdot_{A}$
34		eqid	$⊢ \cdot_{A} = \cdot_{A}$
35	30 31 32 33 34	assaassr	$⊢ (A \in AssAlg \land (y \in {Base}_{Scalar (A)} \land x \in {Base}_{A} \land 1_{W} \in {Base}_{A})) \to x \cdot_{A} (y \cdot_{A} 1_{W}) = y \cdot_{A} (x \cdot_{A} 1_{W})$
36	10 20 24 29 35	syl13anc	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{A} (y \cdot_{A} 1_{W}) = y \cdot_{A} (x \cdot_{A} 1_{W})$
37	14 7	sramulr	$⊢ φ \to \cdot_{W} = \cdot_{A}$
38	37	ad3antrrr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to \cdot_{W} = \cdot_{A}$
39	38	oveqd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{W} (y \cdot_{A} 1_{W}) = x \cdot_{A} (y \cdot_{A} 1_{W})$
40	14 7	sravsca	$⊢ φ \to \cdot_{W} = \cdot_{A}$
41	40	ad3antrrr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to \cdot_{W} = \cdot_{A}$
42	41	oveqd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{W} 1_{W} = y \cdot_{A} 1_{W}$
43		eqid	$⊢ \cdot_{W} = \cdot_{W}$
44	3	ad3antrrr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to W \in Ring$
45	9	adantr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \in {Base}_{W}$
46	5 43 25 44 45	ringridmd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{W} 1_{W} = y$
47	42 46	eqtr3d	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{A} 1_{W} = y$
48	47	oveq2d	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{W} (y \cdot_{A} 1_{W}) = x \cdot_{W} y$
49	39 48	eqtr3d	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{A} (y \cdot_{A} 1_{W}) = x \cdot_{W} y$
50	41	oveqd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{W} (x \cdot_{A} 1_{W}) = y \cdot_{A} (x \cdot_{A} 1_{W})$
51	38	oveqd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{W} 1_{W} = x \cdot_{A} 1_{W}$
52		simpr	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \in {Base}_{W}$
53	5 43 25 44 52	ringridmd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{W} 1_{W} = x$
54	51 53	eqtr3d	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to x \cdot_{A} 1_{W} = x$
55	54	oveq2d	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{W} (x \cdot_{A} 1_{W}) = y \cdot_{W} x$
56	50 55	eqtr3d	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{A} (x \cdot_{A} 1_{W}) = y \cdot_{W} x$
57	36 49 56	3eqtr3rd	$⊢ (((φ \land A \in AssAlg) \land y \in S) \land x \in {Base}_{W}) \to y \cdot_{W} x = x \cdot_{W} y$
58	57	ralrimiva	$⊢ ((φ \land A \in AssAlg) \land y \in S) \to \forall x \in {Base}_{W} y \cdot_{W} x = x \cdot_{W} y$
59		eqid	$⊢ {mulGrp}_{W} = {mulGrp}_{W}$
60	59 5	mgpbas	$⊢ {Base}_{W} = {Base}_{{mulGrp}_{W}}$
61	59 43	mgpplusg	$⊢ \cdot_{W} = +_{{mulGrp}_{W}}$
62	60 61 2	elcntr	$⊢ y \in Z \leftrightarrow (y \in {Base}_{W} \land \forall x \in {Base}_{W} y \cdot_{W} x = x \cdot_{W} y)$
63	9 58 62	sylanbrc	$⊢ ((φ \land A \in AssAlg) \land y \in S) \to y \in Z$
64	63	ex	$⊢ (φ \land A \in AssAlg) \to (y \in S \to y \in Z)$
65	64	ssrdv	$⊢ (φ \land A \in AssAlg) \to S \subseteq Z$
66	21	adantr	$⊢ (φ \land S \subseteq Z) \to {Base}_{W} = {Base}_{A}$
67	15	adantr	$⊢ (φ \land S \subseteq Z) \to W ↾_{𝑠} S = Scalar (A)$
68	13	adantr	$⊢ (φ \land S \subseteq Z) \to S = {Base}_{(W ↾_{𝑠} S)}$
69	40	adantr	$⊢ (φ \land S \subseteq Z) \to \cdot_{W} = \cdot_{A}$
70	37	adantr	$⊢ (φ \land S \subseteq Z) \to \cdot_{W} = \cdot_{A}$
71	1	sralmod	$⊢ S \in SubRing (W) \to A \in LMod$
72	4 71	syl	$⊢ φ \to A \in LMod$
73	72	adantr	$⊢ (φ \land S \subseteq Z) \to A \in LMod$
74	1 5	sraring	$⊢ (W \in Ring \land S \subseteq {Base}_{W}) \to A \in Ring$
75	3 7 74	syl2anc	$⊢ φ \to A \in Ring$
76	75	adantr	$⊢ (φ \land S \subseteq Z) \to A \in Ring$
77	3	ad2antrr	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to W \in Ring$
78	7	adantr	$⊢ (φ \land S \subseteq Z) \to S \subseteq {Base}_{W}$
79	78	sselda	$⊢ ((φ \land S \subseteq Z) \land x \in S) \to x \in {Base}_{W}$
80	79	3ad2antr1	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \in {Base}_{W}$
81		simpr2	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to y \in {Base}_{W}$
82		simpr3	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to z \in {Base}_{W}$
83	5 43 77 80 81 82	ringassd	$⊢ ((φ \land S \subseteq Z) \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)$
84		ssel2	$⊢ (S \subseteq Z \land x \in S) \to x \in Z$
85	84	ad2ant2lr	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W})) \to x \in Z$
86		simprr	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W})) \to y \in {Base}_{W}$
87	60 61 2	cntri	$⊢ (x \in Z \land y \in {Base}_{W}) \to x \cdot_{W} y = y \cdot_{W} x$
88	85 86 87	syl2anc	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W})) \to x \cdot_{W} y = y \cdot_{W} x$
89	88	3adantr3	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \cdot_{W} y = y \cdot_{W} x$
90	89	oveq1d	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x \cdot_{W} y) \cdot_{W} z = (y \cdot_{W} x) \cdot_{W} z$
91	5 43 77 81 80 82	ringassd	$⊢ ((φ \land S \subseteq Z) \land (x \in S \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (y \cdot_{W} x) \cdot_{W} z = y \cdot_{W} (x \cdot_{W} z)$
92	90 83 91	3eqtr3rd	$⊢ ((φ \land S \subseteq Z) \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)$
93	66 67 68 69 70 73 76 83 92	isassad	$⊢ (φ \land S \subseteq Z) \to A \in AssAlg$
94	65 93	impbida	$⊢ φ \to (A \in AssAlg \leftrightarrow S \subseteq Z)$

Metamath Proof Explorer

Theorem sraassab

Proof