Metamath Proof Explorer

Theorem 0ringnnzr

Description: A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019)

Ref Expression
Assertion 0ringnnzr ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 1 ltnri ⊢ ¬ 1 < 1
3 breq2 ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 → ( 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ↔ 1 < 1 ) )
4 2 3 mtbiri ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 → ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
5 4 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
6 5 intnand ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
7 6 ex ⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 → ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) ) )
8 ianor ⊢ ( ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) ↔ ( ¬ 𝑅 ∈ Ring ∨ ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
9 pm2.21 ⊢ ( ¬ 𝑅 ∈ Ring → ( 𝑅 ∈ Ring → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
10 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
11 hashxrcl ⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℝ* )
12 10 11 ax-mp ⊢ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℝ*
13 1xr ⊢ 1 ∈ ℝ*
14 xrlenlt ⊢ ( ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
15 12 13 14 mp2an ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
16 15 bicomi ⊢ ( ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 )
17 simpr ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 )
18 1nn0 ⊢ 1 ∈ ℕ0
19 hashbnd ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ 1 ∈ ℕ0 ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( Base ‘ 𝑅 ) ∈ Fin )
20 10 18 17 19 mp3an12i ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( Base ‘ 𝑅 ) ∈ Fin )
21 hashcl ⊢ ( ( Base ‘ 𝑅 ) ∈ Fin → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 )
22 simpr ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 )
23 hasheq0 ⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 0 ↔ ( Base ‘ 𝑅 ) = ∅ ) )
24 10 23 mp1i ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 0 ↔ ( Base ‘ 𝑅 ) = ∅ ) )
25 24 biimpd ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 0 → ( Base ‘ 𝑅 ) = ∅ ) )
26 25 necon3d ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 → ( ( Base ‘ 𝑅 ) ≠ ∅ → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 0 ) )
27 26 impcom ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 0 )
28 elnnne0 ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ ↔ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 0 ) )
29 22 27 28 sylanbrc ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ )
30 29 ex ⊢ ( ( Base ‘ 𝑅 ) ≠ ∅ → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ ) )
31 30 adantr ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ ) )
32 21 31 syl5com ⊢ ( ( Base ‘ 𝑅 ) ∈ Fin → ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ ) )
33 20 32 mpcom ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ )
34 nnle1eq1 ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
35 33 34 syl ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
36 17 35 mpbid ⊢ ( ( ( Base ‘ 𝑅 ) ≠ ∅ ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
37 36 ex ⊢ ( ( Base ‘ 𝑅 ) ≠ ∅ → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
38 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
39 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
40 39 grpbn0 ⊢ ( 𝑅 ∈ Grp → ( Base ‘ 𝑅 ) ≠ ∅ )
41 38 40 syl ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ≠ ∅ )
42 37 41 syl11 ⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≤ 1 → ( 𝑅 ∈ Ring → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
43 16 42 sylbi ⊢ ( ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) → ( 𝑅 ∈ Ring → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
44 9 43 jaoi ⊢ ( ( ¬ 𝑅 ∈ Ring ∨ ¬ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) → ( 𝑅 ∈ Ring → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
45 8 44 sylbi ⊢ ( ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) → ( 𝑅 ∈ Ring → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
46 45 com12 ⊢ ( 𝑅 ∈ Ring → ( ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
47 7 46 impbid ⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) ) )
48 39 isnzr2hash ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
49 48 bicomi ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) ↔ 𝑅 ∈ NzRing )
50 49 notbii ⊢ ( ¬ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) ↔ ¬ 𝑅 ∈ NzRing )
51 47 50 bitrdi ⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )