Theorem rngqiprngimfv

Description: The value of the function F at an element of (the base set of) a non-unital ring. (Contributed by AV, 24-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	rngqiprngimfv	|- ( ( ph /\ A e. B ) -> ( F ` A ) = <. [ A ] .~ , ( .1. .x. A ) >. )

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	12	a1i	|- ( ( ph /\ A e. B ) -> F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) )
14		eceq1	|- ( x = A -> [ x ] .~ = [ A ] .~ )
15		oveq2	|- ( x = A -> ( .1. .x. x ) = ( .1. .x. A ) )
16	14 15	opeq12d	|- ( x = A -> <. [ x ] .~ , ( .1. .x. x ) >. = <. [ A ] .~ , ( .1. .x. A ) >. )
17	16	adantl	|- ( ( ( ph /\ A e. B ) /\ x = A ) -> <. [ x ] .~ , ( .1. .x. x ) >. = <. [ A ] .~ , ( .1. .x. A ) >. )
18		simpr	|- ( ( ph /\ A e. B ) -> A e. B )
19		opex	|- <. [ A ] .~ , ( .1. .x. A ) >. e. _V
20	19	a1i	|- ( ( ph /\ A e. B ) -> <. [ A ] .~ , ( .1. .x. A ) >. e. _V )
21	13 17 18 20	fvmptd	|- ( ( ph /\ A e. B ) -> ( F ` A ) = <. [ A ] .~ , ( .1. .x. A ) >. )