Metamath Proof Explorer

Theorem imasrhm

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

Ref Expression
Hypotheses imasmhm.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
imasmhm.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
imasmhm.1 ⊢ + = ( +g ‘ 𝑊 )
imasmhm.2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasrhm.3 ⊢ · = ( .r ‘ 𝑊 )
imasrhm.4 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasrhm.w ⊢ ( 𝜑 → 𝑊 ∈ Ring )
Assertion imasrhm ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ Ring ∧ 𝐹 ∈ ( 𝑊 RingHom ( 𝐹 “s 𝑊 ) ) ) )

Proof

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