This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpasscan1

Description: An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008) (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	grpasscan1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} (N (X) \underset{˙}{+} Y) = Y$

Proof

Step	Hyp	Ref	Expression
1		grplcan.b	$⊢ B = {Base}_{G}$
2		grplcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpasscan1.n	$⊢ N = {inv}_{g} (G)$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	1 2 4 3	grprinv	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} N (X) = 0_{G}$
6	5	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} N (X) = 0_{G}$
7	6	oveq1d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} N (X)) \underset{˙}{+} Y = 0_{G} \underset{˙}{+} Y$
8	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
9	1 2	grpass	$⊢ (G \in Grp \land (X \in B \land N (X) \in B \land Y \in B)) \to (X \underset{˙}{+} N (X)) \underset{˙}{+} Y = X \underset{˙}{+} (N (X) \underset{˙}{+} Y)$
10	9	3exp2	$⊢ G \in Grp \to (X \in B \to (N (X) \in B \to (Y \in B \to (X \underset{˙}{+} N (X)) \underset{˙}{+} Y = X \underset{˙}{+} (N (X) \underset{˙}{+} Y))))$
11	10	imp	$⊢ (G \in Grp \land X \in B) \to (N (X) \in B \to (Y \in B \to (X \underset{˙}{+} N (X)) \underset{˙}{+} Y = X \underset{˙}{+} (N (X) \underset{˙}{+} Y)))$
12	8 11	mpd	$⊢ (G \in Grp \land X \in B) \to (Y \in B \to (X \underset{˙}{+} N (X)) \underset{˙}{+} Y = X \underset{˙}{+} (N (X) \underset{˙}{+} Y))$
13	12	3impia	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} N (X)) \underset{˙}{+} Y = X \underset{˙}{+} (N (X) \underset{˙}{+} Y)$
14	1 2 4	grplid	$⊢ (G \in Grp \land Y \in B) \to 0_{G} \underset{˙}{+} Y = Y$
15	14	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to 0_{G} \underset{˙}{+} Y = Y$
16	7 13 15	3eqtr3d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} (N (X) \underset{˙}{+} Y) = Y$