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

Metamath Proof Explorer

Theorem dvdsr02

Description: Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses dvdsr0.b ⊢ B = Base R
dvdsr0.d ⊢ ∥ ˙ = ∥ r ⁡ R
dvdsr0.z ⊢ 0 ˙ = 0 R
Assertion dvdsr02 ⊢ R ∈ Ring ∧ X ∈ B → 0 ˙ ∥ ˙ X ↔ X = 0 ˙

Proof

Step Hyp Ref Expression
1 dvdsr0.b ⊢ B = Base R
2 dvdsr0.d ⊢ ∥ ˙ = ∥ r ⁡ R
3 dvdsr0.z ⊢ 0 ˙ = 0 R
4 1 3 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ B
5 4 adantr ⊢ R ∈ Ring ∧ X ∈ B → 0 ˙ ∈ B
6 eqid ⊢ ⋅ R = ⋅ R
7 1 2 6 dvdsr2 ⊢ 0 ˙ ∈ B → 0 ˙ ∥ ˙ X ↔ ∃ x ∈ B x ⋅ R 0 ˙ = X
8 5 7 syl ⊢ R ∈ Ring ∧ X ∈ B → 0 ˙ ∥ ˙ X ↔ ∃ x ∈ B x ⋅ R 0 ˙ = X
9 1 6 3 ringrz ⊢ R ∈ Ring ∧ x ∈ B → x ⋅ R 0 ˙ = 0 ˙
10 9 eqeq1d ⊢ R ∈ Ring ∧ x ∈ B → x ⋅ R 0 ˙ = X ↔ 0 ˙ = X
11 eqcom ⊢ 0 ˙ = X ↔ X = 0 ˙
12 10 11 bitrdi ⊢ R ∈ Ring ∧ x ∈ B → x ⋅ R 0 ˙ = X ↔ X = 0 ˙
13 12 rexbidva ⊢ R ∈ Ring → ∃ x ∈ B x ⋅ R 0 ˙ = X ↔ ∃ x ∈ B X = 0 ˙
14 ringgrp ⊢ R ∈ Ring → R ∈ Grp
15 1 grpbn0 ⊢ R ∈ Grp → B ≠ ∅
16 r19.9rzv ⊢ B ≠ ∅ → X = 0 ˙ ↔ ∃ x ∈ B X = 0 ˙
17 14 15 16 3syl ⊢ R ∈ Ring → X = 0 ˙ ↔ ∃ x ∈ B X = 0 ˙
18 13 17 bitr4d ⊢ R ∈ Ring → ∃ x ∈ B x ⋅ R 0 ˙ = X ↔ X = 0 ˙
19 18 adantr ⊢ R ∈ Ring ∧ X ∈ B → ∃ x ∈ B x ⋅ R 0 ˙ = X ↔ X = 0 ˙
20 8 19 bitrd ⊢ R ∈ Ring ∧ X ∈ B → 0 ˙ ∥ ˙ X ↔ X = 0 ˙