Metamath Proof Explorer


Theorem cntzsgrpcl

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

Ref Expression
Hypotheses cntzsgrpcl.b 𝐵 = ( Base ‘ 𝑀 )
cntzsgrpcl.z 𝑍 = ( Cntz ‘ 𝑀 )
cntzsgrpcl.c 𝐶 = ( 𝑍𝑆 )
Assertion cntzsgrpcl ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) → ∀ 𝑦𝐶𝑧𝐶 ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 cntzsgrpcl.b 𝐵 = ( Base ‘ 𝑀 )
2 cntzsgrpcl.z 𝑍 = ( Cntz ‘ 𝑀 )
3 cntzsgrpcl.c 𝐶 = ( 𝑍𝑆 )
4 simpll ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → 𝑀 ∈ Smgrp )
5 1 2 cntzssv ( 𝑍𝑆 ) ⊆ 𝐵
6 3 5 eqsstri 𝐶𝐵
7 simprl ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → 𝑦𝐶 )
8 6 7 sselid ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → 𝑦𝐵 )
9 simprr ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → 𝑧𝐶 )
10 6 9 sselid ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → 𝑧𝐵 )
11 eqid ( +g𝑀 ) = ( +g𝑀 )
12 1 11 sgrpcl ( ( 𝑀 ∈ Smgrp ∧ 𝑦𝐵𝑧𝐵 ) → ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐵 )
13 4 8 10 12 syl3anc ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐵 )
14 4 adantr ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → 𝑀 ∈ Smgrp )
15 8 adantr ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → 𝑦𝐵 )
16 10 adantr ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → 𝑧𝐵 )
17 simpr ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) → 𝑆𝐵 )
18 17 sselda ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ 𝑥𝑆 ) → 𝑥𝐵 )
19 18 adantlr ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → 𝑥𝐵 )
20 1 11 sgrpass ( ( 𝑀 ∈ Smgrp ∧ ( 𝑦𝐵𝑧𝐵𝑥𝐵 ) ) → ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑦 ( +g𝑀 ) ( 𝑧 ( +g𝑀 ) 𝑥 ) ) )
21 14 15 16 19 20 syl13anc ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑦 ( +g𝑀 ) ( 𝑧 ( +g𝑀 ) 𝑥 ) ) )
22 3 eleq2i ( 𝑧𝐶𝑧 ∈ ( 𝑍𝑆 ) )
23 11 2 cntzi ( ( 𝑧 ∈ ( 𝑍𝑆 ) ∧ 𝑥𝑆 ) → ( 𝑧 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑧 ) )
24 22 23 sylanb ( ( 𝑧𝐶𝑥𝑆 ) → ( 𝑧 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑧 ) )
25 9 24 sylan ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( 𝑧 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑧 ) )
26 25 oveq2d ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( 𝑦 ( +g𝑀 ) ( 𝑧 ( +g𝑀 ) 𝑥 ) ) = ( 𝑦 ( +g𝑀 ) ( 𝑥 ( +g𝑀 ) 𝑧 ) ) )
27 1 11 sgrpass ( ( 𝑀 ∈ Smgrp ∧ ( 𝑦𝐵𝑥𝐵𝑧𝐵 ) ) → ( ( 𝑦 ( +g𝑀 ) 𝑥 ) ( +g𝑀 ) 𝑧 ) = ( 𝑦 ( +g𝑀 ) ( 𝑥 ( +g𝑀 ) 𝑧 ) ) )
28 14 15 19 16 27 syl13anc ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( ( 𝑦 ( +g𝑀 ) 𝑥 ) ( +g𝑀 ) 𝑧 ) = ( 𝑦 ( +g𝑀 ) ( 𝑥 ( +g𝑀 ) 𝑧 ) ) )
29 3 eleq2i ( 𝑦𝐶𝑦 ∈ ( 𝑍𝑆 ) )
30 11 2 cntzi ( ( 𝑦 ∈ ( 𝑍𝑆 ) ∧ 𝑥𝑆 ) → ( 𝑦 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
31 29 30 sylanb ( ( 𝑦𝐶𝑥𝑆 ) → ( 𝑦 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
32 7 31 sylan ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( 𝑦 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
33 32 oveq1d ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( ( 𝑦 ( +g𝑀 ) 𝑥 ) ( +g𝑀 ) 𝑧 ) = ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( +g𝑀 ) 𝑧 ) )
34 26 28 33 3eqtr2d ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( 𝑦 ( +g𝑀 ) ( 𝑧 ( +g𝑀 ) 𝑥 ) ) = ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( +g𝑀 ) 𝑧 ) )
35 1 11 sgrpass ( ( 𝑀 ∈ Smgrp ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) )
36 14 19 15 16 35 syl13anc ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) )
37 21 34 36 3eqtrd ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) ∧ 𝑥𝑆 ) → ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) )
38 37 ralrimiva ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → ∀ 𝑥𝑆 ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) )
39 3 eleq2i ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐶 ↔ ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ ( 𝑍𝑆 ) )
40 1 11 2 elcntz ( 𝑆𝐵 → ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ ( 𝑍𝑆 ) ↔ ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥𝑆 ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) ) ) )
41 39 40 bitrid ( 𝑆𝐵 → ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐶 ↔ ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥𝑆 ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) ) ) )
42 41 ad2antlr ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐶 ↔ ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥𝑆 ( ( 𝑦 ( +g𝑀 ) 𝑧 ) ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) ) ) )
43 13 38 42 mpbir2and ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) ∧ ( 𝑦𝐶𝑧𝐶 ) ) → ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐶 )
44 43 ralrimivva ( ( 𝑀 ∈ Smgrp ∧ 𝑆𝐵 ) → ∀ 𝑦𝐶𝑧𝐶 ( 𝑦 ( +g𝑀 ) 𝑧 ) ∈ 𝐶 )