Theorem rngqiprngim

Description: F is an isomorphism of non-unital rings. (Contributed by AV, 21-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	rngqiprngim	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RngIso 𝑃 ) )

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	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngho	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RngHom 𝑃 ) )
14	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimf1	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ ( 𝐶 × 𝐼 ) )
15	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfo	⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ ( 𝐶 × 𝐼 ) )
16		df-f1o	⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( 𝐶 × 𝐼 ) ↔ ( 𝐹 : 𝐵 –1-1→ ( 𝐶 × 𝐼 ) ∧ 𝐹 : 𝐵 –onto→ ( 𝐶 × 𝐼 ) ) )
17	14 15 16	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ ( 𝐶 × 𝐼 ) )
18	1 2 3 4 5 6 7 8 9 10 11	rngqipbas	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( 𝐶 × 𝐼 ) )
19	18	f1oeq3d	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑃 ) ↔ 𝐹 : 𝐵 –1-1-onto→ ( 𝐶 × 𝐼 ) ) )
20	17 19	mpbird	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑃 ) )
21	11	ovexi	⊢ 𝑃 ∈ V
22		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
23	5 22	isrngim2	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑃 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHom 𝑃 ) ∧ 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑃 ) ) ) )
24	1 21 23	sylancl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑅 RngIso 𝑃 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHom 𝑃 ) ∧ 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑃 ) ) ) )
25	13 20 24	mpbir2and	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RngIso 𝑃 ) )