Theorem qusrng

Description: The quotient structure of a non-unital ring is a non-unital ring ( qusring2 analog). (Contributed by AV, 23-Feb-2025)

	Ref	Expression
Hypotheses	qusrng.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
	qusrng.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	qusrng.p	⊢ + = ( +g ‘ 𝑅 )
	qusrng.t	⊢ · = ( .r ‘ 𝑅 )
	qusrng.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
	qusrng.e1	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
	qusrng.e2	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) )
	qusrng.x	⊢ ( 𝜑 → 𝑅 ∈ Rng )
Assertion	qusrng	⊢ ( 𝜑 → 𝑈 ∈ Rng )

Proof

Step	Hyp	Ref	Expression
1		qusrng.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2		qusrng.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		qusrng.p	⊢ + = ( +g ‘ 𝑅 )
4		qusrng.t	⊢ · = ( .r ‘ 𝑅 )
5		qusrng.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
6		qusrng.e1	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
7		qusrng.e2	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) )
8		qusrng.x	⊢ ( 𝜑 → 𝑅 ∈ Rng )
9		eqid	⊢ ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) = ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ )
10		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
11	2 10	eqeltrdi	⊢ ( 𝜑 → 𝑉 ∈ V )
12		erex	⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) )
13	5 11 12	sylc	⊢ ( 𝜑 → ∼ ∈ V )
14	1 2 9 13 8	qusval	⊢ ( 𝜑 → 𝑈 = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) “s 𝑅 ) )
15	1 2 9 13 8	quslem	⊢ ( 𝜑 → ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) )
16	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑅 ∈ Rng )
17		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
18	2	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
20	17 19	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
21		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
22	2	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑉 ↔ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑦 ∈ 𝑉 ↔ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
24	21 23	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
25		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26	25 3	rngacl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
27	16 20 24 26	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
28	2	eleq2d	⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) ∈ 𝑉 ↔ ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) ∈ 𝑉 ↔ ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
30	27 29	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
31	5 11 9 30 6	ercpbl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑎 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑝 ) ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑏 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑞 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑝 + 𝑞 ) ) ) )
32	25 4	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
33	16 20 24 32	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
34	2	eleq2d	⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) ∈ 𝑉 ↔ ( 𝑥 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑥 · 𝑦 ) ∈ 𝑉 ↔ ( 𝑥 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
36	33 35	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑉 )
37	5 11 9 36 7	ercpbl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑎 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑝 ) ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑏 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑞 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑝 · 𝑞 ) ) ) )
38	14 2 3 4 15 31 37 8	imasrng	⊢ ( 𝜑 → 𝑈 ∈ Rng )