Metamath Proof Explorer

Theorem isnzr2hash

Description: Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 . (Contributed by AV, 14-Apr-2019)

Ref Expression
Hypothesis isnzr2hash.b ⊢ B = Base R
Assertion isnzr2hash ⊢ R ∈ NzRing ↔ R ∈ Ring ∧ 1 < B

Proof

Step Hyp Ref Expression
1 isnzr2hash.b ⊢ B = Base R
2 eqid ⊢ 1 R = 1 R
3 eqid ⊢ 0 R = 0 R
4 2 3 isnzr ⊢ R ∈ NzRing ↔ R ∈ Ring ∧ 1 R ≠ 0 R
5 1 2 ringidcl ⊢ R ∈ Ring → 1 R ∈ B
6 1 3 ring0cl ⊢ R ∈ Ring → 0 R ∈ B
7 1xr ⊢ 1 ∈ ℝ *
8 7 a1i ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 ∈ ℝ *
9 prex ⊢ 1 R 0 R ∈ V
10 hashxrcl ⊢ 1 R 0 R ∈ V → 1 R 0 R ∈ ℝ *
11 9 10 mp1i ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R 0 R ∈ ℝ *
12 1 fvexi ⊢ B ∈ V
13 hashxrcl ⊢ B ∈ V → B ∈ ℝ *
14 12 13 mp1i ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → B ∈ ℝ *
15 1lt2 ⊢ 1 < 2
16 hashprg ⊢ 1 R ∈ B ∧ 0 R ∈ B → 1 R ≠ 0 R ↔ 1 R 0 R = 2
17 16 biimpa ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R 0 R = 2
18 15 17 breqtrrid ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 < 1 R 0 R
19 fvex ⊢ 1 R ∈ V
20 fvex ⊢ 0 R ∈ V
21 19 20 prss ⊢ 1 R ∈ B ∧ 0 R ∈ B ↔ 1 R 0 R ⊆ B
22 21 birani ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R 0 R ⊆ B
23 hashss ⊢ B ∈ V ∧ 1 R 0 R ⊆ B → 1 R 0 R ≤ B
24 12 22 23 sylancr ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R 0 R ≤ B
25 8 11 14 18 24 xrltletrd ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 < B
26 25 ex ⊢ 1 R ∈ B ∧ 0 R ∈ B → 1 R ≠ 0 R → 1 < B
27 5 6 26 syl2anc ⊢ R ∈ Ring → 1 R ≠ 0 R → 1 < B
28 27 imdistani ⊢ R ∈ Ring ∧ 1 R ≠ 0 R → R ∈ Ring ∧ 1 < B
29 simpl ⊢ R ∈ Ring ∧ 1 < B → R ∈ Ring
30 1 2 3 ring1ne0 ⊢ R ∈ Ring ∧ 1 < B → 1 R ≠ 0 R
31 29 30 jca ⊢ R ∈ Ring ∧ 1 < B → R ∈ Ring ∧ 1 R ≠ 0 R
32 28 31 impbii ⊢ R ∈ Ring ∧ 1 R ≠ 0 R ↔ R ∈ Ring ∧ 1 < B
33 4 32 bitri ⊢ R ∈ NzRing ↔ R ∈ Ring ∧ 1 < B