Metamath Proof Explorer

Theorem psgnghm

Description: The sign is a homomorphism from the finitary permutation group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnghm.s 
|- S = ( SymGrp ` D )
psgnghm.n 
|- N = ( pmSgn ` D )
psgnghm.f 
|- F = ( S |`s dom N )
psgnghm.u 
|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
Assertion psgnghm 
|- ( D e. V -> N e. ( F GrpHom U ) )

Proof

Step Hyp Ref Expression
1 psgnghm.s 
 |-  S = ( SymGrp ` D )
2 psgnghm.n 
 |-  N = ( pmSgn ` D )
3 psgnghm.f 
 |-  F = ( S |`s dom N )
4 psgnghm.u 
 |-  U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin } = { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin }
7 1 5 6 2 psgnfn 
 |-  N Fn { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin }
8 7 fndmi 
 |-  dom N = { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin }
9 8 ssrab3 
 |-  dom N C_ ( Base ` S )
10 3 5 ressbas2 
 |-  ( dom N C_ ( Base ` S ) -> dom N = ( Base ` F ) )
11 9 10 ax-mp 
 |-  dom N = ( Base ` F )
12 4 cnmsgnbas 
 |-  { 1 , -u 1 } = ( Base ` U )
13 11 fvexi 
 |-  dom N e. _V
14 eqid 
 |-  ( +g ` S ) = ( +g ` S )
15 3 14 ressplusg 
 |-  ( dom N e. _V -> ( +g ` S ) = ( +g ` F ) )
16 13 15 ax-mp 
 |-  ( +g ` S ) = ( +g ` F )
17 prex 
 |-  { 1 , -u 1 } e. _V
18 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
19 cnfldmul 
 |-  x. = ( .r ` CCfld )
