Metamath Proof Explorer

Theorem cntzsgrpcl

Description: Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025)

Ref Expression
Hypotheses cntzsgrpcl.b 
|- B = ( Base ` M )
cntzsgrpcl.z 
|- Z = ( Cntz ` M )
cntzsgrpcl.c 
|- C = ( Z ` S )
Assertion cntzsgrpcl 
|- ( ( M e. Smgrp /\ S C_ B ) -> A. y e. C A. z e. C ( y ( +g ` M ) z ) e. C )

Proof

Step Hyp Ref Expression
1 cntzsgrpcl.b 
 |-  B = ( Base ` M )
2 cntzsgrpcl.z 
 |-  Z = ( Cntz ` M )
3 cntzsgrpcl.c 
 |-  C = ( Z ` S )
4 simpll 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> M e. Smgrp )
5 1 2 cntzssv 
 |-  ( Z ` S ) C_ B
6 3 5 eqsstri 
 |-  C C_ B
7 simprl 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> y e. C )
8 6 7 sselid 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> y e. B )
9 simprr 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> z e. C )
10 6 9 sselid 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> z e. B )
11 eqid 
 |-  ( +g ` M ) = ( +g ` M )
12 1 11 sgrpcl 
 |-  ( ( M e. Smgrp /\ y e. B /\ z e. B ) -> ( y ( +g ` M ) z ) e. B )
13 4 8 10 12 syl3anc 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> ( y ( +g ` M ) z ) e. B )
14 4 adantr 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> M e. Smgrp )
15 8 adantr 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> y e. B )
16 10 adantr 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> z e. B )
17 simpr 
 |-  ( ( M e. Smgrp /\ S C_ B ) -> S C_ B )
18 17 sselda 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ x e. S ) -> x e. B )
19 18 adantlr 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> x e. B )
20 1 11 sgrpass 
 |-  ( ( M e. Smgrp /\ ( y e. B /\ z e. B /\ x e. B ) ) -> ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( y ( +g ` M ) ( z ( +g ` M ) x ) ) )
21 14 15 16 19 20 syl13anc 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( y ( +g ` M ) ( z ( +g ` M ) x ) ) )
22 3 eleq2i 
 |-  ( z e. C <-> z e. ( Z ` S ) )
23 11 2 cntzi 
 |-  ( ( z e. ( Z ` S ) /\ x e. S ) -> ( z ( +g ` M ) x ) = ( x ( +g ` M ) z ) )
24 22 23 sylanb 
 |-  ( ( z e. C /\ x e. S ) -> ( z ( +g ` M ) x ) = ( x ( +g ` M ) z ) )
25 9 24 sylan 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( z ( +g ` M ) x ) = ( x ( +g ` M ) z ) )
26 25 oveq2d 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( y ( +g ` M ) ( z ( +g ` M ) x ) ) = ( y ( +g ` M ) ( x ( +g ` M ) z ) ) )
27 1 11 sgrpass 
 |-  ( ( M e. Smgrp /\ ( y e. B /\ x e. B /\ z e. B ) ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) z ) = ( y ( +g ` M ) ( x ( +g ` M ) z ) ) )
28 14 15 19 16 27 syl13anc 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) z ) = ( y ( +g ` M ) ( x ( +g ` M ) z ) ) )
29 3 eleq2i 
 |-  ( y e. C <-> y e. ( Z ` S ) )
30 11 2 cntzi 
 |-  ( ( y e. ( Z ` S ) /\ x e. S ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
31 29 30 sylanb 
 |-  ( ( y e. C /\ x e. S ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
32 7 31 sylan 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
33 32 oveq1d 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) z ) = ( ( x ( +g ` M ) y ) ( +g ` M ) z ) )
34 26 28 33 3eqtr2d 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( y ( +g ` M ) ( z ( +g ` M ) x ) ) = ( ( x ( +g ` M ) y ) ( +g ` M ) z ) )
35 1 11 sgrpass 
 |-  ( ( M e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
36 14 19 15 16 35 syl13anc 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
37 21 34 36 3eqtrd 
 |-  ( ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) /\ x e. S ) -> ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
38 37 ralrimiva 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
39 3 eleq2i 
 |-  ( ( y ( +g ` M ) z ) e. C <-> ( y ( +g ` M ) z ) e. ( Z ` S ) )
40 1 11 2 elcntz 
 |-  ( S C_ B -> ( ( y ( +g ` M ) z ) e. ( Z ` S ) <-> ( ( y ( +g ` M ) z ) e. B /\ A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) )
41 39 40 bitrid 
 |-  ( S C_ B -> ( ( y ( +g ` M ) z ) e. C <-> ( ( y ( +g ` M ) z ) e. B /\ A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) )
42 41 ad2antlr 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> ( ( y ( +g ` M ) z ) e. C <-> ( ( y ( +g ` M ) z ) e. B /\ A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) )
43 13 38 42 mpbir2and 
 |-  ( ( ( M e. Smgrp /\ S C_ B ) /\ ( y e. C /\ z e. C ) ) -> ( y ( +g ` M ) z ) e. C )
44 43 ralrimivva 
 |-  ( ( M e. Smgrp /\ S C_ B ) -> A. y e. C A. z e. C ( y ( +g ` M ) z ) e. C )