Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cntzsubm Structured version   Unicode version

Theorem cntzsubm 16697
 Description: Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
Hypotheses
Ref Expression
cntzrec.b
cntzrec.z Cntz
Assertion
Ref Expression
cntzsubm SubMnd

Proof of Theorem cntzsubm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cntzrec.b . . . 4
2 cntzrec.z . . . 4 Cntz
31, 2cntzssv 16690 . . 3
43a1i 11 . 2
5 eqid 2402 . . . . 5
61, 5mndidcl 16262 . . . 4
8 simpll 752 . . . . . 6
9 simpr 459 . . . . . . 7
109sselda 3442 . . . . . 6
11 eqid 2402 . . . . . . 7
121, 11, 5mndlid 16265 . . . . . 6
138, 10, 12syl2anc 659 . . . . 5
141, 11, 5mndrid 16266 . . . . . 6
158, 10, 14syl2anc 659 . . . . 5
1613, 15eqtr4d 2446 . . . 4
1716ralrimiva 2818 . . 3
181, 11, 2elcntz 16684 . . . 4
207, 17, 19mpbir2and 923 . 2
21 simpll 752 . . . . 5
22 simprl 756 . . . . . 6
233, 22sseldi 3440 . . . . 5
24 simprr 758 . . . . . 6
253, 24sseldi 3440 . . . . 5
261, 11mndcl 16253 . . . . 5
2721, 23, 25, 26syl3anc 1230 . . . 4
2821adantr 463 . . . . . . 7
2923adantr 463 . . . . . . 7
3025adantr 463 . . . . . . 7
3110adantlr 713 . . . . . . 7
321, 11mndass 16254 . . . . . . 7
3328, 29, 30, 31, 32syl13anc 1232 . . . . . 6
3411, 2cntzi 16691 . . . . . . . . 9
3524, 34sylan 469 . . . . . . . 8
3635oveq2d 6294 . . . . . . 7
371, 11mndass 16254 . . . . . . . 8
3828, 29, 31, 30, 37syl13anc 1232 . . . . . . 7
3911, 2cntzi 16691 . . . . . . . . 9
4022, 39sylan 469 . . . . . . . 8
4140oveq1d 6293 . . . . . . 7
4236, 38, 413eqtr2d 2449 . . . . . 6
431, 11mndass 16254 . . . . . . 7
4428, 31, 29, 30, 43syl13anc 1232 . . . . . 6
4533, 42, 443eqtrd 2447 . . . . 5
4645ralrimiva 2818 . . . 4
471, 11, 2elcntz 16684 . . . . 5
4847ad2antlr 725 . . . 4
4927, 46, 48mpbir2and 923 . . 3
5049ralrimivva 2825 . 2
511, 5, 11issubm 16302 . . 3 SubMnd