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 ) )