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	$⊢ B = {Base}_{W}$
	imasmhm.f	$⊢ φ \to F : B ⟶ C$
	imasmhm.1	$⊢ \underset{˙}{+} = +_{W}$
	imasmhm.2	$⊢ (φ \land (a \in B \land b \in B) \land (p \in B \land q \in B)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
	imasrhm.3	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	imasrhm.4	$⊢ (φ \land (a \in B \land b \in B) \land (p \in B \land q \in B)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
	imasrhm.w	$⊢ φ \to W \in Ring$
Assertion	imasrhm	$⊢ φ \to (F “_{𝑠} W \in Ring \land F \in (W RingHom (F “_{𝑠} W)))$

Proof

Step	Hyp	Ref	Expression
1		imasmhm.b	$⊢ B = {Base}_{W}$
2		imasmhm.f	$⊢ φ \to F : B ⟶ C$
3		imasmhm.1	$⊢ \underset{˙}{+} = +_{W}$
4		imasmhm.2	$⊢ (φ \land (a \in B \land b \in B) \land (p \in B \land q \in B)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
5		imasrhm.3	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		imasrhm.4	$⊢ (φ \land (a \in B \land b \in B) \land (p \in B \land q \in B)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
7		imasrhm.w	$⊢ φ \to W \in Ring$
8		eqidd	$⊢ φ \to F “_{𝑠} W = F “_{𝑠} W$
9	1	a1i	$⊢ φ \to B = {Base}_{W}$
10		eqid	$⊢ 1_{W} = 1_{W}$
11		fimadmfo	$⊢ F : B ⟶ C \to F : B \underset{onto}{⟶} F [B]$
12	2 11	syl	$⊢ φ \to F : B \underset{onto}{⟶} F [B]$
13	8 9 3 5 10 12 4 6 7	imasring	$⊢ φ \to (F “_{𝑠} W \in Ring \land F (1_{W}) = 1_{(F “_{𝑠} W)})$
14	13	simpld	$⊢ φ \to F “_{𝑠} W \in Ring$
15		eqid	$⊢ 1_{(F “_{𝑠} W)} = 1_{(F “_{𝑠} W)}$
16		eqid	$⊢ \cdot_{(F “_{𝑠} W)} = \cdot_{(F “_{𝑠} W)}$
17	13	simprd	$⊢ φ \to F (1_{W}) = 1_{(F “_{𝑠} W)}$
18	12 6 8 9 7 5 16	imasmulval	$⊢ (φ \land x \in B \land y \in B) \to F (x) \cdot_{(F “_{𝑠} W)} F (y) = F (x \underset{˙}{\cdot} y)$
19	18	3expb	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) \cdot_{(F “_{𝑠} W)} F (y) = F (x \underset{˙}{\cdot} y)$
20	19	eqcomd	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{\cdot} y) = F (x) \cdot_{(F “_{𝑠} W)} F (y)$
21		eqid	$⊢ {Base}_{(F “_{𝑠} W)} = {Base}_{(F “_{𝑠} W)}$
22		eqid	$⊢ +_{(F “_{𝑠} W)} = +_{(F “_{𝑠} W)}$
23		fof	$⊢ F : B \underset{onto}{⟶} F [B] \to F : B ⟶ F [B]$
24	12 23	syl	$⊢ φ \to F : B ⟶ F [B]$
25	8 9 12 7	imasbas	$⊢ φ \to F [B] = {Base}_{(F “_{𝑠} W)}$
26	25	feq3d	$⊢ φ \to (F : B ⟶ F [B] \leftrightarrow F : B ⟶ {Base}_{(F “_{𝑠} W)})$
27	24 26	mpbid	$⊢ φ \to F : B ⟶ {Base}_{(F “_{𝑠} W)}$
28	12 4 8 9 7 3 22	imasaddval	$⊢ (φ \land x \in B \land y \in B) \to F (x) +_{(F “_{𝑠} W)} F (y) = F (x \underset{˙}{+} y)$
29	28	3expb	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) +_{(F “_{𝑠} W)} F (y) = F (x \underset{˙}{+} y)$
30	29	eqcomd	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{+} y) = F (x) +_{(F “_{𝑠} W)} F (y)$
31	1 10 15 5 16 7 14 17 20 21 3 22 27 30	isrhmd	$⊢ φ \to F \in (W RingHom (F “_{𝑠} W))$
32	14 31	jca	$⊢ φ \to (F “_{𝑠} W \in Ring \land F \in (W RingHom (F “_{𝑠} W)))$

Metamath Proof Explorer

Theorem imasrhm

Proof