| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | crngring 20242 | . . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 2 |  | prmidlidl 33472 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 3 | 1, 2 | sylan 580 | . . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 4 |  | qsidom.1 | . . . 4
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) | 
| 5 |  | eqid 2737 | . . . 4
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 6 | 4, 5 | quscrng 21293 | . . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑄 ∈ CRing) | 
| 7 | 3, 6 | syldan 591 | . 2
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ CRing) | 
| 8 | 5 | crng2idl 21291 | . . . . . . . 8
⊢ (𝑅 ∈ CRing →
(LIdeal‘𝑅) =
(2Ideal‘𝑅)) | 
| 9 | 8 | eleq2d 2827 | . . . . . . 7
⊢ (𝑅 ∈ CRing → (𝐼 ∈ (LIdeal‘𝑅) ↔ 𝐼 ∈ (2Ideal‘𝑅))) | 
| 10 | 9 | biimpa 476 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (2Ideal‘𝑅)) | 
| 11 | 3, 10 | syldan 591 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ∈ (2Ideal‘𝑅)) | 
| 12 |  | eqid 2737 | . . . . . 6
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) | 
| 13 | 4, 12 | qusring 21285 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → 𝑄 ∈ Ring) | 
| 14 | 1, 11, 13 | syl2an2r 685 | . . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ Ring) | 
| 15 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 16 |  | eqid 2737 | . . . . . . . . 9
⊢
(0g‘𝑄) = (0g‘𝑄) | 
| 17 | 15, 16 | ring0cl 20264 | . . . . . . . 8
⊢ (𝑄 ∈ Ring →
(0g‘𝑄)
∈ (Base‘𝑄)) | 
| 18 | 14, 17 | syl 17 | . . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
(0g‘𝑄)
∈ (Base‘𝑄)) | 
| 19 | 18 | snssd 4809 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
{(0g‘𝑄)}
⊆ (Base‘𝑄)) | 
| 20 |  | lidlnsg 21258 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) | 
| 21 | 1, 20 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) | 
| 22 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 23 | 4, 22 | qus0 19207 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) | 
| 24 | 21, 23 | syl 17 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) | 
| 25 | 5 | lidlsubg 21233 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 26 | 1, 25 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 27 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 28 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑅 ~QG 𝐼) = (𝑅 ~QG 𝐼) | 
| 29 | 27, 28, 22 | eqgid 19198 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (SubGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = 𝐼) | 
| 30 | 26, 29 | syl 17 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = 𝐼) | 
| 31 | 24, 30 | eqtr3d 2779 | . . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
(0g‘𝑄) =
𝐼) | 
| 32 | 3, 31 | syldan 591 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
(0g‘𝑄) =
𝐼) | 
| 33 | 32 | sneqd 4638 | . . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
{(0g‘𝑄)} =
{𝐼}) | 
| 34 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 35 | 27, 34 | isprmidlc 33475 | . . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → (𝐼 ∈ (PrmIdeal‘𝑅) ↔ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))))) | 
| 36 | 35 | biimpa 476 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)))) | 
| 37 | 36 | simp2d 1144 | . . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ≠ (Base‘𝑅)) | 
| 38 |  | ringgrp 20235 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 39 | 1, 38 | syl 17 | . . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Grp) | 
| 40 | 39 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝑅 ∈ Grp) | 
| 41 | 1 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝑅 ∈ Ring) | 
| 42 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 43 | 41, 42, 25 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 44 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → (Base‘𝑄) = {𝐼}) | 
| 45 | 27, 4 | qustrivr 33393 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 = (Base‘𝑅)) | 
| 46 | 40, 43, 44, 45 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 = (Base‘𝑅)) | 
| 47 | 37, 46 | mteqand 3033 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → (Base‘𝑄) ≠ {𝐼}) | 
| 48 | 47 | necomd 2996 | . . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → {𝐼} ≠ (Base‘𝑄)) | 
| 49 | 33, 48 | eqnetrd 3008 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
{(0g‘𝑄)}
≠ (Base‘𝑄)) | 
| 50 |  | pssdifn0 4368 | . . . . . 6
⊢
(({(0g‘𝑄)} ⊆ (Base‘𝑄) ∧ {(0g‘𝑄)} ≠ (Base‘𝑄)) → ((Base‘𝑄) ∖
{(0g‘𝑄)})
≠ ∅) | 
| 51 | 19, 49, 50 | syl2anc 584 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ((Base‘𝑄) ∖
{(0g‘𝑄)})
≠ ∅) | 
| 52 |  | n0 4353 | . . . . 5
⊢
(((Base‘𝑄)
∖ {(0g‘𝑄)}) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) | 
| 53 | 51, 52 | sylib 218 | . . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ∃𝑥 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) | 
| 54 | 16, 15 | ringelnzr 20523 | . . . . . 6
⊢ ((𝑄 ∈ Ring ∧ 𝑥 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
→ 𝑄 ∈
NzRing) | 
| 55 | 54 | ex 412 | . . . . 5
⊢ (𝑄 ∈ Ring → (𝑥 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)})
→ 𝑄 ∈
NzRing)) | 
| 56 | 55 | exlimdv 1933 | . . . 4
⊢ (𝑄 ∈ Ring →
(∃𝑥 𝑥 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)})
→ 𝑄 ∈
NzRing)) | 
| 57 | 14, 53, 56 | sylc 65 | . . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ NzRing) | 
| 58 | 36 | simp3d 1145 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) | 
| 59 | 58 | ad7antr 738 | . . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) | 
| 60 |  | simp-4r 784 | . . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑥 ∈ (Base‘𝑅)) | 
| 61 |  | simplr 769 | . . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑦 ∈ (Base‘𝑅)) | 
| 62 |  | simp-8l 791 | . . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑅 ∈ CRing) | 
| 63 | 62, 39 | syl 17 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑅 ∈ Grp) | 
| 64 | 3 | ad7antr 738 | . . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 65 | 62, 64, 26 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 66 | 4 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) | 
| 67 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (Base‘𝑅) = (Base‘𝑅)) | 
| 68 | 27, 28 | eqger 19196 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ (SubGrp‘𝑅) → (𝑅 ~QG 𝐼) Er (Base‘𝑅)) | 
| 69 | 26, 68 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑅 ~QG 𝐼) Er (Base‘𝑅)) | 
| 70 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑅 ∈ CRing) | 
| 71 | 27, 28, 12, 34 | 2idlcpbl 21282 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → ((𝑔(𝑅 ~QG 𝐼)𝑒 ∧ ℎ(𝑅 ~QG 𝐼)𝑓) → (𝑔(.r‘𝑅)ℎ)(𝑅 ~QG 𝐼)(𝑒(.r‘𝑅)𝑓))) | 
| 72 | 1, 10, 71 | syl2an2r 685 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑔(𝑅 ~QG 𝐼)𝑒 ∧ ℎ(𝑅 ~QG 𝐼)𝑓) → (𝑔(.r‘𝑅)ℎ)(𝑅 ~QG 𝐼)(𝑒(.r‘𝑅)𝑓))) | 
| 73 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → 𝑅 ∈ Ring) | 
| 74 |  | simprl 771 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → 𝑒 ∈ (Base‘𝑅)) | 
| 75 |  | simprr 773 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → 𝑓 ∈ (Base‘𝑅)) | 
| 76 | 27, 34 | ringcl 20247 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅)) → (𝑒(.r‘𝑅)𝑓) ∈ (Base‘𝑅)) | 
| 77 | 73, 74, 75, 76 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → (𝑒(.r‘𝑅)𝑓) ∈ (Base‘𝑅)) | 
| 78 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(.r‘𝑄) = (.r‘𝑄) | 
| 79 | 66, 67, 69, 70, 72, 77, 34, 78 | qusmulval 17600 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼)) | 
| 80 | 62, 64, 60, 61, 79 | syl211anc 1378 | . . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼)) | 
| 81 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) | 
| 82 | 81 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) | 
| 83 |  | simpllr 776 | . . . . . . . . . . . . . 14
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑎 = [𝑥](𝑅 ~QG 𝐼)) | 
| 84 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑏 = [𝑦](𝑅 ~QG 𝐼)) | 
| 85 | 83, 84 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎(.r‘𝑄)𝑏) = ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼))) | 
| 86 | 62, 64, 31 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (0g‘𝑄) = 𝐼) | 
| 87 | 82, 85, 86 | 3eqtr3d 2785 | . . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = 𝐼) | 
| 88 | 80, 87 | eqtr3d 2779 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼) | 
| 89 | 28 | eqg0el 19201 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼 ↔ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼)) | 
| 90 | 89 | biimpa 476 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) | 
| 91 | 63, 65, 88, 90 | syl21anc 838 | . . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) | 
| 92 |  | rsp2 3277 | . . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)))) | 
| 93 | 92 | impl 455 | . . . . . . . . . . 11
⊢
(((∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) | 
| 94 | 93 | imp 406 | . . . . . . . . . 10
⊢
((((∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) | 
| 95 | 59, 60, 61, 91, 94 | syl1111anc 841 | . . . . . . . . 9
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) | 
| 96 | 86 | eqeq2d 2748 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎 = (0g‘𝑄) ↔ 𝑎 = 𝐼)) | 
| 97 | 83 | eqeq1d 2739 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎 = 𝐼 ↔ [𝑥](𝑅 ~QG 𝐼) = 𝐼)) | 
| 98 | 28 | eqg0el 19201 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑥 ∈ 𝐼)) | 
| 99 | 63, 65, 98 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑥](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑥 ∈ 𝐼)) | 
| 100 | 96, 97, 99 | 3bitrrd 306 | . . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑥 ∈ 𝐼 ↔ 𝑎 = (0g‘𝑄))) | 
| 101 | 86 | eqeq2d 2748 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑏 = (0g‘𝑄) ↔ 𝑏 = 𝐼)) | 
| 102 | 84 | eqeq1d 2739 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑏 = 𝐼 ↔ [𝑦](𝑅 ~QG 𝐼) = 𝐼)) | 
| 103 | 28 | eqg0el 19201 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([𝑦](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑦 ∈ 𝐼)) | 
| 104 | 63, 65, 103 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑦](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑦 ∈ 𝐼)) | 
| 105 | 101, 102,
104 | 3bitrrd 306 | . . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑦 ∈ 𝐼 ↔ 𝑏 = (0g‘𝑄))) | 
| 106 | 100, 105 | orbi12d 919 | . . . . . . . . 9
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ((𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼) ↔ (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) | 
| 107 | 95, 106 | mpbid 232 | . . . . . . . 8
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄))) | 
| 108 |  | simplr 769 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → 𝑏 ∈ (Base‘𝑄)) | 
| 109 | 4 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) | 
| 110 |  | eqidd 2738 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) =
(Base‘𝑅)) | 
| 111 |  | ovexd 7466 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → (𝑅 ~QG 𝐼) ∈ V) | 
| 112 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CRing) | 
| 113 | 109, 110,
111, 112 | qusbas 17590 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
((Base‘𝑅) /
(𝑅 ~QG
𝐼)) = (Base‘𝑄)) | 
| 114 | 113 | ad4antr 732 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → ((Base‘𝑅) / (𝑅 ~QG 𝐼)) = (Base‘𝑄)) | 
| 115 | 108, 114 | eleqtrrd 2844 | . . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → 𝑏 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) | 
| 116 | 115 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) → 𝑏 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) | 
| 117 |  | elqsi 8810 | . . . . . . . . 9
⊢ (𝑏 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼)) → ∃𝑦 ∈ (Base‘𝑅)𝑏 = [𝑦](𝑅 ~QG 𝐼)) | 
| 118 | 116, 117 | syl 17 | . . . . . . . 8
⊢
(((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) → ∃𝑦 ∈ (Base‘𝑅)𝑏 = [𝑦](𝑅 ~QG 𝐼)) | 
| 119 | 107, 118 | r19.29a 3162 | . . . . . . 7
⊢
(((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄))) | 
| 120 |  | simpllr 776 | . . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → 𝑎 ∈ (Base‘𝑄)) | 
| 121 | 120, 114 | eleqtrrd 2844 | . . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → 𝑎 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) | 
| 122 |  | elqsi 8810 | . . . . . . . 8
⊢ (𝑎 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼)) → ∃𝑥 ∈ (Base‘𝑅)𝑎 = [𝑥](𝑅 ~QG 𝐼)) | 
| 123 | 121, 122 | syl 17 | . . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → ∃𝑥 ∈ (Base‘𝑅)𝑎 = [𝑥](𝑅 ~QG 𝐼)) | 
| 124 | 119, 123 | r19.29a 3162 | . . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄))) | 
| 125 | 124 | ex 412 | . . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ 𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) → ((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) | 
| 126 | 125 | anasss 466 | . . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (𝑎 ∈ (Base‘𝑄) ∧ 𝑏 ∈ (Base‘𝑄))) → ((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) | 
| 127 | 126 | ralrimivva 3202 | . . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ∀𝑎 ∈ (Base‘𝑄)∀𝑏 ∈ (Base‘𝑄)((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) | 
| 128 | 15, 78, 16 | isdomn 20705 | . . 3
⊢ (𝑄 ∈ Domn ↔ (𝑄 ∈ NzRing ∧
∀𝑎 ∈
(Base‘𝑄)∀𝑏 ∈ (Base‘𝑄)((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄))))) | 
| 129 | 57, 127, 128 | sylanbrc 583 | . 2
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ Domn) | 
| 130 |  | isidom 20725 | . 2
⊢ (𝑄 ∈ IDomn ↔ (𝑄 ∈ CRing ∧ 𝑄 ∈ Domn)) | 
| 131 | 7, 129, 130 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) |