Step | Hyp | Ref
| Expression |
1 | | uznzr.1 |
. . . 4
⊢ 𝐺 = (1st ‘𝑅) |
2 | | uznzr.5 |
. . . 4
⊢ 𝑋 = ran 𝐺 |
3 | | uznzr.3 |
. . . 4
⊢ 𝑍 = (GId‘𝐺) |
4 | 1, 2, 3 | rngo0cl 35814 |
. . 3
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋) |
5 | | en1eqsn 8904 |
. . . . . 6
⊢ ((𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o) → 𝑋 = {𝑍}) |
6 | 1 | rneqi 5806 |
. . . . . . . 8
⊢ ran 𝐺 = ran (1st
‘𝑅) |
7 | | uznzr.2 |
. . . . . . . 8
⊢ 𝐻 = (2nd ‘𝑅) |
8 | | uznzr.4 |
. . . . . . . 8
⊢ 𝑈 = (GId‘𝐻) |
9 | 6, 7, 8 | rngo1cl 35834 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ ran 𝐺) |
10 | | eleq2 2826 |
. . . . . . . . . 10
⊢ (𝑋 = {𝑍} → (𝑈 ∈ 𝑋 ↔ 𝑈 ∈ {𝑍})) |
11 | 10 | biimpd 232 |
. . . . . . . . 9
⊢ (𝑋 = {𝑍} → (𝑈 ∈ 𝑋 → 𝑈 ∈ {𝑍})) |
12 | | elsni 4558 |
. . . . . . . . 9
⊢ (𝑈 ∈ {𝑍} → 𝑈 = 𝑍) |
13 | 11, 12 | syl6com 37 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑋 → (𝑋 = {𝑍} → 𝑈 = 𝑍)) |
14 | 2 | eqcomi 2746 |
. . . . . . . 8
⊢ ran 𝐺 = 𝑋 |
15 | 13, 14 | eleq2s 2856 |
. . . . . . 7
⊢ (𝑈 ∈ ran 𝐺 → (𝑋 = {𝑍} → 𝑈 = 𝑍)) |
16 | 9, 15 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → (𝑋 = {𝑍} → 𝑈 = 𝑍)) |
17 | 5, 16 | syl5com 31 |
. . . . 5
⊢ ((𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o) → (𝑅 ∈ RingOps → 𝑈 = 𝑍)) |
18 | 17 | ex 416 |
. . . 4
⊢ (𝑍 ∈ 𝑋 → (𝑋 ≈ 1o → (𝑅 ∈ RingOps → 𝑈 = 𝑍))) |
19 | 18 | com23 86 |
. . 3
⊢ (𝑍 ∈ 𝑋 → (𝑅 ∈ RingOps → (𝑋 ≈ 1o → 𝑈 = 𝑍))) |
20 | 4, 19 | mpcom 38 |
. 2
⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o →
𝑈 = 𝑍)) |
21 | 1, 2 | rngone0 35806 |
. . 3
⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅) |
22 | | oveq2 7221 |
. . . . . 6
⊢ (𝑈 = 𝑍 → (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) |
23 | 22 | ralrimivw 3106 |
. . . . 5
⊢ (𝑈 = 𝑍 → ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) |
24 | 3, 2, 1, 7 | rngorz 35818 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑥𝐻𝑍) = 𝑍) |
25 | 24 | ralrimiva 3105 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍) |
26 | 2, 6 | eqtri 2765 |
. . . . . . . . 9
⊢ 𝑋 = ran (1st
‘𝑅) |
27 | 7, 26, 8 | rngoridm 35833 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑥𝐻𝑈) = 𝑥) |
28 | 27 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = 𝑥) |
29 | | r19.26 3092 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ↔ (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍))) |
30 | | r19.26 3092 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) ↔ (∀𝑥 ∈ 𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍)) |
31 | | eqtr 2760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = (𝑥𝐻𝑈) ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → 𝑥 = (𝑥𝐻𝑍)) |
32 | | eqtr 2760 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = (𝑥𝐻𝑍) ∧ (𝑥𝐻𝑍) = 𝑍) → 𝑥 = 𝑍) |
33 | 32 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍)) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = (𝑥𝐻𝑈) ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍)) |
35 | 34 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑥𝐻𝑈) → ((𝑥𝐻𝑈) = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍))) |
36 | 35 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥𝐻𝑈) = 𝑥 → ((𝑥𝐻𝑈) = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍))) |
37 | 36 | imp31 421 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → 𝑥 = 𝑍) |
38 | 37 | ralimi 3083 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → ∀𝑥 ∈ 𝑋 𝑥 = 𝑍) |
39 | | eqsn 4742 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ≠ ∅ → (𝑋 = {𝑍} ↔ ∀𝑥 ∈ 𝑋 𝑥 = 𝑍)) |
40 | | ensn1g 8696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍 ∈ 𝑋 → {𝑍} ≈ 1o) |
41 | 4, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ RingOps → {𝑍} ≈
1o) |
42 | | breq1 5056 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 = {𝑍} → (𝑋 ≈ 1o ↔ {𝑍} ≈
1o)) |
43 | 41, 42 | syl5ibr 249 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = {𝑍} → (𝑅 ∈ RingOps → 𝑋 ≈ 1o)) |
44 | 39, 43 | syl6bir 257 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ≠ ∅ →
(∀𝑥 ∈ 𝑋 𝑥 = 𝑍 → (𝑅 ∈ RingOps → 𝑋 ≈ 1o))) |
45 | 44 | com3l 89 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑋 𝑥 = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) |
46 | 38, 45 | syl 17 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) |
47 | 30, 46 | sylbir 238 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍) → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) |
48 | 47 | ex 416 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))) |
49 | 29, 48 | sylbir 238 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑋 (𝑥𝐻𝑈) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))) |
50 | 49 | ex 416 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 (𝑥𝐻𝑈) = 𝑥 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))) |
51 | 50 | com24 95 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 (𝑥𝐻𝑈) = 𝑥 → (𝑅 ∈ RingOps → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))) |
52 | 28, 51 | mpcom 38 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
(∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))) |
53 | 25, 52 | mpd 15 |
. . . . 5
⊢ (𝑅 ∈ RingOps →
(∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) |
54 | 23, 53 | syl5com 31 |
. . . 4
⊢ (𝑈 = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) |
55 | 54 | com13 88 |
. . 3
⊢ (𝑋 ≠ ∅ → (𝑅 ∈ RingOps → (𝑈 = 𝑍 → 𝑋 ≈ 1o))) |
56 | 21, 55 | mpcom 38 |
. 2
⊢ (𝑅 ∈ RingOps → (𝑈 = 𝑍 → 𝑋 ≈ 1o)) |
57 | 20, 56 | impbid 215 |
1
⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔
𝑈 = 𝑍)) |