Metamath Proof Explorer


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 ( 𝜑 → ( 𝑌 + ( 𝑁𝑋 ) ) = ( ( 𝑁𝑋 ) + 𝑌 ) )