grplcan

Description: Left cancellation law for groups. (Contributed by NM, 25-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		grplcan.b	$⊢ B = {Base}_{G}$
2		grplcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		oveq2	$⊢ Z \underset{˙}{+} X = Z \underset{˙}{+} Y \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X) = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y)$
4	3	adantl	$⊢ (((G \in Grp \land X \in B) \land (Y \in B \land Z \in B)) \land Z \underset{˙}{+} X = Z \underset{˙}{+} Y) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X) = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y)$
5		eqid	$⊢ 0_{G} = 0_{G}$
6		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
7	1 2 5 6	grplinv	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \underset{˙}{+} Z = 0_{G}$
8	7	adantlr	$⊢ ((G \in Grp \land X \in B) \land Z \in B) \to {inv}_{g} (G) (Z) \underset{˙}{+} Z = 0_{G}$
9	8	oveq1d	$⊢ ((G \in Grp \land X \in B) \land Z \in B) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} X = 0_{G} \underset{˙}{+} X$
10	1 6	grpinvcl	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \in B$
11	10	adantrl	$⊢ (G \in Grp \land (X \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \in B$
12		simprr	$⊢ (G \in Grp \land (X \in B \land Z \in B)) \to Z \in B$
13		simprl	$⊢ (G \in Grp \land (X \in B \land Z \in B)) \to X \in B$
14	11 12 13	3jca	$⊢ (G \in Grp \land (X \in B \land Z \in B)) \to ({inv}_{g} (G) (Z) \in B \land Z \in B \land X \in B)$
15	1 2	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (Z) \in B \land Z \in B \land X \in B)) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} X = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X)$
16	14 15	syldan	$⊢ (G \in Grp \land (X \in B \land Z \in B)) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} X = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X)$
17	16	anassrs	$⊢ ((G \in Grp \land X \in B) \land Z \in B) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} X = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X)$
18	1 2 5	grplid	$⊢ (G \in Grp \land X \in B) \to 0_{G} \underset{˙}{+} X = X$
19	18	adantr	$⊢ ((G \in Grp \land X \in B) \land Z \in B) \to 0_{G} \underset{˙}{+} X = X$
20	9 17 19	3eqtr3d	$⊢ ((G \in Grp \land X \in B) \land Z \in B) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X) = X$
21	20	adantrl	$⊢ ((G \in Grp \land X \in B) \land (Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X) = X$
22	21	adantr	$⊢ (((G \in Grp \land X \in B) \land (Y \in B \land Z \in B)) \land Z \underset{˙}{+} X = Z \underset{˙}{+} Y) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} X) = X$
23	7	adantrl	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \underset{˙}{+} Z = 0_{G}$
24	23	oveq1d	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} Y = 0_{G} \underset{˙}{+} Y$
25	10	adantrl	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \in B$
26		simprr	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to Z \in B$
27		simprl	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to Y \in B$
28	25 26 27	3jca	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to ({inv}_{g} (G) (Z) \in B \land Z \in B \land Y \in B)$
29	1 2	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (Z) \in B \land Z \in B \land Y \in B)) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} Y = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y)$
30	28 29	syldan	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to ({inv}_{g} (G) (Z) \underset{˙}{+} Z) \underset{˙}{+} Y = {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y)$
31	1 2 5	grplid	$⊢ (G \in Grp \land Y \in B) \to 0_{G} \underset{˙}{+} Y = Y$
32	31	adantrr	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to 0_{G} \underset{˙}{+} Y = Y$
33	24 30 32	3eqtr3d	$⊢ (G \in Grp \land (Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y) = Y$
34	33	adantlr	$⊢ ((G \in Grp \land X \in B) \land (Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y) = Y$
35	34	adantr	$⊢ (((G \in Grp \land X \in B) \land (Y \in B \land Z \in B)) \land Z \underset{˙}{+} X = Z \underset{˙}{+} Y) \to {inv}_{g} (G) (Z) \underset{˙}{+} (Z \underset{˙}{+} Y) = Y$
36	4 22 35	3eqtr3d	$⊢ (((G \in Grp \land X \in B) \land (Y \in B \land Z \in B)) \land Z \underset{˙}{+} X = Z \underset{˙}{+} Y) \to X = Y$
37	36	exp53	$⊢ G \in Grp \to (X \in B \to (Y \in B \to (Z \in B \to (Z \underset{˙}{+} X = Z \underset{˙}{+} Y \to X = Y))))$
38	37	3imp2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{+} X = Z \underset{˙}{+} Y \to X = Y)$
39		oveq2	$⊢ X = Y \to Z \underset{˙}{+} X = Z \underset{˙}{+} Y$
40	38 39	impbid1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{+} X = Z \underset{˙}{+} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem grplcan

Proof