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 )