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	$$⊢\underset{\dot{}}{1}=1_R$$
	rngisom1.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	rngisomfv1	$$⊢\left(R\in \mathrm{Ring}\wedge F\in \left(R\mathrm{RngIso}S\right)\right)\to F\left(\underset{\dot{}}{1}\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		rngisom1.1	$$⊢\underset{\dot{}}{1}=1_R$$
2		rngisom1.b	$$⊢B={\mathrm{Base}}_S$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3 2	rngimf1o	$$⊢F\in \left(R\mathrm{RngIso}S\right)\to F:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}B$$
5		f1of	$$⊢F:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}B\to F:{\mathrm{Base}}_R⟶B$$
6	4 5	syl	$$⊢F\in \left(R\mathrm{RngIso}S\right)\to F:{\mathrm{Base}}_R⟶B$$
7	6	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in \left(R\mathrm{RngIso}S\right)\right)\to F:{\mathrm{Base}}_R⟶B$$
8	3 1	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
9	8	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge F\in \left(R\mathrm{RngIso}S\right)\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
10	7 9	ffvelcdmd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in \left(R\mathrm{RngIso}S\right)\right)\to F\left(\underset{\dot{}}{1}\right)\in B$$