Metamath Proof Explorer


Theorem isnzr2

Description: Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypothesis isnzr2.b 𝐵 = ( Base ‘ 𝑅 )
Assertion isnzr2 ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 2o𝐵 ) )

Proof

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𝐵 ) )