Theorem dmnnzd 38061

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

Hypotheses

Ref	Expression
dmnnzd.1	⊢ 𝐺 = (1st ‘𝑅)
dmnnzd.2	⊢ 𝐻 = (2nd ‘𝑅)
dmnnzd.3	⊢ 𝑋 = ran 𝐺
dmnnzd.4	⊢ 𝑍 = (GId‘𝐺)

Assertion

Ref	Expression
dmnnzd	⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍))

Proof of Theorem dmnnzd

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ran crn 5689  ‘cfv 6562  (class class class)co 7430  1^st c1st 8010  2^nd c2nd 8011  GIdcgi 30518  CRingOpsccring 37979  Dmncdmn 38033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-1o 8504  df-en 8984  df-grpo 30521  df-gid 30522  df-ginv 30523  df-ablo 30573  df-ass 37829  df-exid 37831  df-mgmOLD 37835  df-sgrOLD 37847  df-mndo 37853  df-rngo 37881  df-com2 37976  df-crngo 37980  df-idl 37996  df-pridl 37997  df-prrngo 38034  df-dmn 38035  df-igen 38046

This theorem is referenced by:  dmncan1  38062