Metamath Proof Explorer

Theorem evpmss

Description: Even permutations are permutations. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmss.s 
|- S = ( SymGrp ` D )
evpmss.p 
|- P = ( Base ` S )
Assertion evpmss 
|- ( pmEven ` D ) C_ P

Proof

Step Hyp Ref Expression
1 evpmss.s 
 |-  S = ( SymGrp ` D )
2 evpmss.p 
 |-  P = ( Base ` S )
3 fveq2 
 |-  ( d = D -> ( pmSgn ` d ) = ( pmSgn ` D ) )
4 3 cnveqd 
 |-  ( d = D -> `' ( pmSgn ` d ) = `' ( pmSgn ` D ) )
5 4 imaeq1d 
 |-  ( d = D -> ( `' ( pmSgn ` d ) " { 1 } ) = ( `' ( pmSgn ` D ) " { 1 } ) )
6 df-evpm 
 |-  pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )
7 fvex 
 |-  ( pmSgn ` D ) e. _V
8 7 cnvex 
 |-  `' ( pmSgn ` D ) e. _V
9 8 imaex 
 |-  ( `' ( pmSgn ` D ) " { 1 } ) e. _V
10 5 6 9 fvmpt 
 |-  ( D e. _V -> ( pmEven ` D ) = ( `' ( pmSgn ` D ) " { 1 } ) )
11 cnvimass 
 |-  ( `' ( pmSgn ` D ) " { 1 } ) C_ dom ( pmSgn ` D )
12 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
13 eqid 
 |-  ( S |`s dom ( pmSgn ` D ) ) = ( S |`s dom ( pmSgn ` D ) )
14 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
15 1 12 13 14 psgnghm 
 |-  ( D e. _V -> ( pmSgn ` D ) e. ( ( S |`s dom ( pmSgn ` D ) ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
16 eqid 
 |-  ( Base ` ( S |`s dom ( pmSgn ` D ) ) ) = ( Base ` ( S |`s dom ( pmSgn ` D ) ) )
17 eqid 
 |-  ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
18 16 17 ghmf 
 |-  ( ( pmSgn ` D ) e. ( ( S |`s dom ( pmSgn ` D ) ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> ( pmSgn ` D ) : ( Base ` ( S |`s dom ( pmSgn ` D ) ) ) --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
19 fdm 
 |-  ( ( pmSgn ` D ) : ( Base ` ( S |`s dom ( pmSgn ` D ) ) ) --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> dom ( pmSgn ` D ) = ( Base ` ( S |`s dom ( pmSgn ` D ) ) ) )
20 15 18 19 3syl 
 |-  ( D e. _V -> dom ( pmSgn ` D ) = ( Base ` ( S |`s dom ( pmSgn ` D ) ) ) )
21 13 2 ressbasss 
 |-  ( Base ` ( S |`s dom ( pmSgn ` D ) ) ) C_ P
22 20 21 eqsstrdi 
 |-  ( D e. _V -> dom ( pmSgn ` D ) C_ P )
23 11 22 sstrid 
 |-  ( D e. _V -> ( `' ( pmSgn ` D ) " { 1 } ) C_ P )
24 10 23 eqsstrd 
 |-  ( D e. _V -> ( pmEven ` D ) C_ P )
25 fvprc 
 |-  ( -. D e. _V -> ( pmEven ` D ) = (/) )
26 0ss 
 |-  (/) C_ P
27 25 26 eqsstrdi 
 |-  ( -. D e. _V -> ( pmEven ` D ) C_ P )
28 24 27 pm2.61i 
 |-  ( pmEven ` D ) C_ P