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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idlring.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idlring.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rng2idlring.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rng2idlring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rng2idlring.t	⊢ · = ( .r ‘ 𝑅 )
	rng2idlring.1	⊢ 1 = ( 1r ‘ 𝐽 )
	rngqiprngim.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	rngqiprngim.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
	rngqiprngim.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
	rngqiprngim.p	⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
	rngqiprngim.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
Assertion	rngqiprngimfv	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = ⟨ [ 𝐴 ] ∼ , ( 1 · 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rng2idlring.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rng2idlring.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		rng2idlring.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
5		rng2idlring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
6		rng2idlring.t	⊢ · = ( .r ‘ 𝑅 )
7		rng2idlring.1	⊢ 1 = ( 1r ‘ 𝐽 )
8		rngqiprngim.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9		rngqiprngim.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
10		rngqiprngim.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
11		rngqiprngim.p	⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
12		rngqiprngim.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) )
14		eceq1	⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )
15		oveq2	⊢ ( 𝑥 = 𝐴 → ( 1 · 𝑥 ) = ( 1 · 𝐴 ) )
16	14 15	opeq12d	⊢ ( 𝑥 = 𝐴 → ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ = ⟨ [ 𝐴 ] ∼ , ( 1 · 𝐴 ) ⟩ )
17	16	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 = 𝐴 ) → ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ = ⟨ [ 𝐴 ] ∼ , ( 1 · 𝐴 ) ⟩ )
18		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
19		opex	⊢ ⟨ [ 𝐴 ] ∼ , ( 1 · 𝐴 ) ⟩ ∈ V
20	19	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ⟨ [ 𝐴 ] ∼ , ( 1 · 𝐴 ) ⟩ ∈ V )
21	13 17 18 20	fvmptd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = ⟨ [ 𝐴 ] ∼ , ( 1 · 𝐴 ) ⟩ )