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 simpl ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R ∈ B ∧ 0 R ∈ B
20 fvex ⊢ 1 R ∈ V
21 fvex ⊢ 0 R ∈ V
22 20 21 prss ⊢ 1 R ∈ B ∧ 0 R ∈ B ↔ 1 R 0 R ⊆ B
23 19 22 sylib ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R 0 R ⊆ B
24 hashss ⊢ B ∈ V ∧ 1 R 0 R ⊆ B → 1 R 0 R ≤ B
25 12 23 24 sylancr ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 R 0 R ≤ B
26 8 11 14 18 25 xrltletrd ⊢ 1 R ∈ B ∧ 0 R ∈ B ∧ 1 R ≠ 0 R → 1 < B
27 26 ex ⊢ 1 R ∈ B ∧ 0 R ∈ B → 1 R ≠ 0 R → 1 < B
28 5 6 27 syl2anc ⊢ R ∈ Ring → 1 R ≠ 0 R → 1 < B
29 28 imdistani ⊢ R ∈ Ring ∧ 1 R ≠ 0 R → R ∈ Ring ∧ 1 < B
30 simpl ⊢ R ∈ Ring ∧ 1 < B → R ∈ Ring
31 1 2 3 ring1ne0 ⊢ R ∈ Ring ∧ 1 < B → 1 R ≠ 0 R
32 30 31 jca ⊢ R ∈ Ring ∧ 1 < B → R ∈ Ring ∧ 1 R ≠ 0 R
33 29 32 impbii ⊢ R ∈ Ring ∧ 1 R ≠ 0 R ↔ R ∈ Ring ∧ 1 < B
34 4 33 bitri ⊢ R ∈ NzRing ↔ R ∈ Ring ∧ 1 < B