Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
2 | | eqid 2193 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | 1, 2 | isnzr 13655 |
. 2
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅))) |
4 | | isnzr2.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
5 | 4, 1 | ringidcl 13494 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
6 | 5 | adantr 276 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → (1r‘𝑅) ∈ 𝐵) |
7 | 4, 2 | ring0cl 13495 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ 𝐵) |
8 | 7 | adantr 276 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → (0g‘𝑅) ∈ 𝐵) |
9 | | simpr 110 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → (1r‘𝑅) ≠
(0g‘𝑅)) |
10 | | df-ne 2365 |
. . . . . . . . 9
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
11 | | neeq1 2377 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) → (𝑥 ≠ 𝑦 ↔ (1r‘𝑅) ≠ 𝑦)) |
12 | 10, 11 | bitr3id 194 |
. . . . . . . 8
⊢ (𝑥 = (1r‘𝑅) → (¬ 𝑥 = 𝑦 ↔ (1r‘𝑅) ≠ 𝑦)) |
13 | | neeq2 2378 |
. . . . . . . 8
⊢ (𝑦 = (0g‘𝑅) →
((1r‘𝑅)
≠ 𝑦 ↔
(1r‘𝑅)
≠ (0g‘𝑅))) |
14 | 12, 13 | rspc2ev 2879 |
. . . . . . 7
⊢
(((1r‘𝑅) ∈ 𝐵 ∧ (0g‘𝑅) ∈ 𝐵 ∧ (1r‘𝑅) ≠
(0g‘𝑅))
→ ∃𝑥 ∈
𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦) |
15 | 6, 8, 9, 14 | syl3anc 1249 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦) |
16 | 15 | ex 115 |
. . . . 5
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)
≠ (0g‘𝑅) → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦)) |
17 | 4, 1, 2 | ring1eq0 13522 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((1r‘𝑅) = (0g‘𝑅) → 𝑥 = 𝑦)) |
18 | 17 | 3expb 1206 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((1r‘𝑅) = (0g‘𝑅) → 𝑥 = 𝑦)) |
19 | 18 | necon3bd 2407 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (¬ 𝑥 = 𝑦 → (1r‘𝑅) ≠
(0g‘𝑅))) |
20 | 19 | rexlimdvva 2619 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 → (1r‘𝑅) ≠
(0g‘𝑅))) |
21 | 16, 20 | impbid 129 |
. . . 4
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)
≠ (0g‘𝑅) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦)) |
22 | | simpl 109 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦)) → 𝑥 ∈ 𝐵) |
23 | | simprl 529 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦)) → 𝑦 ∈ 𝐵) |
24 | | simprr 531 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦)) → ¬ 𝑥 = 𝑦) |
25 | 22, 23, 24 | enpr2d 6862 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦)) → {𝑥, 𝑦} ≈ 2o) |
26 | 25 | adantl 277 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦))) → {𝑥, 𝑦} ≈ 2o) |
27 | 26 | ensymd 6828 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦))) → 2o ≈ {𝑥, 𝑦}) |
28 | | basfn 12663 |
. . . . . . . . . . . . 13
⊢ Base Fn
V |
29 | | elex 2771 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑅 ∈ V) |
30 | | funfvex 5563 |
. . . . . . . . . . . . . 14
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
31 | 30 | funfni 5346 |
. . . . . . . . . . . . 13
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
32 | 28, 29, 31 | sylancr 414 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ∈
V) |
33 | 4, 32 | eqeltrid 2280 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝐵 ∈ V) |
34 | | ssdomg 6823 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → ({𝑥, 𝑦} ⊆ 𝐵 → {𝑥, 𝑦} ≼ 𝐵)) |
35 | 33, 34 | syl 14 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → ({𝑥, 𝑦} ⊆ 𝐵 → {𝑥, 𝑦} ≼ 𝐵)) |
36 | 22, 23 | prssd 3777 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦)) → {𝑥, 𝑦} ⊆ 𝐵) |
37 | 35, 36 | impel 280 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦))) → {𝑥, 𝑦} ≼ 𝐵) |
38 | | endomtr 6835 |
. . . . . . . . 9
⊢
((2o ≈ {𝑥, 𝑦} ∧ {𝑥, 𝑦} ≼ 𝐵) → 2o ≼ 𝐵) |
39 | 27, 37, 38 | syl2anc 411 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦))) → 2o ≼ 𝐵) |
40 | 39 | anassrs 400 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ ¬ 𝑥 = 𝑦)) → 2o ≼ 𝐵) |
41 | 40 | rexlimdvaa 2612 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 → 2o ≼ 𝐵)) |
42 | 41 | rexlimdva 2611 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 → 2o ≼ 𝐵)) |
43 | | 2dom 6850 |
. . . . 5
⊢
(2o ≼ 𝐵 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦) |
44 | 42, 43 | impbid1 142 |
. . . 4
⊢ (𝑅 ∈ Ring →
(∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ↔ 2o ≼ 𝐵)) |
45 | 21, 44 | bitrd 188 |
. . 3
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)
≠ (0g‘𝑅) ↔ 2o ≼ 𝐵)) |
46 | 45 | pm5.32i 454 |
. 2
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅)) ↔ (𝑅 ∈ Ring ∧ 2o ≼
𝐵)) |
47 | 3, 46 | bitri 184 |
1
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 2o
≼ 𝐵)) |