Proof of Theorem qsnzr
| Step | Hyp | Ref
| Expression |
| 1 | | qsnzr.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 2 | | qsnzr.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
| 3 | | qsnzr.q |
. . . 4
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
| 4 | | eqid 2737 |
. . . 4
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
| 5 | 3, 4 | qusring 21285 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → 𝑄 ∈ Ring) |
| 6 | 1, 2, 5 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑄 ∈ Ring) |
| 7 | | ringgrp 20235 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 8 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 9 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 10 | 8, 9 | grpinvid 19017 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp →
((invg‘𝑅)‘(0g‘𝑅)) = (0g‘𝑅)) |
| 11 | 1, 7, 10 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝑅)‘(0g‘𝑅)) = (0g‘𝑅)) |
| 12 | 11 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 →
(((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(1r‘𝑅))) |
| 13 | | qsnzr.1 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
| 14 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 15 | 1, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 16 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 17 | 13, 16 | ringidcl 20262 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
| 18 | 1, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
| 19 | 13, 14, 8, 15, 18 | grplidd 18987 |
. . . . . . . 8
⊢ (𝜑 →
((0g‘𝑅)(+g‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
| 20 | 12, 19 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 →
(((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
| 21 | 2 | 2idllidld 21264 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
| 22 | | qsnzr.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ≠ 𝐵) |
| 23 | 13, 16 | pridln1 33471 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ (1r‘𝑅) ∈ 𝐼) |
| 24 | 1, 21, 22, 23 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ¬
(1r‘𝑅)
∈ 𝐼) |
| 25 | 20, 24 | eqneltrd 2861 |
. . . . . 6
⊢ (𝜑 → ¬
(((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼) |
| 26 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → 𝑅 ∈ Ring) |
| 27 | | lidlnsg 21258 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
| 28 | 1, 21, 27 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
| 29 | | nsgsubg 19176 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) → 𝐼 ∈ (SubGrp‘𝑅)) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) |
| 31 | 13 | subgss 19145 |
. . . . . . . . 9
⊢ (𝐼 ∈ (SubGrp‘𝑅) → 𝐼 ⊆ 𝐵) |
| 32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
| 33 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → 𝐼 ⊆ 𝐵) |
| 34 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑅 ~QG 𝐼) = (𝑅 ~QG 𝐼) |
| 35 | 13, 34 | eqger 19196 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (SubGrp‘𝑅) → (𝑅 ~QG 𝐼) Er 𝐵) |
| 36 | 30, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ~QG 𝐼) Er 𝐵) |
| 37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (𝑅 ~QG 𝐼) Er 𝐵) |
| 38 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) |
| 39 | 37, 38 | ersym 8757 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (0g‘𝑅)(𝑅 ~QG 𝐼)(1r‘𝑅)) |
| 40 | 13, 9, 14, 34 | eqgval 19195 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵) → ((0g‘𝑅)(𝑅 ~QG 𝐼)(1r‘𝑅) ↔ ((0g‘𝑅) ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝐵 ∧ (((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼))) |
| 41 | 40 | biimpa 476 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵) ∧ (0g‘𝑅)(𝑅 ~QG 𝐼)(1r‘𝑅)) → ((0g‘𝑅) ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝐵 ∧ (((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼)) |
| 42 | 41 | simp3d 1145 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵) ∧ (0g‘𝑅)(𝑅 ~QG 𝐼)(1r‘𝑅)) → (((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼) |
| 43 | 26, 33, 39, 42 | syl21anc 838 |
. . . . . 6
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼) |
| 44 | 25, 43 | mtand 816 |
. . . . 5
⊢ (𝜑 → ¬
(1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) |
| 45 | 36, 18 | erth 8796 |
. . . . 5
⊢ (𝜑 →
((1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅) ↔ [(1r‘𝑅)](𝑅 ~QG 𝐼) = [(0g‘𝑅)](𝑅 ~QG 𝐼))) |
| 46 | 44, 45 | mtbid 324 |
. . . 4
⊢ (𝜑 → ¬
[(1r‘𝑅)](𝑅 ~QG 𝐼) = [(0g‘𝑅)](𝑅 ~QG 𝐼)) |
| 47 | 46 | neqned 2947 |
. . 3
⊢ (𝜑 →
[(1r‘𝑅)](𝑅 ~QG 𝐼) ≠ [(0g‘𝑅)](𝑅 ~QG 𝐼)) |
| 48 | 3, 4, 16 | qus1 21284 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → (𝑄 ∈ Ring ∧
[(1r‘𝑅)](𝑅 ~QG 𝐼) = (1r‘𝑄))) |
| 49 | 1, 2, 48 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑄 ∈ Ring ∧
[(1r‘𝑅)](𝑅 ~QG 𝐼) = (1r‘𝑄))) |
| 50 | 49 | simprd 495 |
. . 3
⊢ (𝜑 →
[(1r‘𝑅)](𝑅 ~QG 𝐼) = (1r‘𝑄)) |
| 51 | 3, 8 | qus0 19207 |
. . . 4
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
| 52 | 28, 51 | syl 17 |
. . 3
⊢ (𝜑 →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
| 53 | 47, 50, 52 | 3netr3d 3017 |
. 2
⊢ (𝜑 → (1r‘𝑄) ≠
(0g‘𝑄)) |
| 54 | | eqid 2737 |
. . 3
⊢
(1r‘𝑄) = (1r‘𝑄) |
| 55 | | eqid 2737 |
. . 3
⊢
(0g‘𝑄) = (0g‘𝑄) |
| 56 | 54, 55 | isnzr 20514 |
. 2
⊢ (𝑄 ∈ NzRing ↔ (𝑄 ∈ Ring ∧
(1r‘𝑄)
≠ (0g‘𝑄))) |
| 57 | 6, 53, 56 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑄 ∈ NzRing) |