Theorem qusring2

Description: The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015)

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

Proof

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