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

Proof

Step Hyp Ref Expression
1 imasrngf1.u 
 |-  U = ( F "s R )
2 imasrngf1.v 
 |-  V = ( Base ` R )
3 1 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Rng ) -> U = ( F "s R ) )
4 2 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Rng ) -> V = ( Base ` R ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 eqid 
 |-  ( .r ` R ) = ( .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 e. 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 e. Rng ) -> F : V -onto-> ran F )
11 8 f1ocpbl 
 |-  ( ( ( F : V -1-1-> B /\ R e. Rng ) /\ ( 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 ) ) ) )
12 8 f1ocpbl 
 |-  ( ( ( F : V -1-1-> B /\ R e. Rng ) /\ ( 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 ) ) ) )
13 simpr 
 |-  ( ( F : V -1-1-> B /\ R e. Rng ) -> R e. Rng )
14 3 4 5 6 10 11 12 13 imasrng 
 |-  ( ( F : V -1-1-> B /\ R e. Rng ) -> U e. Rng )