Metamath Proof Explorer

Theorem rngqiprnglinlem3

Description: Lemma 3 for rngqiprnglin . (Contributed by AV, 28-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 / 𝑠 ∼ ˙
Assertion rngqiprnglinlem3 ⊢ φ ∧ A ∈ B ∧ C ∈ B → A ∼ ˙ ⋅ Q C ∼ ˙ ∈ Base Q

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 1 2 3 4 5 6 7 8 9 rngqiprnglinlem2 ⊢ φ ∧ A ∈ B ∧ C ∈ B → A · ˙ C ∼ ˙ = A ∼ ˙ ⋅ Q C ∼ ˙
11 1 anim1i ⊢ φ ∧ A ∈ B ∧ C ∈ B → R ∈ Rng ∧ A ∈ B ∧ C ∈ B
12 3anass ⊢ R ∈ Rng ∧ A ∈ B ∧ C ∈ B ↔ R ∈ Rng ∧ A ∈ B ∧ C ∈ B
13 11 12 sylibr ⊢ φ ∧ A ∈ B ∧ C ∈ B → R ∈ Rng ∧ A ∈ B ∧ C ∈ B
14 5 6 rngcl ⊢ R ∈ Rng ∧ A ∈ B ∧ C ∈ B → A · ˙ C ∈ B
15 13 14 syl ⊢ φ ∧ A ∈ B ∧ C ∈ B → A · ˙ C ∈ B
16 eqid ⊢ Base Q = Base Q
17 8 9 5 16 quseccl0 ⊢ R ∈ Rng ∧ A · ˙ C ∈ B → A · ˙ C ∼ ˙ ∈ Base Q
18 1 15 17 syl2an2r ⊢ φ ∧ A ∈ B ∧ C ∈ B → A · ˙ C ∼ ˙ ∈ Base Q
19 10 18 eqeltrrd ⊢ φ ∧ A ∈ B ∧ C ∈ B → A ∼ ˙ ⋅ Q C ∼ ˙ ∈ Base Q