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 "s R )
imasringf1.v 
|- V = ( Base ` R )
Assertion imasringf1 
|- ( ( F : V -1-1-> B /\ R e. Ring ) -> U e. Ring )

Proof

Step Hyp Ref Expression
1 imasringf1.u 
 |-  U = ( F "s R )
2 imasringf1.v 
 |-  V = ( Base ` R )
3 1 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Ring ) -> U = ( F "s R ) )
4 2 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Ring ) -> V = ( Base ` R ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 f1f1orn 
 |-  ( F : V -1-1-> B -> F : V -1-1-onto-> ran F )
9 8 adantr 
 |-  ( ( F : V -1-1-> B /\ R e. 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 e. Ring ) -> F : V -onto-> ran F )
12 9 f1ocpbl 
 |-  ( ( ( F : V -1-1-> B /\ R e. Ring ) /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
13 9 f1ocpbl 
 |-  ( ( ( F : V -1-1-> B /\ R e. Ring ) /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( F ` ( p ( .r ` R ) q ) ) ) )
14 simpr 
 |-  ( ( F : V -1-1-> B /\ R e. Ring ) -> R e. Ring )
15 3 4 5 6 7 11 12 13 14 imasring 
 |-  ( ( F : V -1-1-> B /\ R e. Ring ) -> ( U e. Ring /\ ( F ` ( 1r ` R ) ) = ( 1r ` U ) ) )
16 15 simpld 
 |-  ( ( F : V -1-1-> B /\ R e. Ring ) -> U e. Ring )