imasringf1

Description: The image of a ring under an injection is a ring ( imasmndf1 analog). (Contributed by AV, 27-Feb-2025)

	Ref	Expression
Hypotheses	imasringf1.u	$⊢ U = F “_{𝑠} R$
	imasringf1.v	$⊢ V = {Base}_{R}$
Assertion	imasringf1	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to U \in Ring$

Step	Hyp	Ref	Expression
1		imasringf1.u	$⊢ U = F “_{𝑠} R$
2		imasringf1.v	$⊢ V = {Base}_{R}$
3	1	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to U = F “_{𝑠} R$
4	2	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to V = {Base}_{R}$
5		eqid	$⊢ +_{R} = +_{R}$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		eqid	$⊢ 1_{R} = 1_{R}$
8		f1f1orn	$⊢ F : V \underset{1-1}{⟶} B \to F : V \underset{1-1 onto}{⟶} ran F$
9	8	adantr	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to F : V \underset{1-1 onto}{⟶} ran F$
10		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} ran F \to F : V \underset{onto}{⟶} ran F$
11	9 10	syl	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to F : V \underset{onto}{⟶} ran F$
12	9	f1ocpbl	$⊢ ((F : V \underset{1-1}{⟶} B \land R \in Ring) \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a +_{R} b) = F (p +_{R} q))$
13	9	f1ocpbl	$⊢ ((F : V \underset{1-1}{⟶} B \land R \in Ring) \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \cdot_{R} b) = F (p \cdot_{R} q))$
14		simpr	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to R \in Ring$
15	3 4 5 6 7 11 12 13 14	imasring	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to (U \in Ring \land F (1_{R}) = 1_{U})$
16	15	simpld	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Ring) \to U \in Ring$

Metamath Proof Explorer