Step | Hyp | Ref
| Expression |
1 | | crngring 19428 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | | prmidlidl 31191 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ∈ (LIdeal‘𝑅)) |
3 | 1, 2 | sylan 583 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ∈ (LIdeal‘𝑅)) |
4 | | qsidom.1 |
. . . 4
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
5 | | eqid 2738 |
. . . 4
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
6 | 4, 5 | quscrng 20132 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑄 ∈ CRing) |
7 | 3, 6 | syldan 594 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ CRing) |
8 | 5 | crng2idl 20131 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing →
(LIdeal‘𝑅) =
(2Ideal‘𝑅)) |
9 | 8 | eleq2d 2818 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → (𝐼 ∈ (LIdeal‘𝑅) ↔ 𝐼 ∈ (2Ideal‘𝑅))) |
10 | 9 | biimpa 480 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (2Ideal‘𝑅)) |
11 | 3, 10 | syldan 594 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ∈ (2Ideal‘𝑅)) |
12 | | eqid 2738 |
. . . . . 6
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
13 | 4, 12 | qusring 20128 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → 𝑄 ∈ Ring) |
14 | 1, 11, 13 | syl2an2r 685 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ Ring) |
15 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑄) =
(Base‘𝑄) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘𝑄) = (0g‘𝑄) |
17 | 15, 16 | ring0cl 19441 |
. . . . . . . 8
⊢ (𝑄 ∈ Ring →
(0g‘𝑄)
∈ (Base‘𝑄)) |
18 | 14, 17 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
(0g‘𝑄)
∈ (Base‘𝑄)) |
19 | 18 | snssd 4697 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
{(0g‘𝑄)}
⊆ (Base‘𝑄)) |
20 | | lidlnsg 31193 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
21 | 1, 20 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
22 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
23 | 4, 22 | qus0 18456 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
25 | 5 | lidlsubg 20107 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (SubGrp‘𝑅)) |
26 | 1, 25 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (SubGrp‘𝑅)) |
27 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
28 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑅 ~QG 𝐼) = (𝑅 ~QG 𝐼) |
29 | 27, 28, 22 | eqgid 18450 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (SubGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = 𝐼) |
30 | 26, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = 𝐼) |
31 | 24, 30 | eqtr3d 2775 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
(0g‘𝑄) =
𝐼) |
32 | 3, 31 | syldan 594 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
(0g‘𝑄) =
𝐼) |
33 | 32 | sneqd 4528 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
{(0g‘𝑄)} =
{𝐼}) |
34 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
35 | 27, 34 | isprmidlc 31195 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → (𝐼 ∈ (PrmIdeal‘𝑅) ↔ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))))) |
36 | 35 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)))) |
37 | 36 | simp2d 1144 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝐼 ≠ (Base‘𝑅)) |
38 | | ringgrp 19421 |
. . . . . . . . . . . 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 484 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 ∈ (LIdeal‘𝑅)) |
43 | 41, 42, 25 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 ∈ (SubGrp‘𝑅)) |
44 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → (Base‘𝑄) = {𝐼}) |
45 | 27, 4 | qustrivr 31133 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 = (Base‘𝑅)) |
46 | 40, 43, 44, 45 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (Base‘𝑄) = {𝐼}) → 𝐼 = (Base‘𝑅)) |
47 | 37, 46 | mteqand 3037 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → (Base‘𝑄) ≠ {𝐼}) |
48 | 47 | necomd 2989 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → {𝐼} ≠ (Base‘𝑄)) |
49 | 33, 48 | eqnetrd 3001 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) →
{(0g‘𝑄)}
≠ (Base‘𝑄)) |
50 | | pssdifn0 4254 |
. . . . . 6
⊢
(({(0g‘𝑄)} ⊆ (Base‘𝑄) ∧ {(0g‘𝑄)} ≠ (Base‘𝑄)) → ((Base‘𝑄) ∖
{(0g‘𝑄)})
≠ ∅) |
51 | 19, 49, 50 | syl2anc 587 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ((Base‘𝑄) ∖
{(0g‘𝑄)})
≠ ∅) |
52 | | n0 4235 |
. . . . 5
⊢
(((Base‘𝑄)
∖ {(0g‘𝑄)}) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) |
53 | 51, 52 | sylib 221 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ∃𝑥 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) |
54 | 16, 15 | ringelnzr 20158 |
. . . . . 6
⊢ ((𝑄 ∈ Ring ∧ 𝑥 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
→ 𝑄 ∈
NzRing) |
55 | 54 | ex 416 |
. . . . 5
⊢ (𝑄 ∈ Ring → (𝑥 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)})
→ 𝑄 ∈
NzRing)) |
56 | 55 | exlimdv 1940 |
. . . 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 587 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝐼 ∈ (SubGrp‘𝑅)) |
66 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) |
67 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (Base‘𝑅) = (Base‘𝑅)) |
68 | 27, 28 | eqger 18448 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ (SubGrp‘𝑅) → (𝑅 ~QG 𝐼) Er (Base‘𝑅)) |
69 | 26, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑅 ~QG 𝐼) Er (Base‘𝑅)) |
70 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑅 ∈ CRing) |
71 | 27, 28, 12, 34 | 2idlcpbl 20126 |
. . . . . . . . . . . . . . 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 19433 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅)) → (𝑒(.r‘𝑅)𝑓) ∈ (Base‘𝑅)) |
77 | 73, 74, 75, 76 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → (𝑒(.r‘𝑅)𝑓) ∈ (Base‘𝑅)) |
78 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑄) = (.r‘𝑄) |
79 | 66, 67, 69, 70, 72, 77, 34, 78 | qusmulval 16931 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼)) |
80 | 62, 64, 60, 61, 79 | syl211anc 1377 |
. . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼)) |
81 | | simpr 488 |
. . . . . . . . . . . . . 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 488 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → 𝑏 = [𝑦](𝑅 ~QG 𝐼)) |
85 | 83, 84 | oveq12d 7188 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎(.r‘𝑄)𝑏) = ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼))) |
86 | 62, 64, 31 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (0g‘𝑄) = 𝐼) |
87 | 82, 85, 86 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = 𝐼) |
88 | 80, 87 | eqtr3d 2775 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼) |
89 | 28 | eqg0el 31129 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼 ↔ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼)) |
90 | 89 | biimpa 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) |
91 | 63, 65, 88, 90 | syl21anc 837 |
. . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) |
92 | | rsp2 3125 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)))) |
93 | 92 | impl 459 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) |
94 | 93 | imp 410 |
. . . . . . . . . 10
⊢
((((∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) |
95 | 59, 60, 61, 91, 94 | syl1111anc 839 |
. . . . . . . . 9
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) |
96 | 86 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎 = (0g‘𝑄) ↔ 𝑎 = 𝐼)) |
97 | 83 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑎 = 𝐼 ↔ [𝑥](𝑅 ~QG 𝐼) = 𝐼)) |
98 | 28 | eqg0el 31129 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑥 ∈ 𝐼)) |
99 | 63, 65, 98 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑥](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑥 ∈ 𝐼)) |
100 | 96, 97, 99 | 3bitrrd 309 |
. . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑥 ∈ 𝐼 ↔ 𝑎 = (0g‘𝑄))) |
101 | 86 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑏 = (0g‘𝑄) ↔ 𝑏 = 𝐼)) |
102 | 84 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑏 = 𝐼 ↔ [𝑦](𝑅 ~QG 𝐼) = 𝐼)) |
103 | 28 | eqg0el 31129 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([𝑦](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑦 ∈ 𝐼)) |
104 | 63, 65, 103 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ([𝑦](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑦 ∈ 𝐼)) |
105 | 101, 102,
104 | 3bitrrd 309 |
. . . . . . . . . 10
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → (𝑦 ∈ 𝐼 ↔ 𝑏 = (0g‘𝑄))) |
106 | 100, 105 | orbi12d 918 |
. . . . . . . . 9
⊢
(((((((((𝑅 ∈
CRing ∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 = [𝑥](𝑅 ~QG 𝐼)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑏 = [𝑦](𝑅 ~QG 𝐼)) → ((𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼) ↔ (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) |
107 | 95, 106 | mpbid 235 |
. . . . . . . 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 2739 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) =
(Base‘𝑅)) |
111 | | ovexd 7205 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → (𝑅 ~QG 𝐼) ∈ V) |
112 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CRing) |
113 | 109, 110,
111, 112 | qusbas 16921 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
((Base‘𝑅) /
(𝑅 ~QG
𝐼)) = (Base‘𝑄)) |
114 | 113 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → ((Base‘𝑅) / (𝑅 ~QG 𝐼)) = (Base‘𝑄)) |
115 | 108, 114 | eleqtrrd 2836 |
. . . . . . . . . 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 8381 |
. . . . . . . . 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 3199 |
. . . . . . 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 2836 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → 𝑎 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) |
122 | | elqsi 8381 |
. . . . . . . 8
⊢ (𝑎 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼)) → ∃𝑥 ∈ (Base‘𝑅)𝑎 = [𝑥](𝑅 ~QG 𝐼)) |
123 | 121, 122 | syl 17 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → ∃𝑥 ∈ (Base‘𝑅)𝑎 = [𝑥](𝑅 ~QG 𝐼)) |
124 | 119, 123 | r19.29a 3199 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(PrmIdeal‘𝑅)) ∧
𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) ∧ (𝑎(.r‘𝑄)𝑏) = (0g‘𝑄)) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄))) |
125 | 124 | ex 416 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ 𝑎 ∈ (Base‘𝑄)) ∧ 𝑏 ∈ (Base‘𝑄)) → ((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) |
126 | 125 | anasss 470 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) ∧ (𝑎 ∈ (Base‘𝑄) ∧ 𝑏 ∈ (Base‘𝑄))) → ((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) |
127 | 126 | ralrimivva 3103 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → ∀𝑎 ∈ (Base‘𝑄)∀𝑏 ∈ (Base‘𝑄)((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄)))) |
128 | 15, 78, 16 | isdomn 20186 |
. . 3
⊢ (𝑄 ∈ Domn ↔ (𝑄 ∈ NzRing ∧
∀𝑎 ∈
(Base‘𝑄)∀𝑏 ∈ (Base‘𝑄)((𝑎(.r‘𝑄)𝑏) = (0g‘𝑄) → (𝑎 = (0g‘𝑄) ∨ 𝑏 = (0g‘𝑄))))) |
129 | 57, 127, 128 | sylanbrc 586 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ Domn) |
130 | | isidom 20196 |
. 2
⊢ (𝑄 ∈ IDomn ↔ (𝑄 ∈ CRing ∧ 𝑄 ∈ Domn)) |
131 | 7, 129, 130 | sylanbrc 586 |
1
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) |