Theorem rngqiprngimf

Description: F is a function from (the base set of) a non-unital ring to the product of the (base set C of the) quotient with a two-sided ideal and the (base set I of the) two-sided ideal (because of 2idlbas , ( BaseJ ) = I !) (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	rngqiprngimf	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 𝐶 × 𝐼 ) )

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	8	ovexi	⊢ ∼ ∈ V
14	13	ecelqsi	⊢ ( 𝑥 ∈ 𝐵 → [ 𝑥 ] ∼ ∈ ( 𝐵 / ∼ ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ∼ ∈ ( 𝐵 / ∼ ) )
16	9	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑄 = ( 𝑅 /s ∼ ) )
17	5	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑅 ) )
18	13	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∼ ∈ V )
19	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Rng )
20	16 17 18 19	qusbas	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 / ∼ ) = ( Base ‘ 𝑄 ) )
21	20 10	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 / ∼ ) = 𝐶 )
22	15 21	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ∼ ∈ 𝐶 )
23		eqid	⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
24	2 3 23	2idlbas	⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = 𝐼 )
25	2 3 23	2idlelbas	⊢ ( 𝜑 → ( ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
26	25	simprd	⊢ ( 𝜑 → ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
27	24 26	eqeltrrd	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
28		ringrng	⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
29	4 28	syl	⊢ ( 𝜑 → 𝐽 ∈ Rng )
30	3 29	eqeltrrid	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
31	1 2 30	rng2idl0	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
32	1 27 31	3jca	⊢ ( 𝜑 → ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ) )
33	23 7	ringidcl	⊢ ( 𝐽 ∈ Ring → 1 ∈ ( Base ‘ 𝐽 ) )
34	4 33	syl	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝐽 ) )
35	34 24	eleqtrd	⊢ ( 𝜑 → 1 ∈ 𝐼 )
36	35	anim1ci	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ∧ 1 ∈ 𝐼 ) )
37		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
38		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
39	37 5 6 38	rngridlmcl	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 1 ∈ 𝐼 ) ) → ( 1 · 𝑥 ) ∈ 𝐼 )
40	32 36 39	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) ∈ 𝐼 )
41	22 40	opelxpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ∈ ( 𝐶 × 𝐼 ) )
42	41 12	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 𝐶 × 𝐼 ) )