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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) = 𝑍 ) ) → ( 𝐴 = 𝑍 ∨ 𝐵 = 𝑍 ) )