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 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
sraassab.z 𝑍 = ( Cntr ‘ ( mulGrp ‘ 𝑊 ) )
sraassab.w ( 𝜑𝑊 ∈ Ring )
sraassab.s ( 𝜑𝑆 ∈ ( SubRing ‘ 𝑊 ) )
Assertion sraassab ( 𝜑 → ( 𝐴 ∈ AssAlg ↔ 𝑆𝑍 ) )

Proof

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