| Step | Hyp | Ref
| Expression |
| 1 | | crngring 20242 |
. . 3
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 2 | 1 | ad2antrr 726 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝑅 ∈ Ring) |
| 3 | | simplr 769 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (LIdeal‘𝑅)) |
| 4 | | qsidom.1 |
. . . . . . . . 9
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
| 5 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → 𝐼 = (Base‘𝑅)) |
| 6 | 5 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (𝑅 ~QG 𝐼) = (𝑅 ~QG (Base‘𝑅))) |
| 7 | 6 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (𝑅 /s (𝑅 ~QG 𝐼)) = (𝑅 /s (𝑅 ~QG (Base‘𝑅)))) |
| 8 | 4, 7 | eqtrid 2789 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → 𝑄 = (𝑅 /s (𝑅 ~QG (Base‘𝑅)))) |
| 9 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (Base‘𝑄) = (Base‘(𝑅 /s (𝑅 ~QG (Base‘𝑅))))) |
| 10 | | ringgrp 20235 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 11 | 1, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Grp) |
| 12 | 11 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → 𝑅 ∈ Grp) |
| 13 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 14 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑅 /s (𝑅 ~QG
(Base‘𝑅))) = (𝑅 /s (𝑅 ~QG
(Base‘𝑅))) |
| 15 | 13, 14 | qustriv 33392 |
. . . . . . . 8
⊢ (𝑅 ∈ Grp →
(Base‘(𝑅
/s (𝑅
~QG (Base‘𝑅)))) = {(Base‘𝑅)}) |
| 16 | 12, 15 | syl 17 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (Base‘(𝑅 /s (𝑅 ~QG (Base‘𝑅)))) = {(Base‘𝑅)}) |
| 17 | 9, 16 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (Base‘𝑄) = {(Base‘𝑅)}) |
| 18 | 17 | fveq2d 6910 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (♯‘(Base‘𝑄)) =
(♯‘{(Base‘𝑅)})) |
| 19 | | fvex 6919 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
| 20 | | hashsng 14408 |
. . . . . 6
⊢
((Base‘𝑅)
∈ V → (♯‘{(Base‘𝑅)}) = 1) |
| 21 | 19, 20 | ax-mp 5 |
. . . . 5
⊢
(♯‘{(Base‘𝑅)}) = 1 |
| 22 | 18, 21 | eqtrdi 2793 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (♯‘(Base‘𝑄)) = 1) |
| 23 | | 1red 11262 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → 1 ∈ ℝ) |
| 24 | | isidom 20725 |
. . . . . . . . . 10
⊢ (𝑄 ∈ IDomn ↔ (𝑄 ∈ CRing ∧ 𝑄 ∈ Domn)) |
| 25 | 24 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑄 ∈ IDomn → 𝑄 ∈ Domn) |
| 26 | | domnnzr 20706 |
. . . . . . . . 9
⊢ (𝑄 ∈ Domn → 𝑄 ∈ NzRing) |
| 27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ (𝑄 ∈ IDomn → 𝑄 ∈ NzRing) |
| 28 | 27 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → 𝑄 ∈ NzRing) |
| 29 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑄) =
(Base‘𝑄) |
| 30 | 29 | isnzr2hash 20519 |
. . . . . . . 8
⊢ (𝑄 ∈ NzRing ↔ (𝑄 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑄)))) |
| 31 | 30 | simprbi 496 |
. . . . . . 7
⊢ (𝑄 ∈ NzRing → 1 <
(♯‘(Base‘𝑄))) |
| 32 | 28, 31 | syl 17 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → 1 <
(♯‘(Base‘𝑄))) |
| 33 | 23, 32 | gtned 11396 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → (♯‘(Base‘𝑄)) ≠ 1) |
| 34 | 33 | neneqd 2945 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ 𝐼 = (Base‘𝑅)) → ¬
(♯‘(Base‘𝑄)) = 1) |
| 35 | 22, 34 | pm2.65da 817 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → ¬ 𝐼 = (Base‘𝑅)) |
| 36 | 35 | neqned 2947 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ≠ (Base‘𝑅)) |
| 37 | 25 | ad4antlr 733 |
. . . . . . 7
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → 𝑄 ∈ Domn) |
| 38 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑅 ~QG 𝐼) ∈ V |
| 39 | 38 | ecelqsi 8813 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝑅) → [𝑥](𝑅 ~QG 𝐼) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) |
| 40 | 39 | ad3antlr 731 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → [𝑥](𝑅 ~QG 𝐼) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) |
| 41 | | simp-5l 785 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → 𝑅 ∈ CRing) |
| 42 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) |
| 43 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) =
(Base‘𝑅)) |
| 44 | | ovexd 7466 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → (𝑅 ~QG 𝐼) ∈ V) |
| 45 | | id 22 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CRing) |
| 46 | 42, 43, 44, 45 | qusbas 17590 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing →
((Base‘𝑅) /
(𝑅 ~QG
𝐼)) = (Base‘𝑄)) |
| 47 | 41, 46 | syl 17 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → ((Base‘𝑅) / (𝑅 ~QG 𝐼)) = (Base‘𝑄)) |
| 48 | 40, 47 | eleqtrd 2843 |
. . . . . . 7
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → [𝑥](𝑅 ~QG 𝐼) ∈ (Base‘𝑄)) |
| 49 | 38 | ecelqsi 8813 |
. . . . . . . . 9
⊢ (𝑦 ∈ (Base‘𝑅) → [𝑦](𝑅 ~QG 𝐼) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) |
| 50 | 49 | ad2antlr 727 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → [𝑦](𝑅 ~QG 𝐼) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝐼))) |
| 51 | 50, 47 | eleqtrd 2843 |
. . . . . . 7
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → [𝑦](𝑅 ~QG 𝐼) ∈ (Base‘𝑄)) |
| 52 | 41, 1, 10 | 3syl 18 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → 𝑅 ∈ Grp) |
| 53 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
| 54 | 53 | lidlsubg 21233 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (SubGrp‘𝑅)) |
| 55 | 1, 54 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (SubGrp‘𝑅)) |
| 56 | 55 | ad4antr 732 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → 𝐼 ∈ (SubGrp‘𝑅)) |
| 57 | | simpr 484 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) |
| 58 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑅 ~QG 𝐼) = (𝑅 ~QG 𝐼) |
| 59 | 58 | eqg0el 19201 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼 ↔ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼)) |
| 60 | 59 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼) |
| 61 | 52, 56, 57, 60 | syl21anc 838 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼) = 𝐼) |
| 62 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) |
| 63 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (Base‘𝑅) = (Base‘𝑅)) |
| 64 | 13, 58 | eqger 19196 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (SubGrp‘𝑅) → (𝑅 ~QG 𝐼) Er (Base‘𝑅)) |
| 65 | 55, 64 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑅 ~QG 𝐼) Er (Base‘𝑅)) |
| 66 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑅 ∈ CRing) |
| 67 | 53 | crng2idl 21291 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing →
(LIdeal‘𝑅) =
(2Ideal‘𝑅)) |
| 68 | 67 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → (𝐼 ∈ (LIdeal‘𝑅) ↔ 𝐼 ∈ (2Ideal‘𝑅))) |
| 69 | 68 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (2Ideal‘𝑅)) |
| 70 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
| 71 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 72 | 13, 58, 70, 71 | 2idlcpbl 21282 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → ((𝑔(𝑅 ~QG 𝐼)𝑒 ∧ ℎ(𝑅 ~QG 𝐼)𝑓) → (𝑔(.r‘𝑅)ℎ)(𝑅 ~QG 𝐼)(𝑒(.r‘𝑅)𝑓))) |
| 73 | 1, 69, 72 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑔(𝑅 ~QG 𝐼)𝑒 ∧ ℎ(𝑅 ~QG 𝐼)𝑓) → (𝑔(.r‘𝑅)ℎ)(𝑅 ~QG 𝐼)(𝑒(.r‘𝑅)𝑓))) |
| 74 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → 𝑅 ∈ Ring) |
| 75 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → 𝑒 ∈ (Base‘𝑅)) |
| 76 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → 𝑓 ∈ (Base‘𝑅)) |
| 77 | 13, 71 | ringcl 20247 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅)) → (𝑒(.r‘𝑅)𝑓) ∈ (Base‘𝑅)) |
| 78 | 74, 75, 76, 77 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑒 ∈ (Base‘𝑅) ∧ 𝑓 ∈ (Base‘𝑅))) → (𝑒(.r‘𝑅)𝑓) ∈ (Base‘𝑅)) |
| 79 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.r‘𝑄) = (.r‘𝑄) |
| 80 | 62, 63, 65, 66, 73, 78, 71, 79 | qusmulval 17600 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼)) |
| 81 | 80 | ad5ant134 1369 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = [(𝑥(.r‘𝑅)𝑦)](𝑅 ~QG 𝐼)) |
| 82 | | lidlnsg 21258 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
| 83 | 1, 82 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
| 84 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 85 | 4, 84 | qus0 19207 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
| 86 | 83, 85 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
| 87 | 13, 58, 84 | eqgid 19198 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (SubGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = 𝐼) |
| 88 | 55, 87 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = 𝐼) |
| 89 | 86, 88 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) →
(0g‘𝑄) =
𝐼) |
| 90 | 89 | ad4antr 732 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → (0g‘𝑄) = 𝐼) |
| 91 | 61, 81, 90 | 3eqtr4d 2787 |
. . . . . . 7
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = (0g‘𝑄)) |
| 92 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑄) = (0g‘𝑄) |
| 93 | 29, 79, 92 | domneq0 20708 |
. . . . . . . 8
⊢ ((𝑄 ∈ Domn ∧ [𝑥](𝑅 ~QG 𝐼) ∈ (Base‘𝑄) ∧ [𝑦](𝑅 ~QG 𝐼) ∈ (Base‘𝑄)) → (([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = (0g‘𝑄) ↔ ([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ∨ [𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄)))) |
| 94 | 93 | biimpa 476 |
. . . . . . 7
⊢ (((𝑄 ∈ Domn ∧ [𝑥](𝑅 ~QG 𝐼) ∈ (Base‘𝑄) ∧ [𝑦](𝑅 ~QG 𝐼) ∈ (Base‘𝑄)) ∧ ([𝑥](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑦](𝑅 ~QG 𝐼)) = (0g‘𝑄)) → ([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ∨ [𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄))) |
| 95 | 37, 48, 51, 91, 94 | syl31anc 1375 |
. . . . . 6
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → ([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ∨ [𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄))) |
| 96 | 89 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ↔ [𝑥](𝑅 ~QG 𝐼) = 𝐼)) |
| 97 | 66, 1, 10 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝑅 ∈ Grp) |
| 98 | 58 | eqg0el 19201 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑥 ∈ 𝐼)) |
| 99 | 97, 55, 98 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑥 ∈ 𝐼)) |
| 100 | 96, 99 | bitrd 279 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ↔ 𝑥 ∈ 𝐼)) |
| 101 | 89 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ([𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄) ↔ [𝑦](𝑅 ~QG 𝐼) = 𝐼)) |
| 102 | 58 | eqg0el 19201 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (SubGrp‘𝑅)) → ([𝑦](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑦 ∈ 𝐼)) |
| 103 | 97, 55, 102 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ([𝑦](𝑅 ~QG 𝐼) = 𝐼 ↔ 𝑦 ∈ 𝐼)) |
| 104 | 101, 103 | bitrd 279 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ([𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄) ↔ 𝑦 ∈ 𝐼)) |
| 105 | 100, 104 | orbi12d 919 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ∨ [𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄)) ↔ (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) |
| 106 | 105 | ad4antr 732 |
. . . . . 6
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → (([𝑥](𝑅 ~QG 𝐼) = (0g‘𝑄) ∨ [𝑦](𝑅 ~QG 𝐼) = (0g‘𝑄)) ↔ (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) |
| 107 | 95, 106 | mpbid 232 |
. . . . 5
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)) |
| 108 | 107 | ex 412 |
. . . 4
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝑄 ∈ IDomn) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) |
| 109 | 108 | anasss 466 |
. . 3
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) |
| 110 | 109 | ralrimivva 3202 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼))) |
| 111 | 13, 71 | prmidl2 33469 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝐼 ≠ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ 𝐼 → (𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼)))) → 𝐼 ∈ (PrmIdeal‘𝑅)) |
| 112 | 2, 3, 36, 110, 111 | syl22anc 839 |
1
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (PrmIdeal‘𝑅)) |