This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑈 ) ) )