Theorem rngqipring1

Description: The ring unity of the product of the quotient with a two-sided ideal and the two-sided ideal, which both are rings. (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 )
	rngqipring1.p	⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
Assertion	rngqipring1	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ⟨ [ 𝐸 ] ∼ , 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		rngqipring1.p	⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
16	15 10 4	xpsring1d	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ⟨ ( 1r ‘ 𝑄 ) , ( 1r ‘ 𝐽 ) ⟩ )
17	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
18		eleq2	⊢ ( ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) ↔ 𝐸 ∈ [ 𝑥 ] ∼ ) )
19	18	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) ↔ 𝐸 ∈ [ 𝑥 ] ∼ ) )
20		elecg	⊢ ( ( 𝐸 ∈ ( 1r ‘ 𝑄 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐸 ∈ [ 𝑥 ] ∼ ↔ 𝑥 ∼ 𝐸 ) )
21	11 20	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐸 ∈ [ 𝑥 ] ∼ ↔ 𝑥 ∼ 𝐸 ) )
22		ringrng	⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
23	4 22	syl	⊢ ( 𝜑 → 𝐽 ∈ Rng )
24	3 23	eqeltrrid	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
25	1 2 24	rng2idlnsg	⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
26		nsgsubg	⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
27	25 26	syl	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
29	5 8	eqger	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ∼ Er 𝐵 )
30	28 29	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∼ Er 𝐵 )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
32	30 31	erth	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∼ 𝐸 ↔ [ 𝑥 ] ∼ = [ 𝐸 ] ∼ ) )
33	32	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∼ 𝐸 ) → [ 𝑥 ] ∼ = [ 𝐸 ] ∼ )
34	33	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∼ 𝐸 ) → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ )
35	34	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∼ 𝐸 → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ ) )
36	21 35	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐸 ∈ [ 𝑥 ] ∼ → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ ) )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 𝐸 ∈ [ 𝑥 ] ∼ → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ ) )
38	19 37	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ ) )
39	38	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ ) ) )
40	17 39	mpid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ ) )
41	40	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → [ 𝐸 ] ∼ = [ 𝑥 ] ∼ )
42		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ )
43	41 42	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → [ 𝐸 ] ∼ = ( 1r ‘ 𝑄 ) )
44	1 2 3 4 5 6 7 8 9 10	rngqiprngfulem1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ )
45	43 44	r19.29a	⊢ ( 𝜑 → [ 𝐸 ] ∼ = ( 1r ‘ 𝑄 ) )
46	45	eqcomd	⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) = [ 𝐸 ] ∼ )
47	7	eqcomi	⊢ ( 1r ‘ 𝐽 ) = 1
48	47	a1i	⊢ ( 𝜑 → ( 1r ‘ 𝐽 ) = 1 )
49	46 48	opeq12d	⊢ ( 𝜑 → ⟨ ( 1r ‘ 𝑄 ) , ( 1r ‘ 𝐽 ) ⟩ = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )
50	16 49	eqtrd	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )