This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 imasringf1.u ⊢ U = F “ 𝑠 R
2 imasringf1.v ⊢ V = Base R
3 1 a1i ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → U = F “ 𝑠 R
4 2 a1i ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → V = Base R
5 eqid ⊢ + R = + R
6 eqid ⊢ ⋅ R = ⋅ R
7 eqid ⊢ 1 R = 1 R
8 f1f1orn ⊢ F : V ⟶ 1-1 B → F : V ⟶ 1-1 onto ran ⁡ F
9 8 adantr ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → F : V ⟶ 1-1 onto ran ⁡ F
10 f1ofo ⊢ F : V ⟶ 1-1 onto ran ⁡ F → F : V ⟶ onto ran ⁡ F
11 9 10 syl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → F : V ⟶ onto ran ⁡ F
12 9 f1ocpbl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring ∧ 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 9 f1ocpbl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring ∧ a ∈ V ∧ b ∈ V ∧ p ∈ V ∧ q ∈ V → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a ⋅ R b = F ⁡ p ⋅ R q
14 simpr ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → R ∈ Ring
15 3 4 5 6 7 11 12 13 14 imasring ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → U ∈ Ring ∧ F ⁡ 1 R = 1 U
16 15 simpld ⊢ F : V ⟶ 1-1 B ∧ R ∈ Ring → U ∈ Ring