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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpcominv.p	⊢ + = ( +g ‘ 𝐺 )
	grpcominv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grpcominv.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	grpcominv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	grpcominv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	grpcominv.1	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
Assertion	grpcominv2	⊢ ( 𝜑 → ( 𝑌 + ( 𝑁 ‘ 𝑋 ) ) = ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		grpcominv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpcominv.p	⊢ + = ( +g ‘ 𝐺 )
3		grpcominv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		grpcominv.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
5		grpcominv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		grpcominv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		grpcominv.1	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
8	7	eqcomd	⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) = ( 𝑋 + 𝑌 ) )
9	1 2 3 4 6 5 8	grpcominv1	⊢ ( 𝜑 → ( 𝑌 + ( 𝑁 ‘ 𝑋 ) ) = ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) )