Metamath Proof Explorer


Theorem symgov

Description: The value of the group operation of the symmetric group on A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015)

Ref Expression
Hypotheses symgplusg.1 G = SymGrp A
symgplusg.2 B = Base G
symgplusg.3 + ˙ = + G
Assertion symgov X B Y B X + ˙ Y = X Y

Proof

Step Hyp Ref Expression
1 symgplusg.1 G = SymGrp A
2 symgplusg.2 B = Base G
3 symgplusg.3 + ˙ = + G
4 coexg X B Y B X Y V
5 coeq1 f = X f g = X g
6 coeq2 g = Y X g = X Y
7 1 2 3 symgplusg + ˙ = f B , g B f g
8 5 6 7 ovmpog X B Y B X Y V X + ˙ Y = X Y
9 4 8 mpd3an3 X B Y B X + ˙ Y = X Y