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

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 = ( SymGrp ` A )
symgov.2 
|- B = ( Base ` G )
symgov.3 
|- .+ = ( +g ` G )
Assertion symgov 
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )

Proof

Step Hyp Ref Expression
1 symgov.1 
 |-  G = ( SymGrp ` A )
2 symgov.2 
 |-  B = ( Base ` G )
3 symgov.3 
 |-  .+ = ( +g ` G )
4 eqid 
 |-  ( A ^m A ) = ( A ^m A )
5 1 4 3 symgplusg 
 |-  .+ = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) )
6 5 a1i 
 |-  ( ( X e. B /\ Y e. B ) -> .+ = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) )
7 simpl 
 |-  ( ( f = X /\ g = Y ) -> f = X )
8 simpr 
 |-  ( ( f = X /\ g = Y ) -> g = Y )
9 7 8 coeq12d 
 |-  ( ( f = X /\ g = Y ) -> ( f o. g ) = ( X o. Y ) )
10 9 adantl 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( f = X /\ g = Y ) ) -> ( f o. g ) = ( X o. Y ) )
11 1 2 symgbasmap 
 |-  ( X e. B -> X e. ( A ^m A ) )
12 11 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> X e. ( A ^m A ) )
13 1 2 symgbasmap 
 |-  ( Y e. B -> Y e. ( A ^m A ) )
14 13 adantl 
 |-  ( ( X e. B /\ Y e. B ) -> Y e. ( A ^m A ) )
15 coexg 
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )
16 6 10 12 14 15 ovmpod 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )