Metamath Proof Explorer


Theorem psgnunilem4

Description: Lemma for psgnuni . An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypotheses psgnunilem4.g 𝐺 = ( SymGrp ‘ 𝐷 )
psgnunilem4.t 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnunilem4.d ( 𝜑𝐷𝑉 )
psgnunilem4.w1 ( 𝜑𝑊 ∈ Word 𝑇 )
psgnunilem4.w2 ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
Assertion psgnunilem4 ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 psgnunilem4.g 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnunilem4.t 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnunilem4.d ( 𝜑𝐷𝑉 )
4 psgnunilem4.w1 ( 𝜑𝑊 ∈ Word 𝑇 )
5 psgnunilem4.w2 ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
6 wrdfin ( 𝑊 ∈ Word 𝑇𝑊 ∈ Fin )
7 hashcl ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
8 4 6 7 3syl ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9 nn0uz 0 = ( ℤ ‘ 0 )
10 8 9 eleqtrdi ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 0 ) )
11 fveq2 ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ∅ ) )
12 hash0 ( ♯ ‘ ∅ ) = 0
13 11 12 eqtrdi ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = 0 )
14 13 oveq2d ( 𝑤 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ 0 ) )
15 neg1cn - 1 ∈ ℂ
16 exp0 ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
17 15 16 ax-mp ( - 1 ↑ 0 ) = 1
18 14 17 eqtrdi ( 𝑤 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 )
19 18 2a1d ( 𝑤 = ∅ → ( ( 𝜑 ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
20 simpl1 ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → 𝜑 )
21 20 3 syl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → 𝐷𝑉 )
22 simpl3l ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ∈ Word 𝑇 )
23 eqidd ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑤 ) )
24 wrdfin ( 𝑤 ∈ Word 𝑇𝑤 ∈ Fin )
25 22 24 syl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ∈ Fin )
26 simpl2 ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ≠ ∅ )
27 hashnncl ( 𝑤 ∈ Fin → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ 𝑤 ≠ ∅ ) )
28 27 biimpar ( ( 𝑤 ∈ Fin ∧ 𝑤 ≠ ∅ ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
29 25 26 28 syl2anc ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
30 simpl3r ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) )
31 fveqeq2 ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ↔ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ) )
32 oveq2 ( 𝑥 = 𝑦 → ( 𝐺 Σg 𝑥 ) = ( 𝐺 Σg 𝑦 ) )
33 32 eqeq1d ( 𝑥 = 𝑦 → ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
34 31 33 anbi12d ( 𝑥 = 𝑦 → ( ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ( ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) ) )
35 34 cbvrexvw ( ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
36 35 notbii ( ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ¬ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
37 36 biimpi ( ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ¬ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
38 37 adantl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ¬ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
39 1 2 21 22 23 29 30 38 psgnunilem3 ¬ ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
40 iman ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ↔ ¬ ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
41 39 40 mpbir ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
42 df-rex ( ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
43 41 42 sylib ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
44 simprl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → 𝑥 ∈ Word 𝑇 )
45 simprrr ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) )
46 44 45 jca ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
47 wrdfin ( 𝑥 ∈ Word 𝑇𝑥 ∈ Fin )
48 hashcl ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
49 44 47 48 3syl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
50 simp3l ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ∈ Word 𝑇 )
51 50 24 syl ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ∈ Fin )
52 simp2 ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ≠ ∅ )
53 51 52 28 syl2anc ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
54 53 adantr ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
55 simprrl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) )
56 54 nnred ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℝ )
57 2rp 2 ∈ ℝ+
58 ltsubrp ( ( ( ♯ ‘ 𝑤 ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( ♯ ‘ 𝑤 ) − 2 ) < ( ♯ ‘ 𝑤 ) )
59 56 57 58 sylancl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 2 ) < ( ♯ ‘ 𝑤 ) )
60 55 59 eqbrtrd ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑤 ) )
61 elfzo0 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑤 ) ∈ ℕ ∧ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑤 ) ) )
62 49 54 60 61 syl3anbrc ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) )
63 id ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) )
64 63 com13 ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) )
65 46 62 64 sylc ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) )
66 55 oveq2d ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑤 ) − 2 ) ) )
67 15 a1i ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → - 1 ∈ ℂ )
68 neg1ne0 - 1 ≠ 0
69 68 a1i ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → - 1 ≠ 0 )
70 2z 2 ∈ ℤ
71 70 a1i ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → 2 ∈ ℤ )
72 54 nnzd ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℤ )
73 67 69 71 72 expsubd ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ( ♯ ‘ 𝑤 ) − 2 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / ( - 1 ↑ 2 ) ) )
74 neg1sqe1 ( - 1 ↑ 2 ) = 1
75 74 oveq2i ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / ( - 1 ↑ 2 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / 1 )
76 m1expcl ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ ℤ )
77 76 zcnd ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ ℂ )
78 72 77 syl ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ ℂ )
79 78 div1d ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / 1 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
80 75 79 eqtrid ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / ( - 1 ↑ 2 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
81 66 73 80 3eqtrd ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
82 81 eqeq1d ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ↔ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
83 65 82 sylibd ( ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
84 83 ex ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
85 84 com23 ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
86 85 alimdv ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ∀ 𝑥 ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
87 19.23v ( ∀ 𝑥 ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
88 86 87 syl6ib ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
89 43 88 mpid ( ( 𝜑𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
90 89 3exp ( 𝜑 → ( 𝑤 ≠ ∅ → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) ) )
91 90 com34 ( 𝜑 → ( 𝑤 ≠ ∅ → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) ) )
92 91 com12 ( 𝑤 ≠ ∅ → ( 𝜑 → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) ) )
93 92 impd ( 𝑤 ≠ ∅ → ( ( 𝜑 ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
94 19 93 pm2.61ine ( ( 𝜑 ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
95 94 3adant2 ( ( 𝜑 ∧ ( ♯ ‘ 𝑤 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
96 eleq1 ( 𝑤 = 𝑥 → ( 𝑤 ∈ Word 𝑇𝑥 ∈ Word 𝑇 ) )
97 oveq2 ( 𝑤 = 𝑥 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑥 ) )
98 97 eqeq1d ( 𝑤 = 𝑥 → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
99 96 98 anbi12d ( 𝑤 = 𝑥 → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ↔ ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
100 fveq2 ( 𝑤 = 𝑥 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) )
101 100 oveq2d ( 𝑤 = 𝑥 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
102 101 eqeq1d ( 𝑤 = 𝑥 → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ↔ ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) )
103 99 102 imbi12d ( 𝑤 = 𝑥 → ( ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ↔ ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) )
104 eleq1 ( 𝑤 = 𝑊 → ( 𝑤 ∈ Word 𝑇𝑊 ∈ Word 𝑇 ) )
105 oveq2 ( 𝑤 = 𝑊 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑊 ) )
106 105 eqeq1d ( 𝑤 = 𝑊 → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) )
107 104 106 anbi12d ( 𝑤 = 𝑊 → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ↔ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) ) )
108 fveq2 ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
109 108 oveq2d ( 𝑤 = 𝑊 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
110 109 eqeq1d ( 𝑤 = 𝑊 → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ↔ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 ) )
111 107 110 imbi12d ( 𝑤 = 𝑊 → ( ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ↔ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 ) ) )
112 4 10 95 103 111 100 108 uzindi ( 𝜑 → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 ) )
113 4 5 112 mp2and ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 )