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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rngqiprngfu.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rngqiprngfu.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rngqiprngfu.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rngqiprngfu.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rngqiprngfu.t	⊢ · = ( .r ‘ 𝑅 )
	rngqiprngfu.1	⊢ 1 = ( 1r ‘ 𝐽 )
	rngqiprngfu.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	rngqiprngfu.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
	rngqiprngfu.v	⊢ ( 𝜑 → 𝑄 ∈ Ring )
	rngqiprngfu.e	⊢ ( 𝜑 → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
	rngqiprngfu.m	⊢ − = ( -g ‘ 𝑅 )
	rngqiprngfu.a	⊢ + = ( +g ‘ 𝑅 )
	rngqiprngfu.n	⊢ 𝑈 = ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 )
	rngqiprngfu.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
Assertion	rngqiprngfu	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rngqiprngfu.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rngqiprngfu.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		rngqiprngfu.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
5		rngqiprngfu.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
6		rngqiprngfu.t	⊢ · = ( .r ‘ 𝑅 )
7		rngqiprngfu.1	⊢ 1 = ( 1r ‘ 𝐽 )
8		rngqiprngfu.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9		rngqiprngfu.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
10		rngqiprngfu.v	⊢ ( 𝜑 → 𝑄 ∈ Ring )
11		rngqiprngfu.e	⊢ ( 𝜑 → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
12		rngqiprngfu.m	⊢ − = ( -g ‘ 𝑅 )
13		rngqiprngfu.a	⊢ + = ( +g ‘ 𝑅 )
14		rngqiprngfu.n	⊢ 𝑈 = ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 )
15		rngqiprngfu.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem3	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
17		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
18		eqid	⊢ ( 𝑄 ×s 𝐽 ) = ( 𝑄 ×s 𝐽 )
19	1 2 3 4 5 6 7 8 9 17 18 15	rngqiprngimfv	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑈 ) = ⟨ [ 𝑈 ] ∼ , ( 1 · 𝑈 ) ⟩ )
20	16 19	mpdan	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) = ⟨ [ 𝑈 ] ∼ , ( 1 · 𝑈 ) ⟩ )
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem4	⊢ ( 𝜑 → [ 𝑈 ] ∼ = [ 𝐸 ] ∼ )
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem5	⊢ ( 𝜑 → ( 1 · 𝑈 ) = 1 )
23	21 22	opeq12d	⊢ ( 𝜑 → ⟨ [ 𝑈 ] ∼ , ( 1 · 𝑈 ) ⟩ = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )
24	20 23	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )