imasrngf1

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

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

Step	Hyp	Ref	Expression
1		imasrngf1.u	$⊢ U = F “_{𝑠} R$
2		imasrngf1.v	$⊢ V = {Base}_{R}$
3	1	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Rng) \to U = F “_{𝑠} R$
4	2	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Rng) \to V = {Base}_{R}$
5		eqid	$⊢ +_{R} = +_{R}$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		f1f1orn	$⊢ F : V \underset{1-1}{⟶} B \to F : V \underset{1-1 onto}{⟶} ran F$
8	7	adantr	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Rng) \to F : V \underset{1-1 onto}{⟶} ran F$
9		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} ran F \to F : V \underset{onto}{⟶} ran F$
10	8 9	syl	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Rng) \to F : V \underset{onto}{⟶} ran F$
11	8	f1ocpbl	$⊢ ((F : V \underset{1-1}{⟶} B \land R \in Rng) \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))$
12	8	f1ocpbl	$⊢ ((F : V \underset{1-1}{⟶} B \land R \in Rng) \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))$
13		simpr	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Rng) \to R \in Rng$
14	3 4 5 6 10 11 12 13	imasrng	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Rng) \to U \in Rng$

Metamath Proof Explorer