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

Metamath Proof Explorer

Theorem 01eq0ringOLD

Description: Obsolete version of 01eq0ring as of 23-Feb-2025. (Contributed by AV, 16-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 0ring.b ⊢ B = Base R
0ring.0 ⊢ 0 ˙ = 0 R
0ring01eq.1 ⊢ 1 ˙ = 1 R
Assertion 01eq0ringOLD ⊢ R ∈ Ring ∧ 0 ˙ = 1 ˙ → B = 0 ˙

Proof

Step Hyp Ref Expression
1 0ring.b ⊢ B = Base R
2 0ring.0 ⊢ 0 ˙ = 0 R
3 0ring01eq.1 ⊢ 1 ˙ = 1 R
4 1 fvexi ⊢ B ∈ V
5 hashv01gt1 ⊢ B ∈ V → B = 0 ∨ B = 1 ∨ 1 < B
6 4 5 ax-mp ⊢ B = 0 ∨ B = 1 ∨ 1 < B
7 hasheq0 ⊢ B ∈ V → B = 0 ↔ B = ∅
8 4 7 ax-mp ⊢ B = 0 ↔ B = ∅
9 ne0i ⊢ 0 ˙ ∈ B → B ≠ ∅
10 eqneqall ⊢ B = ∅ → B ≠ ∅ → B ≠ 1 → 0 ˙ ≠ 1 ˙
11 9 10 syl5com ⊢ 0 ˙ ∈ B → B = ∅ → B ≠ 1 → 0 ˙ ≠ 1 ˙
12 8 11 biimtrid ⊢ 0 ˙ ∈ B → B = 0 → B ≠ 1 → 0 ˙ ≠ 1 ˙
13 1 2 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ B
14 12 13 syl11 ⊢ B = 0 → R ∈ Ring → B ≠ 1 → 0 ˙ ≠ 1 ˙
15 eqneqall ⊢ B = 1 → B ≠ 1 → 0 ˙ ≠ 1 ˙
16 15 a1d ⊢ B = 1 → R ∈ Ring → B ≠ 1 → 0 ˙ ≠ 1 ˙
17 1 3 2 ring1ne0 ⊢ R ∈ Ring ∧ 1 < B → 1 ˙ ≠ 0 ˙
18 17 necomd ⊢ R ∈ Ring ∧ 1 < B → 0 ˙ ≠ 1 ˙
19 18 ex ⊢ R ∈ Ring → 1 < B → 0 ˙ ≠ 1 ˙
20 19 a1i ⊢ B ≠ 1 → R ∈ Ring → 1 < B → 0 ˙ ≠ 1 ˙
21 20 com13 ⊢ 1 < B → R ∈ Ring → B ≠ 1 → 0 ˙ ≠ 1 ˙
22 14 16 21 3jaoi ⊢ B = 0 ∨ B = 1 ∨ 1 < B → R ∈ Ring → B ≠ 1 → 0 ˙ ≠ 1 ˙
23 6 22 ax-mp ⊢ R ∈ Ring → B ≠ 1 → 0 ˙ ≠ 1 ˙
24 23 necon4d ⊢ R ∈ Ring → 0 ˙ = 1 ˙ → B = 1
25 24 imp ⊢ R ∈ Ring ∧ 0 ˙ = 1 ˙ → B = 1
26 1 2 0ring ⊢ R ∈ Ring ∧ B = 1 → B = 0 ˙
27 25 26 syldan ⊢ R ∈ Ring ∧ 0 ˙ = 1 ˙ → B = 0 ˙