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 2733 |
. . . 4
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
5 | 3, 4 | qusring 20860 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → 𝑄 ∈ Ring) |
6 | 1, 2, 5 | syl2anc 585 |
. 2
⊢ (𝜑 → 𝑄 ∈ Ring) |
7 | | ringgrp 20052 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
8 | | eqid 2733 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
9 | | eqid 2733 |
. . . . . . . . . . 11
⊢
(invg‘𝑅) = (invg‘𝑅) |
10 | 8, 9 | grpinvid 18880 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp →
((invg‘𝑅)‘(0g‘𝑅)) = (0g‘𝑅)) |
11 | 1, 7, 10 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝑅)‘(0g‘𝑅)) = (0g‘𝑅)) |
12 | 11 | oveq1d 7419 |
. . . . . . . 8
⊢ (𝜑 →
(((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(1r‘𝑅))) |
13 | | qsnzr.1 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
14 | | eqid 2733 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
15 | 1, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Grp) |
16 | | eqid 2733 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
17 | 13, 16 | ringidcl 20073 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
18 | 1, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
19 | 13, 14, 8, 15, 18 | grplidd 18850 |
. . . . . . . 8
⊢ (𝜑 →
((0g‘𝑅)(+g‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
20 | 12, 19 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 →
(((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
21 | 2 | 2idllidld 20853 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
22 | | qsnzr.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ≠ 𝐵) |
23 | 13, 16 | pridln1 32519 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ (1r‘𝑅) ∈ 𝐼) |
24 | 1, 21, 22, 23 | syl3anc 1372 |
. . . . . . 7
⊢ (𝜑 → ¬
(1r‘𝑅)
∈ 𝐼) |
25 | 20, 24 | eqneltrd 2854 |
. . . . . 6
⊢ (𝜑 → ¬
(((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼) |
26 | 1 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → 𝑅 ∈ Ring) |
27 | | lidlnsg 32522 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
28 | 1, 21, 27 | syl2anc 585 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
29 | | nsgsubg 19032 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) → 𝐼 ∈ (SubGrp‘𝑅)) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) |
31 | 13 | subgss 19001 |
. . . . . . . . 9
⊢ (𝐼 ∈ (SubGrp‘𝑅) → 𝐼 ⊆ 𝐵) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
33 | 32 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → 𝐼 ⊆ 𝐵) |
34 | | eqid 2733 |
. . . . . . . . . . 11
⊢ (𝑅 ~QG 𝐼) = (𝑅 ~QG 𝐼) |
35 | 13, 34 | eqger 19052 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (SubGrp‘𝑅) → (𝑅 ~QG 𝐼) Er 𝐵) |
36 | 30, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ~QG 𝐼) Er 𝐵) |
37 | 36 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (𝑅 ~QG 𝐼) Er 𝐵) |
38 | | simpr 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) |
39 | 37, 38 | ersym 8711 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (0g‘𝑅)(𝑅 ~QG 𝐼)(1r‘𝑅)) |
40 | 13, 9, 14, 34 | eqgval 19051 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵) → ((0g‘𝑅)(𝑅 ~QG 𝐼)(1r‘𝑅) ↔ ((0g‘𝑅) ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝐵 ∧ (((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼))) |
41 | 40 | biimpa 478 |
. . . . . . . 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 837 |
. . . . . 6
⊢ ((𝜑 ∧ (1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) → (((invg‘𝑅)‘(0g‘𝑅))(+g‘𝑅)(1r‘𝑅)) ∈ 𝐼) |
44 | 25, 43 | mtand 815 |
. . . . 5
⊢ (𝜑 → ¬
(1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅)) |
45 | 36, 18 | erth 8748 |
. . . . 5
⊢ (𝜑 →
((1r‘𝑅)(𝑅 ~QG 𝐼)(0g‘𝑅) ↔ [(1r‘𝑅)](𝑅 ~QG 𝐼) = [(0g‘𝑅)](𝑅 ~QG 𝐼))) |
46 | 44, 45 | mtbid 324 |
. . . 4
⊢ (𝜑 → ¬
[(1r‘𝑅)](𝑅 ~QG 𝐼) = [(0g‘𝑅)](𝑅 ~QG 𝐼)) |
47 | 46 | neqned 2948 |
. . 3
⊢ (𝜑 →
[(1r‘𝑅)](𝑅 ~QG 𝐼) ≠ [(0g‘𝑅)](𝑅 ~QG 𝐼)) |
48 | 3, 4, 16 | qus1 20859 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → (𝑄 ∈ Ring ∧
[(1r‘𝑅)](𝑅 ~QG 𝐼) = (1r‘𝑄))) |
49 | 1, 2, 48 | syl2anc 585 |
. . . 4
⊢ (𝜑 → (𝑄 ∈ Ring ∧
[(1r‘𝑅)](𝑅 ~QG 𝐼) = (1r‘𝑄))) |
50 | 49 | simprd 497 |
. . 3
⊢ (𝜑 →
[(1r‘𝑅)](𝑅 ~QG 𝐼) = (1r‘𝑄)) |
51 | 3, 8 | qus0 19062 |
. . . 4
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
52 | 28, 51 | syl 17 |
. . 3
⊢ (𝜑 →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
53 | 47, 50, 52 | 3netr3d 3018 |
. 2
⊢ (𝜑 → (1r‘𝑄) ≠
(0g‘𝑄)) |
54 | | eqid 2733 |
. . 3
⊢
(1r‘𝑄) = (1r‘𝑄) |
55 | | eqid 2733 |
. . 3
⊢
(0g‘𝑄) = (0g‘𝑄) |
56 | 54, 55 | isnzr 20282 |
. 2
⊢ (𝑄 ∈ NzRing ↔ (𝑄 ∈ Ring ∧
(1r‘𝑄)
≠ (0g‘𝑄))) |
57 | 6, 53, 56 | sylanbrc 584 |
1
⊢ (𝜑 → 𝑄 ∈ NzRing) |