Metamath Proof Explorer

Theorem symgfixfo

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is an onto function. (Contributed by AV, 7-Jan-2019)

Ref Expression
Hypotheses symgfixf.p 
|- P = ( Base ` ( SymGrp ` N ) )
symgfixf.q 
|- Q = { q e. P | ( q ` K ) = K }
symgfixf.s 
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgfixf.h 
|- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
Assertion symgfixfo 
|- ( ( N e. V /\ K e. N ) -> H : Q -onto-> S )

Proof

Step Hyp Ref Expression
1 symgfixf.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 symgfixf.q 
 |-  Q = { q e. P | ( q ` K ) = K }
3 symgfixf.s 
 |-  S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
4 symgfixf.h 
 |-  H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
5 1 2 3 4 symgfixf 
 |-  ( K e. N -> H : Q --> S )
6 5 adantl 
 |-  ( ( N e. V /\ K e. N ) -> H : Q --> S )
7 eqeq1 
 |-  ( i = j -> ( i = K <-> j = K ) )
8 fveq2 
 |-  ( i = j -> ( s ` i ) = ( s ` j ) )
9 7 8 ifbieq2d 
 |-  ( i = j -> if ( i = K , K , ( s ` i ) ) = if ( j = K , K , ( s ` j ) ) )
10 9 cbvmptv 
 |-  ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) = ( j e. N |-> if ( j = K , K , ( s ` j ) ) )
11 1 2 3 4 10 symgfixfolem1 
 |-  ( ( N e. V /\ K e. N /\ s e. S ) -> ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) e. Q )
12 11 3expa 
 |-  ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) e. Q )
13 simpr 
 |-  ( ( N e. V /\ K e. N ) -> K e. N )
14 13 anim1i 
 |-  ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> ( K e. N /\ s e. S ) )
15 14 adantl 
 |-  ( ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) /\ ( ( N e. V /\ K e. N ) /\ s e. S ) ) -> ( K e. N /\ s e. S ) )
16 eqid 
 |-  ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) = ( i e. N |-> if ( i = K , K , ( s ` i ) ) )
17 3 16 symgextres 
 |-  ( ( K e. N /\ s e. S ) -> ( ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) |` ( N \ { K } ) ) = s )
18 15 17 syl 
 |-  ( ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) /\ ( ( N e. V /\ K e. N ) /\ s e. S ) ) -> ( ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) |` ( N \ { K } ) ) = s )
19 18 eqcomd 
 |-  ( ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) /\ ( ( N e. V /\ K e. N ) /\ s e. S ) ) -> s = ( ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) |` ( N \ { K } ) ) )
20 reseq1 
 |-  ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) -> ( p |` ( N \ { K } ) ) = ( ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) |` ( N \ { K } ) ) )
21 20 eqeq2d 
 |-  ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) -> ( s = ( p |` ( N \ { K } ) ) <-> s = ( ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) |` ( N \ { K } ) ) ) )
22 21 adantr 
 |-  ( ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) /\ ( ( N e. V /\ K e. N ) /\ s e. S ) ) -> ( s = ( p |` ( N \ { K } ) ) <-> s = ( ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) |` ( N \ { K } ) ) ) )
23 19 22 mpbird 
 |-  ( ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) /\ ( ( N e. V /\ K e. N ) /\ s e. S ) ) -> s = ( p |` ( N \ { K } ) ) )
24 23 ex 
 |-  ( p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) -> ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> s = ( p |` ( N \ { K } ) ) ) )
25 24 adantl 
 |-  ( ( ( ( N e. V /\ K e. N ) /\ s e. S ) /\ p = ( i e. N |-> if ( i = K , K , ( s ` i ) ) ) ) -> ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> s = ( p |` ( N \ { K } ) ) ) )
26 12 25 rspcimedv 
 |-  ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> E. p e. Q s = ( p |` ( N \ { K } ) ) ) )
27 26 pm2.43i 
 |-  ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> E. p e. Q s = ( p |` ( N \ { K } ) ) )
28 4 fvtresfn 
 |-  ( p e. Q -> ( H ` p ) = ( p |` ( N \ { K } ) ) )
29 28 eqeq2d 
 |-  ( p e. Q -> ( s = ( H ` p ) <-> s = ( p |` ( N \ { K } ) ) ) )
30 29 adantl 
 |-  ( ( ( ( N e. V /\ K e. N ) /\ s e. S ) /\ p e. Q ) -> ( s = ( H ` p ) <-> s = ( p |` ( N \ { K } ) ) ) )
31 30 rexbidva 
 |-  ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> ( E. p e. Q s = ( H ` p ) <-> E. p e. Q s = ( p |` ( N \ { K } ) ) ) )
32 27 31 mpbird 
 |-  ( ( ( N e. V /\ K e. N ) /\ s e. S ) -> E. p e. Q s = ( H ` p ) )
33 32 ralrimiva 
 |-  ( ( N e. V /\ K e. N ) -> A. s e. S E. p e. Q s = ( H ` p ) )
34 dffo3 
 |-  ( H : Q -onto-> S <-> ( H : Q --> S /\ A. s e. S E. p e. Q s = ( H ` p ) ) )
35 6 33 34 sylanbrc 
 |-  ( ( N e. V /\ K e. N ) -> H : Q -onto-> S )