Theorem grpcominv2

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

	Ref	Expression
Hypotheses	grpcominv.b	|- B = ( Base ` G )
	grpcominv.p	|- .+ = ( +g ` G )
	grpcominv.n	|- N = ( invg ` G )
	grpcominv.g	|- ( ph -> G e. Grp )
	grpcominv.x	|- ( ph -> X e. B )
	grpcominv.y	|- ( ph -> Y e. B )
	grpcominv.1	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )
Assertion	grpcominv2	|- ( ph -> ( Y .+ ( N ` X ) ) = ( ( N ` X ) .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		grpcominv.b	|- B = ( Base ` G )
2		grpcominv.p	|- .+ = ( +g ` G )
3		grpcominv.n	|- N = ( invg ` G )
4		grpcominv.g	|- ( ph -> G e. Grp )
5		grpcominv.x	|- ( ph -> X e. B )
6		grpcominv.y	|- ( ph -> Y e. B )
7		grpcominv.1	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )
8	7	eqcomd	|- ( ph -> ( Y .+ X ) = ( X .+ Y ) )
9	1 2 3 4 6 5 8	grpcominv1	|- ( ph -> ( Y .+ ( N ` X ) ) = ( ( N ` X ) .+ Y ) )