Metamath Proof Explorer

Theorem rngoueqz

Description: Obsolete as of 23-Jan-2020. Use 0ring01eqbi instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses uznzr.1 ⊢ G = 1 st ⁡ R
uznzr.2 ⊢ H = 2 nd ⁡ R
uznzr.3 ⊢ Z = GId ⁡ G
uznzr.4 ⊢ U = GId ⁡ H
uznzr.5 ⊢ X = ran ⁡ G
Assertion rngoueqz ⊢ R ∈ RingOps → X ≈ 1 𝑜 ↔ U = Z

Proof

Step Hyp Ref Expression
1 uznzr.1 ⊢ G = 1 st ⁡ R
2 uznzr.2 ⊢ H = 2 nd ⁡ R
3 uznzr.3 ⊢ Z = GId ⁡ G
4 uznzr.4 ⊢ U = GId ⁡ H
5 uznzr.5 ⊢ X = ran ⁡ G
6 1 5 3 rngo0cl ⊢ R ∈ RingOps → Z ∈ X
7 en1eqsn ⊢ Z ∈ X ∧ X ≈ 1 𝑜 → X = Z
8 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
9 8 2 4 rngo1cl ⊢ R ∈ RingOps → U ∈ ran ⁡ G
10 eleq2 ⊢ X = Z → U ∈ X ↔ U ∈ Z
11 10 biimpd ⊢ X = Z → U ∈ X → U ∈ Z
12 elsni ⊢ U ∈ Z → U = Z
13 11 12 syl6com ⊢ U ∈ X → X = Z → U = Z
14 5 eqcomi ⊢ ran ⁡ G = X
15 13 14 eleq2s ⊢ U ∈ ran ⁡ G → X = Z → U = Z
16 9 15 syl ⊢ R ∈ RingOps → X = Z → U = Z
17 7 16 syl5com ⊢ Z ∈ X ∧ X ≈ 1 𝑜 → R ∈ RingOps → U = Z
18 17 ex ⊢ Z ∈ X → X ≈ 1 𝑜 → R ∈ RingOps → U = Z
19 18 com23 ⊢ Z ∈ X → R ∈ RingOps → X ≈ 1 𝑜 → U = Z
20 6 19 mpcom ⊢ R ∈ RingOps → X ≈ 1 𝑜 → U = Z
21 1 5 rngone0 ⊢ R ∈ RingOps → X ≠ ∅
22 oveq2 ⊢ U = Z → x H U = x H Z
23 22 ralrimivw ⊢ U = Z → ∀ x ∈ X x H U = x H Z
24 3 5 1 2 rngorz ⊢ R ∈ RingOps ∧ x ∈ X → x H Z = Z
25 24 ralrimiva ⊢ R ∈ RingOps → ∀ x ∈ X x H Z = Z
26 5 8 eqtri ⊢ X = ran ⁡ 1 st ⁡ R
27 2 26 4 rngoridm ⊢ R ∈ RingOps ∧ x ∈ X → x H U = x
28 27 ralrimiva ⊢ R ∈ RingOps → ∀ x ∈ X x H U = x
29 r19.26 ⊢ ∀ x ∈ X x H U = x ∧ x H U = x H Z ↔ ∀ x ∈ X x H U = x ∧ ∀ x ∈ X x H U = x H Z
30 r19.26 ⊢ ∀ x ∈ X x H U = x ∧ x H U = x H Z ∧ x H Z = Z ↔ ∀ x ∈ X x H U = x ∧ x H U = x H Z ∧ ∀ x ∈ X x H Z = Z
31 eqtr ⊢ x = x H U ∧ x H U = x H Z → x = x H Z
32 eqtr ⊢ x = x H Z ∧ x H Z = Z → x = Z
33 32 ex ⊢ x = x H Z → x H Z = Z → x = Z
34 31 33 syl ⊢ x = x H U ∧ x H U = x H Z → x H Z = Z → x = Z
35 34 ex ⊢ x = x H U → x H U = x H Z → x H Z = Z → x = Z
36 35 eqcoms ⊢ x H U = x → x H U = x H Z → x H Z = Z → x = Z
37 36 imp31 ⊢ x H U = x ∧ x H U = x H Z ∧ x H Z = Z → x = Z
38 37 ralimi ⊢ ∀ x ∈ X x H U = x ∧ x H U = x H Z ∧ x H Z = Z → ∀ x ∈ X x = Z
39 eqsn ⊢ X ≠ ∅ → X = Z ↔ ∀ x ∈ X x = Z
40 ensn1g ⊢ Z ∈ X → Z ≈ 1 𝑜
41 6 40 syl ⊢ R ∈ RingOps → Z ≈ 1 𝑜
42 breq1 ⊢ X = Z → X ≈ 1 𝑜 ↔ Z ≈ 1 𝑜
43 41 42 imbitrrid ⊢ X = Z → R ∈ RingOps → X ≈ 1 𝑜
44 39 43 biimtrrdi ⊢ X ≠ ∅ → ∀ x ∈ X x = Z → R ∈ RingOps → X ≈ 1 𝑜
45 44 com3l ⊢ ∀ x ∈ X x = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
46 38 45 syl ⊢ ∀ x ∈ X x H U = x ∧ x H U = x H Z ∧ x H Z = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
47 30 46 sylbir ⊢ ∀ x ∈ X x H U = x ∧ x H U = x H Z ∧ ∀ x ∈ X x H Z = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
48 47 ex ⊢ ∀ x ∈ X x H U = x ∧ x H U = x H Z → ∀ x ∈ X x H Z = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
49 29 48 sylbir ⊢ ∀ x ∈ X x H U = x ∧ ∀ x ∈ X x H U = x H Z → ∀ x ∈ X x H Z = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
50 49 ex ⊢ ∀ x ∈ X x H U = x → ∀ x ∈ X x H U = x H Z → ∀ x ∈ X x H Z = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
51 50 com24 ⊢ ∀ x ∈ X x H U = x → R ∈ RingOps → ∀ x ∈ X x H Z = Z → ∀ x ∈ X x H U = x H Z → X ≠ ∅ → X ≈ 1 𝑜
52 28 51 mpcom ⊢ R ∈ RingOps → ∀ x ∈ X x H Z = Z → ∀ x ∈ X x H U = x H Z → X ≠ ∅ → X ≈ 1 𝑜
53 25 52 mpd ⊢ R ∈ RingOps → ∀ x ∈ X x H U = x H Z → X ≠ ∅ → X ≈ 1 𝑜
54 23 53 syl5com ⊢ U = Z → R ∈ RingOps → X ≠ ∅ → X ≈ 1 𝑜
55 54 com13 ⊢ X ≠ ∅ → R ∈ RingOps → U = Z → X ≈ 1 𝑜
56 21 55 mpcom ⊢ R ∈ RingOps → U = Z → X ≈ 1 𝑜
57 20 56 impbid ⊢ R ∈ RingOps → X ≈ 1 𝑜 ↔ U = Z