grprcan

Description: Right cancellation law for groups. (Contributed by NM, 24-Aug-2011) (Proof shortened by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grprcan.b	$⊢ B = {Base}_{G}$
	grprcan.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	grprcan	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z = Y \underset{˙}{+} Z \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		grprcan.b	$⊢ B = {Base}_{G}$
2		grprcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		eqid	$⊢ 0_{G} = 0_{G}$
4	1 2 3	grpinvex	$⊢ (G \in Grp \land Z \in B) \to \exists y \in B y \underset{˙}{+} Z = 0_{G}$
5	4	3ad2antr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to \exists y \in B y \underset{˙}{+} Z = 0_{G}$
6		simprr	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X \underset{˙}{+} Z = Y \underset{˙}{+} Z$
7	6	oveq1d	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to (X \underset{˙}{+} Z) \underset{˙}{+} y = (Y \underset{˙}{+} Z) \underset{˙}{+} y$
8		simpll	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to G \in Grp$
9	1 2	grpass	$⊢ (G \in Grp \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{+} v) \underset{˙}{+} w = u \underset{˙}{+} (v \underset{˙}{+} w)$
10	8 9	sylan	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{+} v) \underset{˙}{+} w = u \underset{˙}{+} (v \underset{˙}{+} w)$
11		simplr1	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X \in B$
12		simplr3	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to Z \in B$
13		simprll	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to y \in B$
14	10 11 12 13	caovassd	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to (X \underset{˙}{+} Z) \underset{˙}{+} y = X \underset{˙}{+} (Z \underset{˙}{+} y)$
15		simplr2	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to Y \in B$
16	10 15 12 13	caovassd	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to (Y \underset{˙}{+} Z) \underset{˙}{+} y = Y \underset{˙}{+} (Z \underset{˙}{+} y)$
17	7 14 16	3eqtr3d	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X \underset{˙}{+} (Z \underset{˙}{+} y) = Y \underset{˙}{+} (Z \underset{˙}{+} y)$
18	1 2	grpcl	$⊢ (G \in Grp \land u \in B \land v \in B) \to u \underset{˙}{+} v \in B$
19	8 18	syl3an1	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land u \in B \land v \in B) \to u \underset{˙}{+} v \in B$
20	1 3	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
21	8 20	syl	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to 0_{G} \in B$
22	1 2 3	grplid	$⊢ (G \in Grp \land u \in B) \to 0_{G} \underset{˙}{+} u = u$
23	8 22	sylan	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land u \in B) \to 0_{G} \underset{˙}{+} u = u$
24	1 2 3	grpinvex	$⊢ (G \in Grp \land u \in B) \to \exists v \in B v \underset{˙}{+} u = 0_{G}$
25	8 24	sylan	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land u \in B) \to \exists v \in B v \underset{˙}{+} u = 0_{G}$
26		simpr	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land Z \in B) \to Z \in B$
27	13	adantr	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land Z \in B) \to y \in B$
28		simprlr	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to y \underset{˙}{+} Z = 0_{G}$
29	28	adantr	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land Z \in B) \to y \underset{˙}{+} Z = 0_{G}$
30	19 21 23 10 25 26 27 29	grpinva	$⊢ (((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \land Z \in B) \to Z \underset{˙}{+} y = 0_{G}$
31	12 30	mpdan	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to Z \underset{˙}{+} y = 0_{G}$
32	31	oveq2d	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X \underset{˙}{+} (Z \underset{˙}{+} y) = X \underset{˙}{+} 0_{G}$
33	31	oveq2d	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to Y \underset{˙}{+} (Z \underset{˙}{+} y) = Y \underset{˙}{+} 0_{G}$
34	17 32 33	3eqtr3d	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X \underset{˙}{+} 0_{G} = Y \underset{˙}{+} 0_{G}$
35	1 2 3 8 11	grpridd	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X \underset{˙}{+} 0_{G} = X$
36	1 2 3 8 15	grpridd	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to Y \underset{˙}{+} 0_{G} = Y$
37	34 35 36	3eqtr3d	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land ((y \in B \land y \underset{˙}{+} Z = 0_{G}) \land X \underset{˙}{+} Z = Y \underset{˙}{+} Z)) \to X = Y$
38	37	expr	$⊢ ((G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \land (y \in B \land y \underset{˙}{+} Z = 0_{G})) \to (X \underset{˙}{+} Z = Y \underset{˙}{+} Z \to X = Y)$
39	5 38	rexlimddv	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z = Y \underset{˙}{+} Z \to X = Y)$
40		oveq1	$⊢ X = Y \to X \underset{˙}{+} Z = Y \underset{˙}{+} Z$
41	39 40	impbid1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z = Y \underset{˙}{+} Z \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem grprcan

Proof