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 ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
psgnghm.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
psgnghm.f ⊢ 𝐹 = ( 𝑆 ↾s dom 𝑁 )
psgnghm.u ⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
Assertion psgnghm ( 𝐷 ∈ 𝑉 → 𝑁 ∈ ( 𝐹 GrpHom 𝑈 ) )

Proof

Step Hyp Ref Expression
1 psgnghm.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 psgnghm.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
3 psgnghm.f ⊢ 𝐹 = ( 𝑆 ↾s dom 𝑁 )
4 psgnghm.u ⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
5 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 eqid ⊢ { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } = { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
7 1 5 6 2 psgnfn ⊢ 𝑁 Fn { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
8 7 fndmi ⊢ dom 𝑁 = { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
9 8 ssrab3 ⊢ dom 𝑁 ⊆ ( Base ‘ 𝑆 )
10 3 5 ressbas2 ⊢ ( dom 𝑁 ⊆ ( Base ‘ 𝑆 ) → dom 𝑁 = ( Base ‘ 𝐹 ) )
11 9 10 ax-mp ⊢ dom 𝑁 = ( Base ‘ 𝐹 )
12 4 cnmsgnbas ⊢ { 1 , - 1 } = ( Base ‘ 𝑈 )
13 11 fvexi ⊢ dom 𝑁 ∈ V
14 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
15 3 14 ressplusg ⊢ ( dom 𝑁 ∈ V → ( +g ‘ 𝑆 ) = ( +g ‘ 𝐹 ) )
16 13 15 ax-mp ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝐹 )
17 prex ⊢ { 1 , - 1 } ∈ V
18 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
19 cnfldmul ⊢ · = ( .r ‘ ℂfld )
20 18 19 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
21 4 20 ressplusg ⊢ ( { 1 , - 1 } ∈ V → · = ( +g ‘ 𝑈 ) )
22 17 21 ax-mp ⊢ · = ( +g ‘ 𝑈 )
23 1 2 psgndmsubg ⊢ ( 𝐷 ∈ 𝑉 → dom 𝑁 ∈ ( SubGrp ‘ 𝑆 ) )
24 3 subggrp ⊢ ( dom 𝑁 ∈ ( SubGrp ‘ 𝑆 ) → 𝐹 ∈ Grp )
25 23 24 syl ⊢ ( 𝐷 ∈ 𝑉 → 𝐹 ∈ Grp )
26 4 cnmsgngrp ⊢ 𝑈 ∈ Grp
27 26 a1i ⊢ ( 𝐷 ∈ 𝑉 → 𝑈 ∈ Grp )
28 fnfun ⊢ ( 𝑁 Fn { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } → Fun 𝑁 )
29 7 28 ax-mp ⊢ Fun 𝑁
30 funfn ⊢ ( Fun 𝑁 ↔ 𝑁 Fn dom 𝑁 )
31 29 30 mpbi ⊢ 𝑁 Fn dom 𝑁
32 31 a1i ⊢ ( 𝐷 ∈ 𝑉 → 𝑁 Fn dom 𝑁 )
33 eqid ⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 )
34 1 33 2 psgnvali ⊢ ( 𝑥 ∈ dom 𝑁 → ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) )
35 lencl ⊢ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
36 35 nn0zd ⊢ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ♯ ‘ 𝑧 ) ∈ ℤ )
37 m1expcl2 ⊢ ( ( ♯ ‘ 𝑧 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∈ { - 1 , 1 } )
38 prcom ⊢ { - 1 , 1 } = { 1 , - 1 }
39 37 38 eleqtrdi ⊢ ( ( ♯ ‘ 𝑧 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∈ { 1 , - 1 } )
40 eleq1a ⊢ ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∈ { 1 , - 1 } → ( ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) → ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } ) )
41 36 39 40 3syl ⊢ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) → ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } ) )
42 41 adantld ⊢ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) → ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } ) )
43 42 rexlimiv ⊢ ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) → ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } )
44 43 a1i ⊢ ( 𝐷 ∈ 𝑉 → ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) → ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } ) )
45 34 44 syl5 ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑥 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } ) )
46 45 ralrimiv ⊢ ( 𝐷 ∈ 𝑉 → ∀ 𝑥 ∈ dom 𝑁 ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } )
47 ffnfv ⊢ ( 𝑁 : dom 𝑁 ⟶ { 1 , - 1 } ↔ ( 𝑁 Fn dom 𝑁 ∧ ∀ 𝑥 ∈ dom 𝑁 ( 𝑁 ‘ 𝑥 ) ∈ { 1 , - 1 } ) )
48 32 46 47 sylanbrc ⊢ ( 𝐷 ∈ 𝑉 → 𝑁 : dom 𝑁 ⟶ { 1 , - 1 } )
49 ccatcl ⊢ ( ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( 𝑧 ++ 𝑤 ) ∈ Word ran ( pmTrsp ‘ 𝐷 ) )
50 1 33 2 psgnvalii ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ++ 𝑤 ) ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( 𝑁 ‘ ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) ) = ( - 1 ↑ ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) ) )
51 49 50 sylan2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑁 ‘ ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) ) = ( - 1 ↑ ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) ) )
52 1 symggrp ⊢ ( 𝐷 ∈ 𝑉 → 𝑆 ∈ Grp )
53 grpmnd ⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
54 52 53 syl ⊢ ( 𝐷 ∈ 𝑉 → 𝑆 ∈ Mnd )
55 33 1 5 symgtrf ⊢ ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 )
56 sswrd ⊢ ( ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 ) → Word ran ( pmTrsp ‘ 𝐷 ) ⊆ Word ( Base ‘ 𝑆 ) )
57 55 56 ax-mp ⊢ Word ran ( pmTrsp ‘ 𝐷 ) ⊆ Word ( Base ‘ 𝑆 )
58 57 sseli ⊢ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → 𝑧 ∈ Word ( Base ‘ 𝑆 ) )
59 57 sseli ⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → 𝑤 ∈ Word ( Base ‘ 𝑆 ) )
60 5 14 gsumccat ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑧 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑤 ∈ Word ( Base ‘ 𝑆 ) ) → ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
61 54 58 59 60 syl3an ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
62 61 3expb ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
63 62 fveq2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑁 ‘ ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) ) = ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) )
64 ccatlen ⊢ ( ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) = ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) )
65 64 adantl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) = ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) )
66 65 oveq2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) ) )
67 neg1cn ⊢ - 1 ∈ ℂ
68 67 a1i ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → - 1 ∈ ℂ )
69 lencl ⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
70 69 ad2antll ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
71 35 ad2antrl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
72 68 70 71 expaddd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( - 1 ↑ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
73 66 72 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
74 51 63 73 3eqtr3d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
75 oveq12 ⊢ ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ 𝑦 = ( 𝑆 Σg 𝑤 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
76 75 fveq2d ⊢ ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ 𝑦 = ( 𝑆 Σg 𝑤 ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) )
77 oveq12 ⊢ ( ( ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
78 76 77 eqeqan12d ⊢ ( ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ 𝑦 = ( 𝑆 Σg 𝑤 ) ) ∧ ( ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
79 78 an4s ⊢ ( ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
80 74 79 syl5ibrcom ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
81 80 rexlimdvva ⊢ ( 𝐷 ∈ 𝑉 → ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
82 1 33 2 psgnvali ⊢ ( 𝑦 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
83 34 82 anim12i ⊢ ( ( 𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁 ) → ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
84 reeanv ⊢ ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ↔ ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
85 83 84 sylibr ⊢ ( ( 𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁 ) → ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
86 81 85 impel ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁 ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) )
87 11 12 16 22 25 27 48 86 isghmd ⊢ ( 𝐷 ∈ 𝑉 → 𝑁 ∈ ( 𝐹 GrpHom 𝑈 ) )