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

Metamath Proof Explorer

Theorem cntzmhm

Description: Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cntzmhm.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
cntzmhm.y ⊢ 𝑌 = ( Cntz ‘ 𝐻 )
Assertion cntzmhm ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 cntzmhm.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2 cntzmhm.y ⊢ 𝑌 = ( Cntz ‘ 𝐻 )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5 3 4 mhmf ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
6 3 1 cntzssv ⊢ ( 𝑍 ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 )
7 6 sseli ⊢ ( 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
8 ffvelcdm ⊢ ( ( 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝐻 ) )
9 5 7 8 syl2an ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝐻 ) )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 10 1 cntzi ⊢ ( ( 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝐴 ) )
12 11 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝐴 ) )
13 12 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ‘ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝐴 ) ) )
14 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) )
15 7 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
16 3 1 cntzrcl ⊢ ( 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝐺 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) )
17 16 adantl ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐺 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) )
18 17 simprd ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
19 18 sselda ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
20 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
21 3 10 20 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
22 14 15 19 21 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ‘ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
23 3 10 20 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝐴 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) )
24 14 19 15 23 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝐴 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) )
25 13 22 24 3eqtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) )
26 25 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) )
27 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
28 27 ffnd ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝐹 Fn ( Base ‘ 𝐺 ) )
29 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
30 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) )
31 29 30 eqeq12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ) )
32 31 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ) )
33 28 18 32 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ) )
34 26 33 mpbird ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ∀ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) )
35 imassrn ⊢ ( 𝐹 “ 𝑆 ) ⊆ ran 𝐹
36 27 frnd ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝐻 ) )
37 35 36 sstrid ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐹 “ 𝑆 ) ⊆ ( Base ‘ 𝐻 ) )
38 4 20 2 elcntz ⊢ ( ( 𝐹 “ 𝑆 ) ⊆ ( Base ‘ 𝐻 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑆 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ) ) )
39 37 38 syl ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑆 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ( ( 𝐹 ‘ 𝐴 ) ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝐴 ) ) ) ) )
40 9 34 39 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝐴 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑆 ) ) )