Metamath Proof Explorer

Theorem 0rngo

Description: In a ring, 0 = 1 iff the ring contains only 0 . (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Hypotheses 0ring.1 ⊢ G = 1 st ⁡ R
0ring.2 ⊢ H = 2 nd ⁡ R
0ring.3 ⊢ X = ran ⁡ G
0ring.4 ⊢ Z = GId ⁡ G
0ring.5 ⊢ U = GId ⁡ H
Assertion 0rngo ⊢ R ∈ RingOps → Z = U ↔ X = Z

Proof

Step Hyp Ref Expression
1 0ring.1 ⊢ G = 1 st ⁡ R
2 0ring.2 ⊢ H = 2 nd ⁡ R
3 0ring.3 ⊢ X = ran ⁡ G
4 0ring.4 ⊢ Z = GId ⁡ G
5 0ring.5 ⊢ U = GId ⁡ H
6 4 fvexi ⊢ Z ∈ V
7 6 snid ⊢ Z ∈ Z
8 eleq1 ⊢ Z = U → Z ∈ Z ↔ U ∈ Z
9 7 8 mpbii ⊢ Z = U → U ∈ Z
10 1 4 0idl ⊢ R ∈ RingOps → Z ∈ Idl ⁡ R
11 1 2 3 5 1idl ⊢ R ∈ RingOps ∧ Z ∈ Idl ⁡ R → U ∈ Z ↔ Z = X
12 10 11 mpdan ⊢ R ∈ RingOps → U ∈ Z ↔ Z = X
13 9 12 syl5ib ⊢ R ∈ RingOps → Z = U → Z = X
14 eqcom ⊢ Z = X ↔ X = Z
15 13 14 syl6ib ⊢ R ∈ RingOps → Z = U → X = Z
16 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
17 3 16 eqtri ⊢ X = ran ⁡ 1 st ⁡ R
18 17 2 5 rngo1cl ⊢ R ∈ RingOps → U ∈ X
19 eleq2 ⊢ X = Z → U ∈ X ↔ U ∈ Z
20 elsni ⊢ U ∈ Z → U = Z
21 20 eqcomd ⊢ U ∈ Z → Z = U
22 19 21 syl6bi ⊢ X = Z → U ∈ X → Z = U
23 18 22 syl5com ⊢ R ∈ RingOps → X = Z → Z = U
24 15 23 impbid ⊢ R ∈ RingOps → Z = U ↔ X = Z