Metamath Proof Explorer

Theorem imasmhm

Description: Given a function F with homomorphic properties, build the image of a monoid. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses imasmhm.b ⊢ B = Base W
imasmhm.f ⊢ φ → F : B ⟶ C
imasmhm.1 ⊢ + ˙ = + W
imasmhm.2 ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ p ∈ B ∧ q ∈ B → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a + ˙ b = F ⁡ p + ˙ q
imasmhm.w ⊢ φ → W ∈ Mnd
Assertion imasmhm ⊢ φ → F “ 𝑠 W ∈ Mnd ∧ F ∈ W MndHom F “ 𝑠 W

Proof

Step Hyp Ref Expression
1 imasmhm.b ⊢ B = Base W
2 imasmhm.f ⊢ φ → F : B ⟶ C
3 imasmhm.1 ⊢ + ˙ = + W
4 imasmhm.2 ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ p ∈ B ∧ q ∈ B → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a + ˙ b = F ⁡ p + ˙ q
5 imasmhm.w ⊢ φ → W ∈ Mnd
6 eqidd ⊢ φ → F “ 𝑠 W = F “ 𝑠 W
7 1 a1i ⊢ φ → B = Base W
8 fimadmfo ⊢ F : B ⟶ C → F : B ⟶ onto F B
9 2 8 syl ⊢ φ → F : B ⟶ onto F B
10 eqid ⊢ 0 W = 0 W
11 6 7 3 9 4 5 10 imasmnd ⊢ φ → F “ 𝑠 W ∈ Mnd ∧ F ⁡ 0 W = 0 F “ 𝑠 W
12 11 simpld ⊢ φ → F “ 𝑠 W ∈ Mnd
13 eqid ⊢ Base F “ 𝑠 W = Base F “ 𝑠 W
14 eqid ⊢ + F “ 𝑠 W = + F “ 𝑠 W
15 eqid ⊢ 0 F “ 𝑠 W = 0 F “ 𝑠 W
16 fof ⊢ F : B ⟶ onto F B → F : B ⟶ F B
17 9 16 syl ⊢ φ → F : B ⟶ F B
18 6 7 9 5 imasbas ⊢ φ → F B = Base F “ 𝑠 W
19 18 feq3d ⊢ φ → F : B ⟶ F B ↔ F : B ⟶ Base F “ 𝑠 W
20 17 19 mpbid ⊢ φ → F : B ⟶ Base F “ 𝑠 W
21 9 4 6 7 5 3 14 imasaddval ⊢ φ ∧ x ∈ B ∧ y ∈ B → F ⁡ x + F “ 𝑠 W F ⁡ y = F ⁡ x + ˙ y
22 21 3expb ⊢ φ ∧ x ∈ B ∧ y ∈ B → F ⁡ x + F “ 𝑠 W F ⁡ y = F ⁡ x + ˙ y
23 22 eqcomd ⊢ φ ∧ x ∈ B ∧ y ∈ B → F ⁡ x + ˙ y = F ⁡ x + F “ 𝑠 W F ⁡ y
24 11 simprd ⊢ φ → F ⁡ 0 W = 0 F “ 𝑠 W
25 1 13 3 14 10 15 5 12 20 23 24 ismhmd ⊢ φ → F ∈ W MndHom F “ 𝑠 W
26 12 25 jca ⊢ φ → F “ 𝑠 W ∈ Mnd ∧ F ∈ W MndHom F “ 𝑠 W