Metamath Proof Explorer

Theorem rngqiprng

Description: The product of the quotient with a two-sided ideal and the two-sided ideal is a non-unital ring. (Contributed by AV, 23-Feb-2025)

Ref Expression
Hypotheses rng2idlring.r ⊢ φ → R ∈ Rng
rng2idlring.i ⊢ φ → I ∈ 2Ideal ⁡ R
rng2idlring.j ⊢ J = R ↾ 𝑠 I
rng2idlring.u ⊢ φ → J ∈ Ring
rng2idlring.b ⊢ B = Base R
rng2idlring.t ⊢ · ˙ = ⋅ R
rng2idlring.1 ⊢ 1 ˙ = 1 J
rngqiprngim.g ⊢ ∼ ˙ = R ~ QG I
rngqiprngim.q ⊢ Q = R / 𝑠 ∼ ˙
rngqiprngim.c ⊢ C = Base Q
rngqiprngim.p ⊢ P = Q × 𝑠 J
Assertion rngqiprng ⊢ φ → P ∈ Rng

Proof

Step Hyp Ref Expression
1 rng2idlring.r ⊢ φ → R ∈ Rng
2 rng2idlring.i ⊢ φ → I ∈ 2Ideal ⁡ R
3 rng2idlring.j ⊢ J = R ↾ 𝑠 I
4 rng2idlring.u ⊢ φ → J ∈ Ring
5 rng2idlring.b ⊢ B = Base R
6 rng2idlring.t ⊢ · ˙ = ⋅ R
7 rng2idlring.1 ⊢ 1 ˙ = 1 J
8 rngqiprngim.g ⊢ ∼ ˙ = R ~ QG I
9 rngqiprngim.q ⊢ Q = R / 𝑠 ∼ ˙
10 rngqiprngim.c ⊢ C = Base Q
11 rngqiprngim.p ⊢ P = Q × 𝑠 J
12 ringrng ⊢ J ∈ Ring → J ∈ Rng
13 4 12 syl ⊢ φ → J ∈ Rng
14 3 13 eqeltrrid ⊢ φ → R ↾ 𝑠 I ∈ Rng
15 1 2 14 rng2idlsubrng ⊢ φ → I ∈ SubRng ⁡ R
16 subrngsubg ⊢ I ∈ SubRng ⁡ R → I ∈ SubGrp ⁡ R
17 15 16 syl ⊢ φ → I ∈ SubGrp ⁡ R
18 8 oveq2i ⊢ R / 𝑠 ∼ ˙ = R / 𝑠 R ~ QG I
19 9 18 eqtri ⊢ Q = R / 𝑠 R ~ QG I
20 eqid ⊢ 2Ideal ⁡ R = 2Ideal ⁡ R
21 19 20 qus2idrng ⊢ R ∈ Rng ∧ I ∈ 2Ideal ⁡ R ∧ I ∈ SubGrp ⁡ R → Q ∈ Rng
22 1 2 17 21 syl3anc ⊢ φ → Q ∈ Rng
23 11 22 13 xpsrngd ⊢ φ → P ∈ Rng