Metamath Proof Explorer


Theorem 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 φ W Ring
sraassab.s φ S SubRing W
Assertion sraassab φ A AssAlg S Z

Proof

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