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 \in Dmn \land (A \in X \land B \in X \land A H B = Z)) \to (A = Z \lor 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 \in Dmn \leftrightarrow (R \in CRingOps \land GId (H) \neq Z \land \forall a \in X \forall b \in X (a H b = Z \to (a = Z \lor b = Z)))$
7	6	simp3bi	$⊢ R \in Dmn \to \forall a \in X \forall b \in X (a H b = Z \to (a = Z \lor b = Z))$
8		oveq1	$⊢ a = A \to a H b = A H b$
9	8	eqeq1d	$⊢ a = A \to (a H b = Z \leftrightarrow A H b = Z)$
10		eqeq1	$⊢ a = A \to (a = Z \leftrightarrow A = Z)$
11	10	orbi1d	$⊢ a = A \to ((a = Z \lor b = Z) \leftrightarrow (A = Z \lor b = Z))$
12	9 11	imbi12d	$⊢ a = A \to ((a H b = Z \to (a = Z \lor b = Z)) \leftrightarrow (A H b = Z \to (A = Z \lor b = Z)))$
13		oveq2	$⊢ b = B \to A H b = A H B$
14	13	eqeq1d	$⊢ b = B \to (A H b = Z \leftrightarrow A H B = Z)$
15		eqeq1	$⊢ b = B \to (b = Z \leftrightarrow B = Z)$
16	15	orbi2d	$⊢ b = B \to ((A = Z \lor b = Z) \leftrightarrow (A = Z \lor B = Z))$
17	14 16	imbi12d	$⊢ b = B \to ((A H b = Z \to (A = Z \lor b = Z)) \leftrightarrow (A H B = Z \to (A = Z \lor B = Z)))$
18	12 17	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall a \in X \forall b \in X (a H b = Z \to (a = Z \lor b = Z)) \to (A H B = Z \to (A = Z \lor B = Z)))$
19	7 18	syl5com	$⊢ R \in Dmn \to ((A \in X \land B \in X) \to (A H B = Z \to (A = Z \lor B = Z)))$
20	19	expd	$⊢ R \in Dmn \to (A \in X \to (B \in X \to (A H B = Z \to (A = Z \lor B = Z))))$
21	20	3imp2	$⊢ (R \in Dmn \land (A \in X \land B \in X \land A H B = Z)) \to (A = Z \lor B = Z)$

Metamath Proof Explorer

Theorem dmnnzd

Proof