20 18 19 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
21 4 20 ressplusg 
 |-  ( { 1 , -u 1 } e. _V -> x. = ( +g ` U ) )
22 17 21 ax-mp 
 |-  x. = ( +g ` U )
23 1 2 psgndmsubg 
 |-  ( D e. V -> dom N e. ( SubGrp ` S ) )
24 3 subggrp 
 |-  ( dom N e. ( SubGrp ` S ) -> F e. Grp )
25 23 24 syl 
 |-  ( D e. V -> F e. Grp )
26 4 cnmsgngrp 
 |-  U e. Grp
27 26 a1i 
 |-  ( D e. V -> U e. Grp )
28 fnfun 
 |-  ( N Fn { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin } -> Fun N )
29 7 28 ax-mp 
 |-  Fun N
30 funfn 
 |-  ( Fun N <-> N Fn dom N )
31 29 30 mpbi 
 |-  N Fn dom N
32 31 a1i 
 |-  ( D e. V -> N Fn dom N )
33 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
34 1 33 2 psgnvali 
 |-  ( x e. dom N -> E. z e. Word ran ( pmTrsp ` D ) ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) )
35 lencl 
 |-  ( z e. Word ran ( pmTrsp ` D ) -> ( # ` z ) e. NN0 )
36 35 nn0zd 
 |-  ( z e. Word ran ( pmTrsp ` D ) -> ( # ` z ) e. ZZ )
37 m1expcl2 
 |-  ( ( # ` z ) e. ZZ -> ( -u 1 ^ ( # ` z ) ) e. { -u 1 , 1 } )
38 prcom 
 |-  { -u 1 , 1 } = { 1 , -u 1 }
39 37 38 eleqtrdi 
 |-  ( ( # ` z ) e. ZZ -> ( -u 1 ^ ( # ` z ) ) e. { 1 , -u 1 } )
40 eleq1a 
 |-  ( ( -u 1 ^ ( # ` z ) ) e. { 1 , -u 1 } -> ( ( N ` x ) = ( -u 1 ^ ( # ` z ) ) -> ( N ` x ) e. { 1 , -u 1 } ) )
41 36 39 40 3syl 
 |-  ( z e. Word ran ( pmTrsp ` D ) -> ( ( N ` x ) = ( -u 1 ^ ( # ` z ) ) -> ( N ` x ) e. { 1 , -u 1 } ) )
42 41 adantld 
 |-  ( z e. Word ran ( pmTrsp ` D ) -> ( ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) -> ( N ` x ) e. { 1 , -u 1 } ) )
43 42 rexlimiv 
 |-  ( E. z e. Word ran ( pmTrsp ` D ) ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) -> ( N ` x ) e. { 1 , -u 1 } )
44 43 a1i 
 |-  ( D e. V -> ( E. z e. Word ran ( pmTrsp ` D ) ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) -> ( N ` x ) e. { 1 , -u 1 } ) )
45 34 44 syl5 
 |-  ( D e. V -> ( x e. dom N -> ( N ` x ) e. { 1 , -u 1 } ) )
46 45 ralrimiv 
 |-  ( D e. V -> A. x e. dom N ( N ` x ) e. { 1 , -u 1 } )
47 ffnfv 
 |-  ( N : dom N --> { 1 , -u 1 } <-> ( N Fn dom N /\ A. x e. dom N ( N ` x ) e. { 1 , -u 1 } ) )
48 32 46 47 sylanbrc 
 |-  ( D e. V -> N : dom N --> { 1 , -u 1 } )
49 ccatcl 
 |-  ( ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) -> ( z ++ w ) e. Word ran ( pmTrsp ` D ) )
50 1 33 2 psgnvalii 
 |-  ( ( D e. V /\ ( z ++ w ) e. Word ran ( pmTrsp ` D ) ) -> ( N ` ( S gsum ( z ++ w ) ) ) = ( -u 1 ^ ( # ` ( z ++ w ) ) ) )
51 49 50 sylan2 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( N ` ( S gsum ( z ++ w ) ) ) = ( -u 1 ^ ( # ` ( z ++ w ) ) ) )
52 1 symggrp 
 |-  ( D e. V -> S e. Grp )
53 52 grpmndd 
 |-  ( D e. V -> S e. Mnd )
54 33 1 5 symgtrf 
 |-  ran ( pmTrsp ` D ) C_ ( Base ` S )
55 sswrd 
 |-  ( ran ( pmTrsp ` D ) C_ ( Base ` S ) -> Word ran ( pmTrsp ` D ) C_ Word ( Base ` S ) )
56 54 55 ax-mp 
 |-  Word ran ( pmTrsp ` D ) C_ Word ( Base ` S )
57 56 sseli 
 |-  ( z e. Word ran ( pmTrsp ` D ) -> z e. Word ( Base ` S ) )
58 56 sseli 
 |-  ( w e. Word ran ( pmTrsp ` D ) -> w e. Word ( Base ` S ) )
59 5 14 gsumccat 
 |-  ( ( S e. Mnd /\ z e. Word ( Base ` S ) /\ w e. Word ( Base ` S ) ) -> ( S gsum ( z ++ w ) ) = ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) )
60 53 57 58 59 syl3an 
 |-  ( ( D e. V /\ z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) -> ( S gsum ( z ++ w ) ) = ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) )
61 60 3expb 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( S gsum ( z ++ w ) ) = ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) )
62 61 fveq2d 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( N ` ( S gsum ( z ++ w ) ) ) = ( N ` ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) ) )
63 ccatlen 
 |-  ( ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) -> ( # ` ( z ++ w ) ) = ( ( # ` z ) + ( # ` w ) ) )
64 63 adantl 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( # ` ( z ++ w ) ) = ( ( # ` z ) + ( # ` w ) ) )
65 64 oveq2d 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( -u 1 ^ ( # ` ( z ++ w ) ) ) = ( -u 1 ^ ( ( # ` z ) + ( # ` w ) ) ) )
66 neg1cn 
 |-  -u 1 e. CC
67 66 a1i 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> -u 1 e. CC )
68 lencl 
 |-  ( w e. Word ran ( pmTrsp ` D ) -> ( # ` w ) e. NN0 )
69 68 ad2antll 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( # ` w ) e. NN0 )
70 35 ad2antrl 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( # ` z ) e. NN0 )
71 67 69 70 expaddd 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( -u 1 ^ ( ( # ` z ) + ( # ` w ) ) ) = ( ( -u 1 ^ ( # ` z ) ) x. ( -u 1 ^ ( # ` w ) ) ) )
72 65 71 eqtrd 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( -u 1 ^ ( # ` ( z ++ w ) ) ) = ( ( -u 1 ^ ( # ` z ) ) x. ( -u 1 ^ ( # ` w ) ) ) )
73 51 62 72 3eqtr3d 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( N ` ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) ) = ( ( -u 1 ^ ( # ` z ) ) x. ( -u 1 ^ ( # ` w ) ) ) )
74 oveq12 
 |-  ( ( x = ( S gsum z ) /\ y = ( S gsum w ) ) -> ( x ( +g ` S ) y ) = ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) )
75 74 fveq2d 
 |-  ( ( x = ( S gsum z ) /\ y = ( S gsum w ) ) -> ( N ` ( x ( +g ` S ) y ) ) = ( N ` ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) ) )
76 oveq12 
 |-  ( ( ( N ` x ) = ( -u 1 ^ ( # ` z ) ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) -> ( ( N ` x ) x. ( N ` y ) ) = ( ( -u 1 ^ ( # ` z ) ) x. ( -u 1 ^ ( # ` w ) ) ) )
77 75 76 eqeqan12d 
 |-  ( ( ( x = ( S gsum z ) /\ y = ( S gsum w ) ) /\ ( ( N ` x ) = ( -u 1 ^ ( # ` z ) ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) -> ( ( N ` ( x ( +g ` S ) y ) ) = ( ( N ` x ) x. ( N ` y ) ) <-> ( N ` ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) ) = ( ( -u 1 ^ ( # ` z ) ) x. ( -u 1 ^ ( # ` w ) ) ) ) )
78 77 an4s 
 |-  ( ( ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) -> ( ( N ` ( x ( +g ` S ) y ) ) = ( ( N ` x ) x. ( N ` y ) ) <-> ( N ` ( ( S gsum z ) ( +g ` S ) ( S gsum w ) ) ) = ( ( -u 1 ^ ( # ` z ) ) x. ( -u 1 ^ ( # ` w ) ) ) ) )
79 73 78 syl5ibrcom 
 |-  ( ( D e. V /\ ( z e. Word ran ( pmTrsp ` D ) /\ w e. Word ran ( pmTrsp ` D ) ) ) -> ( ( ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) -> ( N ` ( x ( +g ` S ) y ) ) = ( ( N ` x ) x. ( N ` y ) ) ) )
80 79 rexlimdvva 
 |-  ( D e. V -> ( E. z e. Word ran ( pmTrsp ` D ) E. w e. Word ran ( pmTrsp ` D ) ( ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) -> ( N ` ( x ( +g ` S ) y ) ) = ( ( N ` x ) x. ( N ` y ) ) ) )
81 1 33 2 psgnvali 
 |-  ( y e. dom N -> E. w e. Word ran ( pmTrsp ` D ) ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) )
82 34 81 anim12i 
 |-  ( ( x e. dom N /\ y e. dom N ) -> ( E. z e. Word ran ( pmTrsp ` D ) ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ E. w e. Word ran ( pmTrsp ` D ) ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) )
83 reeanv 
 |-  ( E. z e. Word ran ( pmTrsp ` D ) E. w e. Word ran ( pmTrsp ` D ) ( ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) <-> ( E. z e. Word ran ( pmTrsp ` D ) ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ E. w e. Word ran ( pmTrsp ` D ) ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) )
84 82 83 sylibr 
 |-  ( ( x e. dom N /\ y e. dom N ) -> E. z e. Word ran ( pmTrsp ` D ) E. w e. Word ran ( pmTrsp ` D ) ( ( x = ( S gsum z ) /\ ( N ` x ) = ( -u 1 ^ ( # ` z ) ) ) /\ ( y = ( S gsum w ) /\ ( N ` y ) = ( -u 1 ^ ( # ` w ) ) ) ) )
85 80 84 impel 
 |-  ( ( D e. V /\ ( x e. dom N /\ y e. dom N ) ) -> ( N ` ( x ( +g ` S ) y ) ) = ( ( N ` x ) x. ( N ` y ) ) )
86 11 12 16 22 25 27 48 85 isghmd 
 |-  ( D e. V -> N e. ( F GrpHom U ) )