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
|- ( ph -> W e. Ring )
sraassab.s
|- ( ph -> S e. ( SubRing ` W ) )
Assertion sraassab
|- ( ph -> ( A e. AssAlg <-> S C_ Z ) )

Proof

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