Metamath Proof Explorer

Theorem imasghm

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

Ref Expression
Hypotheses imasmhm.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
imasmhm.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
imasmhm.1 ⊢ + = ( +g ‘ 𝑊 )
imasmhm.2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasghm.w ⊢ ( 𝜑 → 𝑊 ∈ Grp )
Assertion imasghm ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ Grp ∧ 𝐹 ∈ ( 𝑊 GrpHom ( 𝐹 “s 𝑊 ) ) ) )

Proof

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