Theorem rngqiprngim

Description: F is an isomorphism of non-unital rings. (Contributed by AV, 21-Feb-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	|- ( ph -> R e. Rng )
	rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlring.j	|- J = ( R |`s I )
	rng2idlring.u	|- ( ph -> J e. Ring )
	rng2idlring.b	|- B = ( Base ` R )
	rng2idlring.t	|- .x. = ( .r ` R )
	rng2idlring.1	|- .1. = ( 1r ` J )
	rngqiprngim.g	|- .~ = ( R ~QG I )
	rngqiprngim.q	|- Q = ( R /s .~ )
	rngqiprngim.c	|- C = ( Base ` Q )
	rngqiprngim.p	|- P = ( Q Xs. J )
	rngqiprngim.f	|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
Assertion	rngqiprngim	|- ( ph -> F e. ( R RngIso P ) )

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	|- ( ph -> R e. Rng )
2		rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idlring.j	|- J = ( R |`s I )
4		rng2idlring.u	|- ( ph -> J e. Ring )
5		rng2idlring.b	|- B = ( Base ` R )
6		rng2idlring.t	|- .x. = ( .r ` R )
7		rng2idlring.1	|- .1. = ( 1r ` J )
8		rngqiprngim.g	|- .~ = ( R ~QG I )
9		rngqiprngim.q	|- Q = ( R /s .~ )
10		rngqiprngim.c	|- C = ( Base ` Q )
11		rngqiprngim.p	|- P = ( Q Xs. J )
12		rngqiprngim.f	|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
13	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngho	|- ( ph -> F e. ( R RngHom P ) )
14	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimf1	|- ( ph -> F : B -1-1-> ( C X. I ) )
15	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfo	|- ( ph -> F : B -onto-> ( C X. I ) )
16		df-f1o	|- ( F : B -1-1-onto-> ( C X. I ) <-> ( F : B -1-1-> ( C X. I ) /\ F : B -onto-> ( C X. I ) ) )
17	14 15 16	sylanbrc	|- ( ph -> F : B -1-1-onto-> ( C X. I ) )
18	1 2 3 4 5 6 7 8 9 10 11	rngqipbas	|- ( ph -> ( Base ` P ) = ( C X. I ) )
19	18	f1oeq3d	|- ( ph -> ( F : B -1-1-onto-> ( Base ` P ) <-> F : B -1-1-onto-> ( C X. I ) ) )
20	17 19	mpbird	|- ( ph -> F : B -1-1-onto-> ( Base ` P ) )
21	11	ovexi	|- P e. _V
22		eqid	|- ( Base ` P ) = ( Base ` P )
23	5 22	isrngim2	|- ( ( R e. Rng /\ P e. _V ) -> ( F e. ( R RngIso P ) <-> ( F e. ( R RngHom P ) /\ F : B -1-1-onto-> ( Base ` P ) ) ) )
24	1 21 23	sylancl	|- ( ph -> ( F e. ( R RngIso P ) <-> ( F e. ( R RngHom P ) /\ F : B -1-1-onto-> ( Base ` P ) ) ) )
25	13 20 24	mpbir2and	|- ( ph -> F e. ( R RngIso P ) )