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) (Revised by AV, 30-Mar-2024)

Ref Expression
Hypotheses symgov.1 G=SymGrpA
symgov.2 B=BaseG
symgov.3 +˙=+G
Assertion symgov XBYBX+˙Y=XY

Proof

Step Hyp Ref Expression
1 symgov.1 G=SymGrpA
2 symgov.2 B=BaseG
3 symgov.3 +˙=+G
4 eqid AA=AA
5 1 4 3 symgplusg +˙=fAA,gAAfg
6 5 a1i XBYB+˙=fAA,gAAfg
7 simpl f=Xg=Yf=X
8 simpr f=Xg=Yg=Y
9 7 8 coeq12d f=Xg=Yfg=XY
10 9 adantl XBYBf=Xg=Yfg=XY
11 1 2 symgbasmap XBXAA
12 11 adantr XBYBXAA
13 1 2 symgbasmap YBYAA
14 13 adantl XBYBYAA
15 coexg XBYBXYV
16 6 10 12 14 15 ovmpod XBYBX+˙Y=XY