Metamath Proof Explorer

Theorem cntzsubm

Description: Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses cntzrec.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntzrec.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntzsubm ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 cntzrec.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntzrec.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3 1 2 cntzssv ⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵
4 3 a1i ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
5 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
6 1 5 mndidcl ⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
7 6 adantr ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
8 simpll ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑀 ∈ Mnd )
9 simpr ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ⊆ 𝐵 )
10 9 sselda ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
11 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
12 1 11 5 mndlid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 )
13 8 10 12 syl2anc ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 )
14 1 11 5 mndrid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = 𝑥 )
15 8 10 14 syl2anc ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = 𝑥 )
16 13 15 eqtr4d ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
17 16 ralrimiva ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
18 1 11 2 elcntz ⊢ ( 𝑆 ⊆ 𝐵 → ( ( 0g ‘ 𝑀 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) ) ) )
19 18 adantl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( ( 0g ‘ 𝑀 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) ) ) )
20 7 17 19 mpbir2and ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑍 ‘ 𝑆 ) )
21 simpll ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → 𝑀 ∈ Mnd )
22 simprl ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) )
23 3 22 sseldi ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → 𝑦 ∈ 𝐵 )
24 simprr ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) )
25 3 24 sseldi ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → 𝑧 ∈ 𝐵 )
26 1 11 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 )
27 21 23 25 26 syl3anc ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 )
28 21 adantr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑀 ∈ Mnd )
29 23 adantr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 )
30 25 adantr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑧 ∈ 𝐵 )
31 10 adantlr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
32 1 11 mndass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) )
33 28 29 30 31 32 syl13anc ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) )
34 11 2 cntzi ⊢ ( ( 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) )
35 24 34 sylan ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) )
36 35 oveq2d ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) )
37 1 11 mndass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) )
38 28 29 31 30 37 syl13anc ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) )
39 11 2 cntzi ⊢ ( ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
40 22 39 sylan ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
41 40 oveq1d ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) )
42 36 38 41 3eqtr2d ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) )
43 1 11 mndass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) )
44 28 31 29 30 43 syl13anc ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) )
45 33 42 44 3eqtrd ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) )
46 45 ralrimiva ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) )
47 1 11 2 elcntz ⊢ ( 𝑆 ⊆ 𝐵 → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) ) )
48 47 ad2antlr ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) ) )
49 27 46 48 mpbir2and ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) )
50 49 ralrimivva ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∀ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) )
51 1 5 11 issubm ⊢ ( 𝑀 ∈ Mnd → ( ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 ∧ ( 0g ‘ 𝑀 ) ∈ ( 𝑍 ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∀ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) ) ) )
52 51 adantr ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 ∧ ( 0g ‘ 𝑀 ) ∈ ( 𝑍 ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∀ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) ) ) )
53 4 20 50 52 mpbir3and ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) )