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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
	rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
	rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
	rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
	rngqiprngim.f	$$⊢F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
Assertion	rngqiprngimfv	$$⊢\left(\phi \wedge A\in B\right)\to F\left(A\right)=⟨\left[A\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}A⟩$$

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
6		rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
8		rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10		rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
11		rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
12		rngqiprngim.f	$$⊢F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
13	12	a1i	$$⊢\left(\phi \wedge A\in B\right)\to F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
14		eceq1	$$⊢x=A\to \left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$
15		oveq2	$$⊢x=A\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=\underset{\dot{}}{1}\underset{\dot{}}{·}A$$
16	14 15	opeq12d	$$⊢x=A\to ⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩=⟨\left[A\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}A⟩$$
17	16	adantl	$$⊢\left(\left(\phi \wedge A\in B\right)\wedge x=A\right)\to ⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩=⟨\left[A\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}A⟩$$
18		simpr	$$⊢\left(\phi \wedge A\in B\right)\to A\in B$$
19		opex	$$⊢⟨\left[A\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}A⟩\in \mathrm{V}$$
20	19	a1i	$$⊢\left(\phi \wedge A\in B\right)\to ⟨\left[A\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}A⟩\in \mathrm{V}$$
21	13 17 18 20	fvmptd	$$⊢\left(\phi \wedge A\in B\right)\to F\left(A\right)=⟨\left[A\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}A⟩$$