Metamath Proof Explorer

Theorem dmnnzd

Description: A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses dmnnzd.1 ⊢ G = 1 st ⁡ R
dmnnzd.2 ⊢ H = 2 nd ⁡ R
dmnnzd.3 ⊢ X = ran ⁡ G
dmnnzd.4 ⊢ Z = GId ⁡ G
Assertion dmnnzd ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ A H B = Z → A = Z ∨ B = Z

Proof

Step Hyp Ref Expression
1 dmnnzd.1 ⊢ G = 1 st ⁡ R
2 dmnnzd.2 ⊢ H = 2 nd ⁡ R
3 dmnnzd.3 ⊢ X = ran ⁡ G
4 dmnnzd.4 ⊢ Z = GId ⁡ G
5 eqid ⊢ GId ⁡ H = GId ⁡ H
6 1 2 3 4 5 isdmn3 ⊢ R ∈ Dmn ↔ R ∈ CRingOps ∧ GId ⁡ H ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
7 6 simp3bi ⊢ R ∈ Dmn → ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
8 oveq1 ⊢ a = A → a H b = A H b
9 8 eqeq1d ⊢ a = A → a H b = Z ↔ A H b = Z
10 eqeq1 ⊢ a = A → a = Z ↔ A = Z
11 10 orbi1d ⊢ a = A → a = Z ∨ b = Z ↔ A = Z ∨ b = Z
12 9 11 imbi12d ⊢ a = A → a H b = Z → a = Z ∨ b = Z ↔ A H b = Z → A = Z ∨ b = Z
13 oveq2 ⊢ b = B → A H b = A H B
14 13 eqeq1d ⊢ b = B → A H b = Z ↔ A H B = Z
15 eqeq1 ⊢ b = B → b = Z ↔ B = Z
16 15 orbi2d ⊢ b = B → A = Z ∨ b = Z ↔ A = Z ∨ B = Z
17 14 16 imbi12d ⊢ b = B → A H b = Z → A = Z ∨ b = Z ↔ A H B = Z → A = Z ∨ B = Z
18 12 17 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z → A H B = Z → A = Z ∨ B = Z
19 7 18 syl5com ⊢ R ∈ Dmn → A ∈ X ∧ B ∈ X → A H B = Z → A = Z ∨ B = Z
20 19 expd ⊢ R ∈ Dmn → A ∈ X → B ∈ X → A H B = Z → A = Z ∨ B = Z
21 20 3imp2 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ A H B = Z → A = Z ∨ B = Z