Metamath Proof Explorer

Theorem symggrp

Description: The symmetric group on a set A is a group. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 28-Jan-2024)

Ref Expression
Hypothesis symggrp.1 
|- G = ( SymGrp ` A )
Assertion symggrp 
|- ( A e. V -> G e. Grp )

Proof

Step Hyp Ref Expression
1 symggrp.1 
 |-  G = ( SymGrp ` A )
2 eqidd 
 |-  ( A e. V -> ( Base ` G ) = ( Base ` G ) )
3 eqidd 
 |-  ( A e. V -> ( +g ` G ) = ( +g ` G ) )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 1 4 5 symgcl 
 |-  ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
7 6 3adant1 
 |-  ( ( A e. V /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
8 1 4 5 symgcl 
 |-  ( ( f e. ( Base ` G ) /\ g e. ( Base ` G ) ) -> ( f ( +g ` G ) g ) e. ( Base ` G ) )
9 1 4 5 symgov 
 |-  ( ( f e. ( Base ` G ) /\ g e. ( Base ` G ) ) -> ( f ( +g ` G ) g ) = ( f o. g ) )
10 8 9 symggrplem 
 |-  ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) )
11 10 adantl 
 |-  ( ( A e. V /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) )
12 1 idresperm 
 |-  ( A e. V -> ( _I |` A ) e. ( Base ` G ) )
13 1 4 5 symgov 
 |-  ( ( ( _I |` A ) e. ( Base ` G ) /\ x e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) x ) = ( ( _I |` A ) o. x ) )
14 12 13 sylan 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) x ) = ( ( _I |` A ) o. x ) )
15 1 4 elsymgbas 
 |-  ( A e. V -> ( x e. ( Base ` G ) <-> x : A -1-1-onto-> A ) )
16 15 biimpa 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> x : A -1-1-onto-> A )
17 f1of 
 |-  ( x : A -1-1-onto-> A -> x : A --> A )
18 fcoi2 
 |-  ( x : A --> A -> ( ( _I |` A ) o. x ) = x )
19 16 17 18 3syl 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> ( ( _I |` A ) o. x ) = x )
20 14 19 eqtrd 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) x ) = x )
21 f1ocnv 
 |-  ( x : A -1-1-onto-> A -> `' x : A -1-1-onto-> A )
22 21 a1i 
 |-  ( A e. V -> ( x : A -1-1-onto-> A -> `' x : A -1-1-onto-> A ) )
23 1 4 elsymgbas 
 |-  ( A e. V -> ( `' x e. ( Base ` G ) <-> `' x : A -1-1-onto-> A ) )
24 22 15 23 3imtr4d 
 |-  ( A e. V -> ( x e. ( Base ` G ) -> `' x e. ( Base ` G ) ) )
25 24 imp 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> `' x e. ( Base ` G ) )
26 1 4 5 symgov 
 |-  ( ( `' x e. ( Base ` G ) /\ x e. ( Base ` G ) ) -> ( `' x ( +g ` G ) x ) = ( `' x o. x ) )
27 25 26 sylancom 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> ( `' x ( +g ` G ) x ) = ( `' x o. x ) )
28 f1ococnv1 
 |-  ( x : A -1-1-onto-> A -> ( `' x o. x ) = ( _I |` A ) )
29 16 28 syl 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> ( `' x o. x ) = ( _I |` A ) )
30 27 29 eqtrd 
 |-  ( ( A e. V /\ x e. ( Base ` G ) ) -> ( `' x ( +g ` G ) x ) = ( _I |` A ) )
31 2 3 7 11 12 20 25 30 isgrpd 
 |-  ( A e. V -> G e. Grp )