Theorem rngisomfv1

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is an element of the base set of the non-unital ring. (Contributed by AV, 27-Feb-2025)

	Ref	Expression
Hypotheses	rngisom1.1	|- .1. = ( 1r ` R )
	rngisom1.b	|- B = ( Base ` S )
Assertion	rngisomfv1	|- ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> ( F ` .1. ) e. B )

Proof

Step	Hyp	Ref	Expression
1		rngisom1.1	|- .1. = ( 1r ` R )
2		rngisom1.b	|- B = ( Base ` S )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4	3 2	rngimf1o	|- ( F e. ( R RngIso S ) -> F : ( Base ` R ) -1-1-onto-> B )
5		f1of	|- ( F : ( Base ` R ) -1-1-onto-> B -> F : ( Base ` R ) --> B )
6	4 5	syl	|- ( F e. ( R RngIso S ) -> F : ( Base ` R ) --> B )
7	6	adantl	|- ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> F : ( Base ` R ) --> B )
8	3 1	ringidcl	|- ( R e. Ring -> .1. e. ( Base ` R ) )
9	8	adantr	|- ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> .1. e. ( Base ` R ) )
10	7 9	ffvelcdmd	|- ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> ( F ` .1. ) e. B )