This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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