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

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