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

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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
dmnnzd.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
dmnnzd.3 ⊢ 𝑋 = ran 𝐺
dmnnzd.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion dmnnzd ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) = 𝑍 ) ) → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 dmnnzd.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 dmnnzd.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 dmnnzd.3 ⊢ 𝑋 = ran 𝐺
4 dmnnzd.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 eqid ⊢ ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
6 1 2 3 4 5 isdmn3 ⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ CRingOps ∧ ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )
7 6 simp3bi ⊢ ( 𝑅 ∈ Dmn → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) )
8 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 𝐻 𝑏 ) = ( 𝐴 𝐻 𝑏 ) )
9 8 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 𝐻 𝑏 ) = 𝑍 ↔ ( 𝐴 𝐻 𝑏 ) = 𝑍 ) )
10 eqeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 = 𝑍 ↔ 𝐴 = 𝑍 ) )
11 10 orbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ↔ ( 𝐴 = 𝑍 ∨ 𝑏 = 𝑍 ) ) )
12 9 11 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ↔ ( ( 𝐴 𝐻 𝑏 ) = 𝑍 → ( 𝐴 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )
13 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 𝐻 𝑏 ) = ( 𝐴 𝐻 𝐵 ) )
14 13 eqeq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 𝐻 𝑏 ) = 𝑍 ↔ ( 𝐴 𝐻 𝐵 ) = 𝑍 ) )
15 eqeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 = 𝑍 ↔ 𝐵 = 𝑍 ) )
16 15 orbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 = 𝑍 ∨ 𝑏 = 𝑍 ) ↔ ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) ) )
17 14 16 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 𝐻 𝑏 ) = 𝑍 → ( 𝐴 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ↔ ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) ) ) )
18 12 17 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) ) ) )
19 7 18 syl5com ⊢ ( 𝑅 ∈ Dmn → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) ) ) )
20 19 expd ⊢ ( 𝑅 ∈ Dmn → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) ) ) ) )
21 20 3imp2 ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) = 𝑍 ) ) → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) )