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 bilani ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ¬ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
38 1 2 21 22 23 29 30 37 psgnunilem3 ⊢ ¬ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
39 iman ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ↔ ¬ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
40 38 39 mpbir ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
41 df-rex ⊢ ( ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
42 40 41 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
43 simprl ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → 𝑥 ∈ Word 𝑇 )
44 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) )
45 43 44 jca ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
46 wrdfin ⊢ ( 𝑥 ∈ Word 𝑇 → 𝑥 ∈ Fin )
47 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
48 43 46 47 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
49 simp3l ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ∈ Word 𝑇 )
50 49 24 syl ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ∈ Fin )
51 simp2 ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → 𝑤 ≠ ∅ )
52 50 51 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
54 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) )
55 53 nnred ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℝ )
56 2rp ⊢ 2 ∈ ℝ+
57 ltsubrp ⊢ ( ( ( ♯ ‘ 𝑤 ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( ♯ ‘ 𝑤 ) − 2 ) < ( ♯ ‘ 𝑤 ) )
58 55 56 57 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 2 ) < ( ♯ ‘ 𝑤 ) )
59 54 58 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑤 ) )
60 elfzo0 ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑤 ) ∈ ℕ ∧ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑤 ) ) )
61 48 53 59 60 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) )
62 id ⊢ ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) )
63 62 com13 ⊢ ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) )
64 45 61 63 sylc ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) )
65 54 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑤 ) − 2 ) ) )
66 15 a1i ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → - 1 ∈ ℂ )
67 neg1ne0 ⊢ - 1 ≠ 0
68 67 a1i ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → - 1 ≠ 0 )
69 2z ⊢ 2 ∈ ℤ
70 69 a1i ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → 2 ∈ ℤ )
71 53 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℤ )
72 66 68 70 71 expsubd ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ( ♯ ‘ 𝑤 ) − 2 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / ( - 1 ↑ 2 ) ) )
73 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
74 73 oveq2i ⊢ ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / ( - 1 ↑ 2 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / 1 )
75 m1expcl ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ ℤ )
76 75 zcnd ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ ℂ )
77 71 76 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ ℂ )
78 77 div1d ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / 1 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
79 74 78 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) / ( - 1 ↑ 2 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
80 65 72 79 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
81 80 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ↔ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
82 64 81 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
83 82 ex ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
84 83 com23 ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
85 84 alimdv ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ∀ 𝑥 ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
86 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
87 85 86 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ Word 𝑇 ∧ ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑤 ) − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
88 42 87 mpid ⊢ ( ( 𝜑 ∧ 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
89 88 3exp ⊢ ( 𝜑 → ( 𝑤 ≠ ∅ → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) ) )
90 89 com34 ⊢ ( 𝜑 → ( 𝑤 ≠ ∅ → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) ) )
91 90 com12 ⊢ ( 𝑤 ≠ ∅ → ( 𝜑 → ( ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) ) )
92 91 impd ⊢ ( 𝑤 ≠ ∅ → ( ( 𝜑 ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ) )
93 19 92 pm2.61ine ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
94 93 3adant2 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑤 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑥 ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) ) → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) )
95 eleq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ Word 𝑇 ↔ 𝑥 ∈ Word 𝑇 ) )
96 oveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑥 ) )
97 96 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
98 95 97 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ↔ ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ) )
99 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) )
100 99 oveq2d ⊢ ( 𝑤 = 𝑥 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
101 100 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ↔ ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) )
102 98 101 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ↔ ( ( 𝑥 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = 1 ) ) )
103 eleq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ∈ Word 𝑇 ↔ 𝑊 ∈ Word 𝑇 ) )
104 oveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑊 ) )
105 104 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) )
106 103 105 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) ↔ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) ) )
107 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
108 107 oveq2d ⊢ ( 𝑤 = 𝑊 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
109 108 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ↔ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 ) )
110 106 109 imbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = 1 ) ↔ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 ) ) )
111 4 10 94 102 110 99 107 uzindi ⊢ ( 𝜑 → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 ) )
112 4 5 111 mp2and ⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = 1 )