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 𝑠 dom N
psgnghm.u U = mulGrp fld 𝑠 1 1
Assertion psgnghm D V N 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 𝑠 dom N
4 psgnghm.u U = mulGrp fld 𝑠 1 1
5 eqid Base S = Base S
6 eqid x Base S | dom x I Fin = x Base S | dom x I Fin
7 1 5 6 2 psgnfn N Fn x Base S | dom x I Fin
8 7 fndmi dom N = x Base S | dom x I Fin
9 8 ssrab3 dom N Base S
10 3 5 ressbas2 dom N Base S dom N = Base F
11 9 10 ax-mp dom N = Base F
12 4 cnmsgnbas 1 1 = Base U
13 11 fvexi dom N V
14 eqid + S = + S
15 3 14 ressplusg dom N V + S = + F
16 13 15 ax-mp + S = + F
17 prex 1 1 V
18 eqid mulGrp fld = mulGrp fld
19 cnfldmul × = fld
20 18 19 mgpplusg × = + mulGrp fld
21 4 20 ressplusg 1 1 V × = + U
22 17 21 ax-mp × = + U
23 1 2 psgndmsubg D V dom N SubGrp S
24 3 subggrp dom N SubGrp S F Grp
25 23 24 syl D V F Grp
26 4 cnmsgngrp U Grp
27 26 a1i D V U Grp
28 fnfun N Fn x Base S | dom x I 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 V N Fn dom N
33 eqid ran pmTrsp D = ran pmTrsp D
34 1 33 2 psgnvali x dom N z Word ran pmTrsp D x = S z N x = 1 z
35 lencl z Word ran pmTrsp D z 0
36 35 nn0zd z Word ran pmTrsp D z
37 m1expcl2 z 1 z 1 1
38 prcom 1 1 = 1 1
39 37 38 eleqtrdi z 1 z 1 1
40 eleq1a 1 z 1 1 N x = 1 z N x 1 1
41 36 39 40 3syl z Word ran pmTrsp D N x = 1 z N x 1 1
42 41 adantld z Word ran pmTrsp D x = S z N x = 1 z N x 1 1
43 42 rexlimiv z Word ran pmTrsp D x = S z N x = 1 z N x 1 1
44 43 a1i D V z Word ran pmTrsp D x = S z N x = 1 z N x 1 1
45 34 44 syl5 D V x dom N N x 1 1
46 45 ralrimiv D V x dom N N x 1 1
47 ffnfv N : dom N 1 1 N Fn dom N x dom N N x 1 1
48 32 46 47 sylanbrc D V N : dom N 1 1
49 ccatcl z Word ran pmTrsp D w Word ran pmTrsp D z ++ w Word ran pmTrsp D
50 1 33 2 psgnvalii D V z ++ w Word ran pmTrsp D N S z ++ w = 1 z ++ w
51 49 50 sylan2 D V z Word ran pmTrsp D w Word ran pmTrsp D N S z ++ w = 1 z ++ w
52 1 symggrp D V S Grp
53 52 grpmndd D V S Mnd
54 33 1 5 symgtrf ran pmTrsp D Base S
55 sswrd ran pmTrsp D Base S Word ran pmTrsp D Word Base S
56 54 55 ax-mp Word ran pmTrsp D Word Base S
57 56 sseli z Word ran pmTrsp D z Word Base S
58 56 sseli w Word ran pmTrsp D w Word Base S
59 5 14 gsumccat S Mnd z Word Base S w Word Base S S z ++ w = S z + S S w
60 53 57 58 59 syl3an D V z Word ran pmTrsp D w Word ran pmTrsp D S z ++ w = S z + S S w
61 60 3expb D V z Word ran pmTrsp D w Word ran pmTrsp D S z ++ w = S z + S S w
62 61 fveq2d D V z Word ran pmTrsp D w Word ran pmTrsp D N S z ++ w = N S z + S S w
63 ccatlen z Word ran pmTrsp D w Word ran pmTrsp D z ++ w = z + w
64 63 adantl D V z Word ran pmTrsp D w Word ran pmTrsp D z ++ w = z + w
65 64 oveq2d D V z Word ran pmTrsp D w Word ran pmTrsp D 1 z ++ w = 1 z + w
66 neg1cn 1
67 66 a1i D V z Word ran pmTrsp D w Word ran pmTrsp D 1
68 lencl w Word ran pmTrsp D w 0
69 68 ad2antll D V z Word ran pmTrsp D w Word ran pmTrsp D w 0
70 35 ad2antrl D V z Word ran pmTrsp D w Word ran pmTrsp D z 0
71 67 69 70 expaddd D V z Word ran pmTrsp D w Word ran pmTrsp D 1 z + w = 1 z 1 w
72 65 71 eqtrd D V z Word ran pmTrsp D w Word ran pmTrsp D 1 z ++ w = 1 z 1 w
73 51 62 72 3eqtr3d D V z Word ran pmTrsp D w Word ran pmTrsp D N S z + S S w = 1 z 1 w
74 oveq12 x = S z y = S w x + S y = S z + S S w
75 74 fveq2d x = S z y = S w N x + S y = N S z + S S w
76 oveq12 N x = 1 z N y = 1 w N x N y = 1 z 1 w
77 75 76 eqeqan12d x = S z y = S w N x = 1 z N y = 1 w N x + S y = N x N y N S z + S S w = 1 z 1 w
78 77 an4s x = S z N x = 1 z y = S w N y = 1 w N x + S y = N x N y N S z + S S w = 1 z 1 w
79 73 78 syl5ibrcom D V z Word ran pmTrsp D w Word ran pmTrsp D x = S z N x = 1 z y = S w N y = 1 w N x + S y = N x N y
80 79 rexlimdvva D V z Word ran pmTrsp D w Word ran pmTrsp D x = S z N x = 1 z y = S w N y = 1 w N x + S y = N x N y
81 1 33 2 psgnvali y dom N w Word ran pmTrsp D y = S w N y = 1 w
82 34 81 anim12i x dom N y dom N z Word ran pmTrsp D x = S z N x = 1 z w Word ran pmTrsp D y = S w N y = 1 w
83 reeanv z Word ran pmTrsp D w Word ran pmTrsp D x = S z N x = 1 z y = S w N y = 1 w z Word ran pmTrsp D x = S z N x = 1 z w Word ran pmTrsp D y = S w N y = 1 w
84 82 83 sylibr x dom N y dom N z Word ran pmTrsp D w Word ran pmTrsp D x = S z N x = 1 z y = S w N y = 1 w
85 80 84 impel D V x dom N y dom N N x + S y = N x N y
86 11 12 16 22 25 27 48 85 isghmd D V N F GrpHom U