Metamath Proof Explorer

Theorem 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 ⟶ 1-1 B ∧ R ∈ Rng → U ∈ Rng

Proof

Step Hyp Ref Expression
1 imasrngf1.u ⊢ U = F “ 𝑠 R
2 imasrngf1.v ⊢ V = Base R
3 1 a1i ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng → U = F “ 𝑠 R
4 2 a1i ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng → V = Base R
5 eqid ⊢ + R = + R
6 eqid ⊢ ⋅ R = ⋅ R
7 f1f1orn ⊢ F : V ⟶ 1-1 B → F : V ⟶ 1-1 onto ran ⁡ F
8 7 adantr ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng → F : V ⟶ 1-1 onto ran ⁡ F
9 f1ofo ⊢ F : V ⟶ 1-1 onto ran ⁡ F → F : V ⟶ onto ran ⁡ F
10 8 9 syl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng → F : V ⟶ onto ran ⁡ F
11 8 f1ocpbl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng ∧ a ∈ V ∧ b ∈ V ∧ p ∈ V ∧ q ∈ V → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a + R b = F ⁡ p + R q
12 8 f1ocpbl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng ∧ a ∈ V ∧ b ∈ V ∧ p ∈ V ∧ q ∈ V → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a ⋅ R b = F ⁡ p ⋅ R q
13 simpr ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng → R ∈ Rng
14 3 4 5 6 10 11 12 13 imasrng ⊢ F : V ⟶ 1-1 B ∧ R ∈ Rng → U ∈ Rng