Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
grpcominv2
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( 𝑌 + ( 𝑁 ‘ 𝑋 ) ) = ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) )