Step |
Hyp |
Ref |
Expression |
1 |
|
isnzr2.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
4 |
2 3
|
isnzr |
⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ) |
5 |
1 2
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 ) |
6 |
5
|
adantr |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 ) |
7 |
1 3
|
ring0cl |
⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ 𝐵 ) |
8 |
7
|
adantr |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝐵 ) |
9 |
|
simpr |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) |
10 |
|
df-ne |
⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 ) |
11 |
|
neeq1 |
⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( 𝑥 ≠ 𝑦 ↔ ( 1r ‘ 𝑅 ) ≠ 𝑦 ) ) |
12 |
10 11
|
bitr3id |
⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ¬ 𝑥 = 𝑦 ↔ ( 1r ‘ 𝑅 ) ≠ 𝑦 ) ) |
13 |
|
neeq2 |
⊢ ( 𝑦 = ( 0g ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ≠ 𝑦 ↔ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ) |
14 |
12 13
|
rspc2ev |
⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) |
15 |
6 8 9 14
|
syl3anc |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) |
16 |
15
|
ex |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) ) |
17 |
1 2 3
|
ring1eq0 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → 𝑥 = 𝑦 ) ) |
18 |
17
|
3expb |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → 𝑥 = 𝑦 ) ) |
19 |
18
|
necon3bd |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ¬ 𝑥 = 𝑦 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ) |
20 |
19
|
rexlimdvva |
⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ) |
21 |
16 20
|
impbid |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) ) |
22 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
23 |
|
1sdom |
⊢ ( 𝐵 ∈ V → ( 1o ≺ 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) ) |
24 |
22 23
|
ax-mp |
⊢ ( 1o ≺ 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) |
25 |
21 24
|
bitr4di |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ 1o ≺ 𝐵 ) ) |
26 |
|
1onn |
⊢ 1o ∈ ω |
27 |
|
sucdom |
⊢ ( 1o ∈ ω → ( 1o ≺ 𝐵 ↔ suc 1o ≼ 𝐵 ) ) |
28 |
26 27
|
ax-mp |
⊢ ( 1o ≺ 𝐵 ↔ suc 1o ≼ 𝐵 ) |
29 |
|
df-2o |
⊢ 2o = suc 1o |
30 |
29
|
breq1i |
⊢ ( 2o ≼ 𝐵 ↔ suc 1o ≼ 𝐵 ) |
31 |
28 30
|
bitr4i |
⊢ ( 1o ≺ 𝐵 ↔ 2o ≼ 𝐵 ) |
32 |
25 31
|
bitrdi |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ 2o ≼ 𝐵 ) ) |
33 |
32
|
pm5.32i |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Ring ∧ 2o ≼ 𝐵 ) ) |
34 |
4 33
|
bitri |
⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 2o ≼ 𝐵 ) ) |