grpcominv1

Description: If two elements commute, then they commute with each other's inverses (case of the first element commuting with the inverse of the second element). (Contributed by SN, 29-Jan-2025)

	Ref	Expression
Hypotheses	grpcominv.b	$⊢ B = {Base}_{G}$
	grpcominv.p	$⊢ \underset{˙}{+} = +_{G}$
	grpcominv.n	$⊢ N = {inv}_{g} (G)$
	grpcominv.g	$⊢ φ \to G \in Grp$
	grpcominv.x	$⊢ φ \to X \in B$
	grpcominv.y	$⊢ φ \to Y \in B$
	grpcominv.1	$⊢ φ \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
Assertion	grpcominv1	$⊢ φ \to X \underset{˙}{+} N (Y) = N (Y) \underset{˙}{+} X$

Proof

Step	Hyp	Ref	Expression
1		grpcominv.b	$⊢ B = {Base}_{G}$
2		grpcominv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpcominv.n	$⊢ N = {inv}_{g} (G)$
4		grpcominv.g	$⊢ φ \to G \in Grp$
5		grpcominv.x	$⊢ φ \to X \in B$
6		grpcominv.y	$⊢ φ \to Y \in B$
7		grpcominv.1	$⊢ φ \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
8	1 3 4 6	grpinvcld	$⊢ φ \to N (Y) \in B$
9	1 2 4 8 6 5	grpassd	$⊢ φ \to (N (Y) \underset{˙}{+} Y) \underset{˙}{+} X = N (Y) \underset{˙}{+} (Y \underset{˙}{+} X)$
10		eqid	$⊢ 0_{G} = 0_{G}$
11	1 2 10 3 4 6	grplinvd	$⊢ φ \to N (Y) \underset{˙}{+} Y = 0_{G}$
12	11	oveq1d	$⊢ φ \to (N (Y) \underset{˙}{+} Y) \underset{˙}{+} X = 0_{G} \underset{˙}{+} X$
13	1 2 10 4 5	grplidd	$⊢ φ \to 0_{G} \underset{˙}{+} X = X$
14	12 13	eqtr2d	$⊢ φ \to X = (N (Y) \underset{˙}{+} Y) \underset{˙}{+} X$
15	7	oveq2d	$⊢ φ \to N (Y) \underset{˙}{+} (X \underset{˙}{+} Y) = N (Y) \underset{˙}{+} (Y \underset{˙}{+} X)$
16	9 14 15	3eqtr4rd	$⊢ φ \to N (Y) \underset{˙}{+} (X \underset{˙}{+} Y) = X$
17	1 2 4 8 5 6	grpassd	$⊢ φ \to (N (Y) \underset{˙}{+} X) \underset{˙}{+} Y = N (Y) \underset{˙}{+} (X \underset{˙}{+} Y)$
18	1 2 3 4 5 6	grpasscan2d	$⊢ φ \to (X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = X$
19	16 17 18	3eqtr4rd	$⊢ φ \to (X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = (N (Y) \underset{˙}{+} X) \underset{˙}{+} Y$
20	1 2 4 5 8	grpcld	$⊢ φ \to X \underset{˙}{+} N (Y) \in B$
21	1 2 4 8 5	grpcld	$⊢ φ \to N (Y) \underset{˙}{+} X \in B$
22	1 2	grprcan	$⊢ (G \in Grp \land (X \underset{˙}{+} N (Y) \in B \land N (Y) \underset{˙}{+} X \in B \land Y \in B)) \to ((X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = (N (Y) \underset{˙}{+} X) \underset{˙}{+} Y \leftrightarrow X \underset{˙}{+} N (Y) = N (Y) \underset{˙}{+} X)$
23	4 20 21 6 22	syl13anc	$⊢ φ \to ((X \underset{˙}{+} N (Y)) \underset{˙}{+} Y = (N (Y) \underset{˙}{+} X) \underset{˙}{+} Y \leftrightarrow X \underset{˙}{+} N (Y) = N (Y) \underset{˙}{+} X)$
24	19 23	mpbid	$⊢ φ \to X \underset{˙}{+} N (Y) = N (Y) \underset{˙}{+} X$

Metamath Proof Explorer

Theorem grpcominv1

Proof