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 ⊢ Z = Cntz ⁡ G
cntzmhm.y ⊢ Y = Cntz ⁡ H
Assertion cntzmhm ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F ⁡ A ∈ Y ⁡ F S

Proof

Step Hyp Ref Expression
1 cntzmhm.z ⊢ Z = Cntz ⁡ G
2 cntzmhm.y ⊢ Y = Cntz ⁡ H
3 eqid ⊢ Base G = Base G
4 eqid ⊢ Base H = Base H
5 3 4 mhmf ⊢ F ∈ G MndHom H → F : Base G ⟶ Base H
6 3 1 cntzssv ⊢ Z ⁡ S ⊆ Base G
7 6 sseli ⊢ A ∈ Z ⁡ S → A ∈ Base G
8 ffvelrn ⊢ F : Base G ⟶ Base H ∧ A ∈ Base G → F ⁡ A ∈ Base H
9 5 7 8 syl2an ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F ⁡ A ∈ Base H
10 eqid ⊢ + G = + G
11 10 1 cntzi ⊢ A ∈ Z ⁡ S ∧ x ∈ S → A + G x = x + G A
12 11 adantll ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → A + G x = x + G A
13 12 fveq2d ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → F ⁡ A + G x = F ⁡ x + G A
14 simpll ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → F ∈ G MndHom H
15 7 ad2antlr ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → A ∈ Base G
16 3 1 cntzrcl ⊢ A ∈ Z ⁡ S → G ∈ V ∧ S ⊆ Base G
17 16 adantl ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → G ∈ V ∧ S ⊆ Base G
18 17 simprd ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → S ⊆ Base G
19 18 sselda ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → x ∈ Base G
20 eqid ⊢ + H = + H
21 3 10 20 mhmlin ⊢ F ∈ G MndHom H ∧ A ∈ Base G ∧ x ∈ Base G → F ⁡ A + G x = F ⁡ A + H F ⁡ x
22 14 15 19 21 syl3anc ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → F ⁡ A + G x = F ⁡ A + H F ⁡ x
23 3 10 20 mhmlin ⊢ F ∈ G MndHom H ∧ x ∈ Base G ∧ A ∈ Base G → F ⁡ x + G A = F ⁡ x + H F ⁡ A
24 14 19 15 23 syl3anc ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → F ⁡ x + G A = F ⁡ x + H F ⁡ A
25 13 22 24 3eqtr3d ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S ∧ x ∈ S → F ⁡ A + H F ⁡ x = F ⁡ x + H F ⁡ A
26 25 ralrimiva ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → ∀ x ∈ S F ⁡ A + H F ⁡ x = F ⁡ x + H F ⁡ A
27 5 adantr ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F : Base G ⟶ Base H
28 27 ffnd ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F Fn Base G
29 oveq2 ⊢ y = F ⁡ x → F ⁡ A + H y = F ⁡ A + H F ⁡ x
30 oveq1 ⊢ y = F ⁡ x → y + H F ⁡ A = F ⁡ x + H F ⁡ A
31 29 30 eqeq12d ⊢ y = F ⁡ x → F ⁡ A + H y = y + H F ⁡ A ↔ F ⁡ A + H F ⁡ x = F ⁡ x + H F ⁡ A
32 31 ralima ⊢ F Fn Base G ∧ S ⊆ Base G → ∀ y ∈ F S F ⁡ A + H y = y + H F ⁡ A ↔ ∀ x ∈ S F ⁡ A + H F ⁡ x = F ⁡ x + H F ⁡ A
33 28 18 32 syl2anc ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → ∀ y ∈ F S F ⁡ A + H y = y + H F ⁡ A ↔ ∀ x ∈ S F ⁡ A + H F ⁡ x = F ⁡ x + H F ⁡ A
34 26 33 mpbird ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → ∀ y ∈ F S F ⁡ A + H y = y + H F ⁡ A
35 imassrn ⊢ F S ⊆ ran ⁡ F
36 27 frnd ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → ran ⁡ F ⊆ Base H
37 35 36 sstrid ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F S ⊆ Base H
38 4 20 2 elcntz ⊢ F S ⊆ Base H → F ⁡ A ∈ Y ⁡ F S ↔ F ⁡ A ∈ Base H ∧ ∀ y ∈ F S F ⁡ A + H y = y + H F ⁡ A
39 37 38 syl ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F ⁡ A ∈ Y ⁡ F S ↔ F ⁡ A ∈ Base H ∧ ∀ y ∈ F S F ⁡ A + H y = y + H F ⁡ A
40 9 34 39 mpbir2and ⊢ F ∈ G MndHom H ∧ A ∈ Z ⁡ S → F ⁡ A ∈ Y ⁡ F S