Theorem rngqiprngfu

Description: The function value of F at the constructed expected ring unity of R is the ring unity of the product of the quotient with the two-sided ideal and the two-sided ideal. (Contributed by AV, 16-Mar-2025)

	Ref	Expression
Hypotheses	rngqiprngfu.r	|- ( ph -> R e. Rng )
	rngqiprngfu.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rngqiprngfu.j	|- J = ( R |`s I )
	rngqiprngfu.u	|- ( ph -> J e. Ring )
	rngqiprngfu.b	|- B = ( Base ` R )
	rngqiprngfu.t	|- .x. = ( .r ` R )
	rngqiprngfu.1	|- .1. = ( 1r ` J )
	rngqiprngfu.g	|- .~ = ( R ~QG I )
	rngqiprngfu.q	|- Q = ( R /s .~ )
	rngqiprngfu.v	|- ( ph -> Q e. Ring )
	rngqiprngfu.e	|- ( ph -> E e. ( 1r ` Q ) )
	rngqiprngfu.m	|- .- = ( -g ` R )
	rngqiprngfu.a	|- .+ = ( +g ` R )
	rngqiprngfu.n	|- U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
	rngqiprngfu.f	|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
Assertion	rngqiprngfu	|- ( ph -> ( F ` U ) = <. [ E ] .~ , .1. >. )

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	|- ( ph -> R e. Rng )
2		rngqiprngfu.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rngqiprngfu.j	|- J = ( R |`s I )
4		rngqiprngfu.u	|- ( ph -> J e. Ring )
5		rngqiprngfu.b	|- B = ( Base ` R )
6		rngqiprngfu.t	|- .x. = ( .r ` R )
7		rngqiprngfu.1	|- .1. = ( 1r ` J )
8		rngqiprngfu.g	|- .~ = ( R ~QG I )
9		rngqiprngfu.q	|- Q = ( R /s .~ )
10		rngqiprngfu.v	|- ( ph -> Q e. Ring )
11		rngqiprngfu.e	|- ( ph -> E e. ( 1r ` Q ) )
12		rngqiprngfu.m	|- .- = ( -g ` R )
13		rngqiprngfu.a	|- .+ = ( +g ` R )
14		rngqiprngfu.n	|- U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
15		rngqiprngfu.f	|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem3	|- ( ph -> U e. B )
17		eqid	|- ( Base ` Q ) = ( Base ` Q )
18		eqid	|- ( Q Xs. J ) = ( Q Xs. J )
19	1 2 3 4 5 6 7 8 9 17 18 15	rngqiprngimfv	|- ( ( ph /\ U e. B ) -> ( F ` U ) = <. [ U ] .~ , ( .1. .x. U ) >. )
20	16 19	mpdan	|- ( ph -> ( F ` U ) = <. [ U ] .~ , ( .1. .x. U ) >. )
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem4	|- ( ph -> [ U ] .~ = [ E ] .~ )
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem5	|- ( ph -> ( .1. .x. U ) = .1. )
23	21 22	opeq12d	|- ( ph -> <. [ U ] .~ , ( .1. .x. U ) >. = <. [ E ] .~ , .1. >. )
24	20 23	eqtrd	|- ( ph -> ( F ` U ) = <. [ E ] .~ , .1. >. )