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	52	grpmndd	⊢ ( 𝐷 ∈ 𝑉 → 𝑆 ∈ Mnd )
54	33 1 5	symgtrf	⊢ ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 )
55		sswrd	⊢ ( ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 ) → Word ran ( pmTrsp ‘ 𝐷 ) ⊆ Word ( Base ‘ 𝑆 ) )
56	54 55	ax-mp	⊢ Word ran ( pmTrsp ‘ 𝐷 ) ⊆ Word ( Base ‘ 𝑆 )
57	56	sseli	⊢ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → 𝑧 ∈ Word ( Base ‘ 𝑆 ) )
58	56	sseli	⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → 𝑤 ∈ Word ( Base ‘ 𝑆 ) )
59	5 14	gsumccat	⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑧 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑤 ∈ Word ( Base ‘ 𝑆 ) ) → ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
60	53 57 58 59	syl3an	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
61	60	3expb	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
62	61	fveq2d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑁 ‘ ( 𝑆 Σg ( 𝑧 ++ 𝑤 ) ) ) = ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) )
63		ccatlen	⊢ ( ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) = ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) )
64	63	adantl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) = ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) )
65	64	oveq2d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) ) )
66		neg1cn	⊢ - 1 ∈ ℂ
67	66	a1i	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → - 1 ∈ ℂ )
68		lencl	⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
69	68	ad2antll	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
70	35	ad2antrl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
71	67 69 70	expaddd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( - 1 ↑ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
72	65 71	eqtrd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ ( 𝑧 ++ 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
73	51 62 72	3eqtr3d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
74		oveq12	⊢ ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ 𝑦 = ( 𝑆 Σg 𝑤 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) )
75	74	fveq2d	⊢ ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ 𝑦 = ( 𝑆 Σg 𝑤 ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) )
76		oveq12	⊢ ( ( ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
77	75 76	eqeqan12d	⊢ ( ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ 𝑦 = ( 𝑆 Σg 𝑤 ) ) ∧ ( ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
78	77	an4s	⊢ ( ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( ( 𝑆 Σg 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑤 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) · ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
79	73 78	syl5ibrcom	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ) → ( ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
80	79	rexlimdvva	⊢ ( 𝐷 ∈ 𝑉 → ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
81	1 33 2	psgnvali	⊢ ( 𝑦 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
82	34 81	anim12i	⊢ ( ( 𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁 ) → ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
83		reeanv	⊢ ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ↔ ( ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
84	82 83	sylibr	⊢ ( ( 𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁 ) → ∃ 𝑧 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( ( 𝑥 = ( 𝑆 Σg 𝑧 ) ∧ ( 𝑁 ‘ 𝑥 ) = ( - 1 ↑ ( ♯ ‘ 𝑧 ) ) ) ∧ ( 𝑦 = ( 𝑆 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑦 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
85	80 84	impel	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁 ) ) → ( 𝑁 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) )
86	11 12 16 22 25 27 48 85	isghmd	⊢ ( 𝐷 ∈ 𝑉 → 𝑁 ∈ ( 𝐹 GrpHom 𝑈 ) )