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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
imasmhm.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
imasmhm.1 ⊢ + = ( +g ‘ 𝑊 )
imasmhm.2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasmhm.w ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
Assertion imasmhm ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ Mnd ∧ 𝐹 ∈ ( 𝑊 MndHom ( 𝐹 “s 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 imasmhm.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 imasmhm.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
3 imasmhm.1 ⊢ + = ( +g ‘ 𝑊 )
4 imasmhm.2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
5 imasmhm.w ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
6 eqidd ⊢ ( 𝜑 → ( 𝐹 “s 𝑊 ) = ( 𝐹 “s 𝑊 ) )
7 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑊 ) )
8 fimadmfo ⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 → 𝐹 : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) )
9 2 8 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) )
10 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
11 6 7 3 9 4 5 10 imasmnd ⊢ ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ Mnd ∧ ( 𝐹 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ ( 𝐹 “s 𝑊 ) ) ) )
12 11 simpld ⊢ ( 𝜑 → ( 𝐹 “s 𝑊 ) ∈ Mnd )
13 eqid ⊢ ( Base ‘ ( 𝐹 “s 𝑊 ) ) = ( Base ‘ ( 𝐹 “s 𝑊 ) )
14 eqid ⊢ ( +g ‘ ( 𝐹 “s 𝑊 ) ) = ( +g ‘ ( 𝐹 “s 𝑊 ) )
15 eqid ⊢ ( 0g ‘ ( 𝐹 “s 𝑊 ) ) = ( 0g ‘ ( 𝐹 “s 𝑊 ) )
16 fof ⊢ ( 𝐹 : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) → 𝐹 : 𝐵 ⟶ ( 𝐹 “ 𝐵 ) )
17 9 16 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 𝐹 “ 𝐵 ) )
18 6 7 9 5 imasbas ⊢ ( 𝜑 → ( 𝐹 “ 𝐵 ) = ( Base ‘ ( 𝐹 “s 𝑊 ) ) )
19 18 feq3d ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( 𝐹 “ 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ ( Base ‘ ( 𝐹 “s 𝑊 ) ) ) )
20 17 19 mpbid ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ ( 𝐹 “s 𝑊 ) ) )
21 9 4 6 7 5 3 14 imasaddval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝐹 “s 𝑊 ) ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
22 21 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝐹 “s 𝑊 ) ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
23 22 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝐹 “s 𝑊 ) ) ( 𝐹 ‘ 𝑦 ) ) )
24 11 simprd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ ( 𝐹 “s 𝑊 ) ) )
25 1 13 3 14 10 15 5 12 20 23 24 ismhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑊 MndHom ( 𝐹 “s 𝑊 ) ) )
26 12 25 jca ⊢ ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ Mnd ∧ 𝐹 ∈ ( 𝑊 MndHom ( 𝐹 “s 𝑊 ) ) ) )