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
⊢ B = Base G
grpcominv.p
⊢ + ˙ = + G
grpcominv.n
⊢ N = inv g ⁡ G
grpcominv.g
⊢ φ → G ∈ Grp
grpcominv.x
⊢ φ → X ∈ B
grpcominv.y
⊢ φ → Y ∈ B
grpcominv.1
⊢ φ → X + ˙ Y = Y + ˙ X
Assertion
grpcominv2
⊢ φ → Y + ˙ N ⁡ X = N ⁡ X + ˙ Y
Proof
Step
Hyp
Ref
Expression
1
grpcominv.b
⊢ B = Base G
2
grpcominv.p
⊢ + ˙ = + G
3
grpcominv.n
⊢ N = inv g ⁡ G
4
grpcominv.g
⊢ φ → G ∈ Grp
5
grpcominv.x
⊢ φ → X ∈ B
6
grpcominv.y
⊢ φ → Y ∈ B
7
grpcominv.1
⊢ φ → X + ˙ Y = Y + ˙ X
8
7
eqcomd
⊢ φ → Y + ˙ X = X + ˙ Y
9
1 2 3 4 6 5 8
grpcominv1
⊢ φ → Y + ˙ N ⁡ X = N ⁡ X + ˙ Y