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 ⊢ 𝑈 = ( 𝐹 “s 𝑅 )
imasringf1.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
Assertion imasringf1 ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝑈 ∈ Ring )

Proof

Step Hyp Ref Expression
1 imasringf1.u ⊢ 𝑈 = ( 𝐹 “s 𝑅 )
2 imasringf1.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
3 1 a1i ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
4 2 a1i ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝑉 = ( Base ‘ 𝑅 ) )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 f1f1orn ⊢ ( 𝐹 : 𝑉 –1-1→ 𝐵 → 𝐹 : 𝑉 –1-1-onto→ ran 𝐹 )
9 8 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝑉 –1-1-onto→ ran 𝐹 )
10 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ran 𝐹 → 𝐹 : 𝑉 –onto→ ran 𝐹 )
11 9 10 syl ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝑉 –onto→ ran 𝐹 )
12 9 f1ocpbl ⊢ ( ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ) )
13 9 f1ocpbl ⊢ ( ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ) )
14 simpr ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
15 3 4 5 6 7 11 12 13 14 imasring ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → ( 𝑈 ∈ Ring ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑈 ) ) )
16 15 simpld ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ 𝑅 ∈ Ring ) → 𝑈 ∈ Ring )