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=BaseR
Assertion isnzr2hash RNzRingRRing1<B

Proof

Step Hyp Ref Expression
1 isnzr2hash.b B=BaseR
2 eqid 1R=1R
3 eqid 0R=0R
4 2 3 isnzr RNzRingRRing1R0R
5 1 2 ringidcl RRing1RB
6 1 3 ring0cl RRing0RB
7 1xr 1*
8 7 a1i 1RB0RB1R0R1*
9 prex 1R0RV
10 hashxrcl 1R0RV1R0R*
11 9 10 mp1i 1RB0RB1R0R1R0R*
12 1 fvexi BV
13 hashxrcl BVB*
14 12 13 mp1i 1RB0RB1R0RB*
15 1lt2 1<2
16 hashprg 1RB0RB1R0R1R0R=2
17 16 biimpa 1RB0RB1R0R1R0R=2
18 15 17 breqtrrid 1RB0RB1R0R1<1R0R
19 simpl 1RB0RB1R0R1RB0RB
20 fvex 1RV
21 fvex 0RV
22 20 21 prss 1RB0RB1R0RB
23 19 22 sylib 1RB0RB1R0R1R0RB
24 hashss BV1R0RB1R0RB
25 12 23 24 sylancr 1RB0RB1R0R1R0RB
26 8 11 14 18 25 xrltletrd 1RB0RB1R0R1<B
27 26 ex 1RB0RB1R0R1<B
28 5 6 27 syl2anc RRing1R0R1<B
29 28 imdistani RRing1R0RRRing1<B
30 simpl RRing1<BRRing
31 1 2 3 ring1ne0 RRing1<B1R0R
32 30 31 jca RRing1<BRRing1R0R
33 29 32 impbii RRing1R0RRRing1<B
34 4 33 bitri RNzRingRRing1<B