This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑀 ) 𝑧 ) ∈ 𝐶 )