Metamath Proof Explorer

Theorem pgrpsubgsymg

Description: Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019) (Revised by AV, 30-Mar-2024)

Ref Expression
Hypotheses pgrpsubgsymgbi.g 
|- G = ( SymGrp ` A )
pgrpsubgsymgbi.b 
|- B = ( Base ` G )
pgrpsubgsymg.c 
|- F = ( Base ` P )
Assertion pgrpsubgsymg 
|- ( A e. V -> ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F e. ( SubGrp ` G ) ) )

Proof

Step Hyp Ref Expression
1 pgrpsubgsymgbi.g 
 |-  G = ( SymGrp ` A )
2 pgrpsubgsymgbi.b 
 |-  B = ( Base ` G )
3 pgrpsubgsymg.c 
 |-  F = ( Base ` P )
4 1 symggrp 
 |-  ( A e. V -> G e. Grp )
5 simp1 
 |-  ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> P e. Grp )
6 4 5 anim12i 
 |-  ( ( A e. V /\ ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) ) -> ( G e. Grp /\ P e. Grp ) )
7 simp2 
 |-  ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F C_ B )
8 simp3 
 |-  ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) )
9 1 2 symgbasmap 
 |-  ( f e. B -> f e. ( A ^m A ) )
10 9 ssriv 
 |-  B C_ ( A ^m A )
11 sstr 
 |-  ( ( F C_ B /\ B C_ ( A ^m A ) ) -> F C_ ( A ^m A ) )
12 10 11 mpan2 
 |-  ( F C_ B -> F C_ ( A ^m A ) )
13 resmpo 
 |-  ( ( F C_ ( A ^m A ) /\ F C_ ( A ^m A ) ) -> ( ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) |` ( F X. F ) ) = ( f e. F , g e. F |-> ( f o. g ) ) )
14 13 anidms 
 |-  ( F C_ ( A ^m A ) -> ( ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) |` ( F X. F ) ) = ( f e. F , g e. F |-> ( f o. g ) ) )
15 12 14 syl 
 |-  ( F C_ B -> ( ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) |` ( F X. F ) ) = ( f e. F , g e. F |-> ( f o. g ) ) )
16 eqid 
 |-  ( A ^m A ) = ( A ^m A )
17 eqid 
 |-  ( +g ` G ) = ( +g ` G )
18 1 16 17 symgplusg 
 |-  ( +g ` G ) = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) )
19 18 eqcomi 
 |-  ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) = ( +g ` G )
20 19 reseq1i 
 |-  ( ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) |` ( F X. F ) ) = ( ( +g ` G ) |` ( F X. F ) )
21 15 20 eqtr3di 
 |-  ( F C_ B -> ( f e. F , g e. F |-> ( f o. g ) ) = ( ( +g ` G ) |` ( F X. F ) ) )
22 21 3ad2ant2 
 |-  ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( f e. F , g e. F |-> ( f o. g ) ) = ( ( +g ` G ) |` ( F X. F ) ) )
23 8 22 eqtrd 
 |-  ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( +g ` P ) = ( ( +g ` G ) |` ( F X. F ) ) )
24 7 23 jca 
 |-  ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( F C_ B /\ ( +g ` P ) = ( ( +g ` G ) |` ( F X. F ) ) ) )
25 24 adantl 
 |-  ( ( A e. V /\ ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) ) -> ( F C_ B /\ ( +g ` P ) = ( ( +g ` G ) |` ( F X. F ) ) ) )
26 2 3 grpissubg 
 |-  ( ( G e. Grp /\ P e. Grp ) -> ( ( F C_ B /\ ( +g ` P ) = ( ( +g ` G ) |` ( F X. F ) ) ) -> F e. ( SubGrp ` G ) ) )
27 6 25 26 sylc 
 |-  ( ( A e. V /\ ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) ) -> F e. ( SubGrp ` G ) )
28 27 ex 
 |-  ( A e. V -> ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F e. ( SubGrp ` G ) ) )