dmncan1

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011)

	Ref	Expression
Hypotheses	dmncan.1	$⊢ G = 1^{st} (R)$
	dmncan.2	$⊢ H = 2^{nd} (R)$
	dmncan.3	$⊢ X = ran G$
	dmncan.4	$⊢ Z = GId (G)$
Assertion	dmncan1	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to (A H B = A H C \to B = C)$

Proof

Step	Hyp	Ref	Expression
1		dmncan.1	$⊢ G = 1^{st} (R)$
2		dmncan.2	$⊢ H = 2^{nd} (R)$
3		dmncan.3	$⊢ X = ran G$
4		dmncan.4	$⊢ Z = GId (G)$
5		dmnrngo	$⊢ R \in Dmn \to R \in RingOps$
6		eqid	$⊢ /_{g} (G) = /_{g} (G)$
7	1 2 3 6	rngosubdi	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B /_{g} (G) C) = (A H B) /_{g} (G) (A H C)$
8	5 7	sylan	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to A H (B /_{g} (G) C) = (A H B) /_{g} (G) (A H C)$
9	8	adantr	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to A H (B /_{g} (G) C) = (A H B) /_{g} (G) (A H C)$
10	9	eqeq1d	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to (A H (B /_{g} (G) C) = Z \leftrightarrow (A H B) /_{g} (G) (A H C) = Z)$
11	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
12	5 11	syl	$⊢ R \in Dmn \to G \in GrpOp$
13	3 6	grpodivcl	$⊢ (G \in GrpOp \land B \in X \land C \in X) \to B /_{g} (G) C \in X$
14	13	3expb	$⊢ (G \in GrpOp \land (B \in X \land C \in X)) \to B /_{g} (G) C \in X$
15	12 14	sylan	$⊢ (R \in Dmn \land (B \in X \land C \in X)) \to B /_{g} (G) C \in X$
16	15	adantlr	$⊢ ((R \in Dmn \land A \in X) \land (B \in X \land C \in X)) \to B /_{g} (G) C \in X$
17	1 2 3 4	dmnnzd	$⊢ (R \in Dmn \land (A \in X \land B /_{g} (G) C \in X \land A H (B /_{g} (G) C) = Z)) \to (A = Z \lor B /_{g} (G) C = Z)$
18	17	3exp2	$⊢ R \in Dmn \to (A \in X \to (B /_{g} (G) C \in X \to (A H (B /_{g} (G) C) = Z \to (A = Z \lor B /_{g} (G) C = Z))))$
19	18	imp31	$⊢ ((R \in Dmn \land A \in X) \land B /_{g} (G) C \in X) \to (A H (B /_{g} (G) C) = Z \to (A = Z \lor B /_{g} (G) C = Z))$
20	16 19	syldan	$⊢ ((R \in Dmn \land A \in X) \land (B \in X \land C \in X)) \to (A H (B /_{g} (G) C) = Z \to (A = Z \lor B /_{g} (G) C = Z))$
21	20	exp43	$⊢ R \in Dmn \to (A \in X \to (B \in X \to (C \in X \to (A H (B /_{g} (G) C) = Z \to (A = Z \lor B /_{g} (G) C = Z)))))$
22	21	3imp2	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to (A H (B /_{g} (G) C) = Z \to (A = Z \lor B /_{g} (G) C = Z))$
23		neor	$⊢ (A = Z \lor B /_{g} (G) C = Z) \leftrightarrow (A \neq Z \to B /_{g} (G) C = Z)$
24	22 23	imbitrdi	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to (A H (B /_{g} (G) C) = Z \to (A \neq Z \to B /_{g} (G) C = Z))$
25	24	com23	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to (A \neq Z \to (A H (B /_{g} (G) C) = Z \to B /_{g} (G) C = Z))$
26	25	imp	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to (A H (B /_{g} (G) C) = Z \to B /_{g} (G) C = Z)$
27	10 26	sylbird	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to ((A H B) /_{g} (G) (A H C) = Z \to B /_{g} (G) C = Z)$
28	12	adantr	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to G \in GrpOp$
29	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A H B \in X$
30	29	3adant3r3	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H B \in X$
31	5 30	sylan	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to A H B \in X$
32	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land C \in X) \to A H C \in X$
33	32	3adant3r2	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H C \in X$
34	5 33	sylan	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to A H C \in X$
35	3 4 6	grpoeqdivid	$⊢ (G \in GrpOp \land A H B \in X \land A H C \in X) \to (A H B = A H C \leftrightarrow (A H B) /_{g} (G) (A H C) = Z)$
36	28 31 34 35	syl3anc	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to (A H B = A H C \leftrightarrow (A H B) /_{g} (G) (A H C) = Z)$
37	36	adantr	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to (A H B = A H C \leftrightarrow (A H B) /_{g} (G) (A H C) = Z)$
38	3 4 6	grpoeqdivid	$⊢ (G \in GrpOp \land B \in X \land C \in X) \to (B = C \leftrightarrow B /_{g} (G) C = Z)$
39	38	3expb	$⊢ (G \in GrpOp \land (B \in X \land C \in X)) \to (B = C \leftrightarrow B /_{g} (G) C = Z)$
40	12 39	sylan	$⊢ (R \in Dmn \land (B \in X \land C \in X)) \to (B = C \leftrightarrow B /_{g} (G) C = Z)$
41	40	3adantr1	$⊢ (R \in Dmn \land (A \in X \land B \in X \land C \in X)) \to (B = C \leftrightarrow B /_{g} (G) C = Z)$
42	41	adantr	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to (B = C \leftrightarrow B /_{g} (G) C = Z)$
43	27 37 42	3imtr4d	$⊢ ((R \in Dmn \land (A \in X \land B \in X \land C \in X)) \land A \neq Z) \to (A H B = A H C \to B = C)$

Metamath Proof Explorer

Theorem dmncan1

Proof