grpasscan2

Description: An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	grplcan.b	$⊢ B = {Base}_{G}$
	grplcan.p	$⊢ \underset{˙}{+} = +_{G}$
	grpasscan1.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpasscan2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = X$

Step	Hyp	Ref	Expression
1		grplcan.b	$⊢ B = {Base}_{G}$
2		grplcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpasscan1.n	$⊢ N = {inv}_{g} (G)$
4		simp1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to G \in Grp$
5		simp2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \in B$
6	1 3	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to N (Y) \in B$
7	6	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (Y) \in B$
8		simp3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \in B$
9	1 2	grpass	$⊢ (G \in Grp \land (X \in B \land N (Y) \in B \land Y \in B)) \to (X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = X \underset{˙}{+} (N (Y) \underset{˙}{+} Y)$
10	4 5 7 8 9	syl13anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = X \underset{˙}{+} (N (Y) \underset{˙}{+} Y)$
11		eqid	$⊢ 0_{G} = 0_{G}$
12	1 2 11 3	grplinv	$⊢ (G \in Grp \land Y \in B) \to N (Y) \underset{˙}{+} Y = 0_{G}$
13	12	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (Y) \underset{˙}{+} Y = 0_{G}$
14	13	oveq2d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} (N (Y) \underset{˙}{+} Y) = X \underset{˙}{+} 0_{G}$
15	1 2 11	grprid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} 0_{G} = X$
16	15	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} 0_{G} = X$
17	10 14 16	3eqtrd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = X$

Metamath Proof Explorer