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

Metamath Proof Explorer

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 )