Metamath Proof Explorer

Theorem psgnunilem3

Description: Lemma for psgnuni . Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypotheses psgnunilem3.g ⊢ G = SymGrp ⁡ D
psgnunilem3.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnunilem3.d ⊢ φ → D ∈ V
psgnunilem3.w1 ⊢ φ → W ∈ Word T
psgnunilem3.l ⊢ φ → W = L
psgnunilem3.w2 ⊢ φ → W ∈ ℕ
psgnunilem3.w3 ⊢ φ → ∑ G W = I ↾ D
psgnunilem3.in ⊢ φ → ¬ ∃ x ∈ Word T x = L − 2 ∧ ∑ G x = I ↾ D
Assertion psgnunilem3 ⊢ ¬ φ

Proof

Step Hyp Ref Expression
1 psgnunilem3.g ⊢ G = SymGrp ⁡ D
2 psgnunilem3.t ⊢ T = ran ⁡ pmTrsp ⁡ D
3 psgnunilem3.d ⊢ φ → D ∈ V
4 psgnunilem3.w1 ⊢ φ → W ∈ Word T
5 psgnunilem3.l ⊢ φ → W = L
6 psgnunilem3.w2 ⊢ φ → W ∈ ℕ
7 psgnunilem3.w3 ⊢ φ → ∑ G W = I ↾ D
8 psgnunilem3.in ⊢ φ → ¬ ∃ x ∈ Word T x = L − 2 ∧ ∑ G x = I ↾ D
9 5 6 eqeltrrd ⊢ φ → L ∈ ℕ
10 9 nnnn0d ⊢ φ → L ∈ ℕ 0
11 wrdf ⊢ W ∈ Word T → W : 0 ..^ W ⟶ T
12 4 11 syl ⊢ φ → W : 0 ..^ W ⟶ T
13 0nn0 ⊢ 0 ∈ ℕ 0
14 13 a1i ⊢ φ → 0 ∈ ℕ 0
15 9 nngt0d ⊢ φ → 0 < L
16 elfzo0 ⊢ 0 ∈ 0 ..^ L ↔ 0 ∈ ℕ 0 ∧ L ∈ ℕ ∧ 0 < L
17 14 9 15 16 syl3anbrc ⊢ φ → 0 ∈ 0 ..^ L
18 5 oveq2d ⊢ φ → 0 ..^ W = 0 ..^ L
19 17 18 eleqtrrd ⊢ φ → 0 ∈ 0 ..^ W
20 12 19 ffvelcdmd ⊢ φ → W ⁡ 0 ∈ T
21 eqid ⊢ pmTrsp ⁡ D = pmTrsp ⁡ D
22 21 2 pmtrfmvdn0 ⊢ W ⁡ 0 ∈ T → dom ⁡ W ⁡ 0 ∖ I ≠ ∅
23 20 22 syl ⊢ φ → dom ⁡ W ⁡ 0 ∖ I ≠ ∅
24 n0 ⊢ dom ⁡ W ⁡ 0 ∖ I ≠ ∅ ↔ ∃ e e ∈ dom ⁡ W ⁡ 0 ∖ I
25 23 24 sylib ⊢ φ → ∃ e e ∈ dom ⁡ W ⁡ 0 ∖ I
26 fzonel ⊢ ¬ L ∈ 0 ..^ L
27 simpr1 ⊢ ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I → L ∈ 0 ..^ L
28 26 27 mto ⊢ ¬ ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
29 28 a1i ⊢ w ∈ Word T → ¬ ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
30 29 nrex ⊢ ¬ ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
31 eleq1 ⊢ a = 0 → a ∈ 0 ..^ L ↔ 0 ∈ 0 ..^ L
32 fveq2 ⊢ a = 0 → w ⁡ a = w ⁡ 0
33 32 difeq1d ⊢ a = 0 → w ⁡ a ∖ I = w ⁡ 0 ∖ I
34 33 dmeqd ⊢ a = 0 → dom ⁡ w ⁡ a ∖ I = dom ⁡ w ⁡ 0 ∖ I
35 34 eleq2d ⊢ a = 0 → e ∈ dom ⁡ w ⁡ a ∖ I ↔ e ∈ dom ⁡ w ⁡ 0 ∖ I
36 oveq2 ⊢ a = 0 → 0 ..^ a = 0 ..^ 0
37 36 raleqdv ⊢ a = 0 → ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
38 31 35 37 3anbi123d ⊢ a = 0 → a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
39 38 anbi2d ⊢ a = 0 → ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∑ G w = I ↾ D ∧ w = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
40 39 rexbidv ⊢ a = 0 → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
41 40 imbi2d ⊢ a = 0 → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
42 eleq1 ⊢ a = b → a ∈ 0 ..^ L ↔ b ∈ 0 ..^ L
43 fveq2 ⊢ a = b → w ⁡ a = w ⁡ b
44 43 difeq1d ⊢ a = b → w ⁡ a ∖ I = w ⁡ b ∖ I
45 44 dmeqd ⊢ a = b → dom ⁡ w ⁡ a ∖ I = dom ⁡ w ⁡ b ∖ I
46 45 eleq2d ⊢ a = b → e ∈ dom ⁡ w ⁡ a ∖ I ↔ e ∈ dom ⁡ w ⁡ b ∖ I
47 oveq2 ⊢ a = b → 0 ..^ a = 0 ..^ b
48 47 raleqdv ⊢ a = b → ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I
49 42 46 48 3anbi123d ⊢ a = b → a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b ∖ I ∧ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I
50 49 anbi2d ⊢ a = b → ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∑ G w = I ↾ D ∧ w = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b ∖ I ∧ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I
51 50 rexbidv ⊢ a = b → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b ∖ I ∧ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I
52 oveq2 ⊢ w = x → ∑ G w = ∑ G x
53 52 eqeq1d ⊢ w = x → ∑ G w = I ↾ D ↔ ∑ G x = I ↾ D
54 fveqeq2 ⊢ w = x → w = L ↔ x = L
55 53 54 anbi12d ⊢ w = x → ∑ G w = I ↾ D ∧ w = L ↔ ∑ G x = I ↾ D ∧ x = L
56 fveq1 ⊢ w = x → w ⁡ b = x ⁡ b
57 56 difeq1d ⊢ w = x → w ⁡ b ∖ I = x ⁡ b ∖ I
58 57 dmeqd ⊢ w = x → dom ⁡ w ⁡ b ∖ I = dom ⁡ x ⁡ b ∖ I
59 58 eleq2d ⊢ w = x → e ∈ dom ⁡ w ⁡ b ∖ I ↔ e ∈ dom ⁡ x ⁡ b ∖ I
60 fveq1 ⊢ w = x → w ⁡ c = x ⁡ c
61 60 difeq1d ⊢ w = x → w ⁡ c ∖ I = x ⁡ c ∖ I
62 61 dmeqd ⊢ w = x → dom ⁡ w ⁡ c ∖ I = dom ⁡ x ⁡ c ∖ I
63 62 eleq2d ⊢ w = x → e ∈ dom ⁡ w ⁡ c ∖ I ↔ e ∈ dom ⁡ x ⁡ c ∖ I
64 63 notbid ⊢ w = x → ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ¬ e ∈ dom ⁡ x ⁡ c ∖ I
65 64 ralbidv ⊢ w = x → ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ c ∖ I
66 fveq2 ⊢ c = d → x ⁡ c = x ⁡ d
67 66 difeq1d ⊢ c = d → x ⁡ c ∖ I = x ⁡ d ∖ I
68 67 dmeqd ⊢ c = d → dom ⁡ x ⁡ c ∖ I = dom ⁡ x ⁡ d ∖ I
69 68 eleq2d ⊢ c = d → e ∈ dom ⁡ x ⁡ c ∖ I ↔ e ∈ dom ⁡ x ⁡ d ∖ I
70 69 notbid ⊢ c = d → ¬ e ∈ dom ⁡ x ⁡ c ∖ I ↔ ¬ e ∈ dom ⁡ x ⁡ d ∖ I
71 70 cbvralvw ⊢ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ c ∖ I ↔ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
72 65 71 bitrdi ⊢ w = x → ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
73 59 72 3anbi23d ⊢ w = x → b ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b ∖ I ∧ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
74 55 73 anbi12d ⊢ w = x → ∑ G w = I ↾ D ∧ w = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b ∖ I ∧ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
75 74 cbvrexvw ⊢ ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b ∖ I ∧ ∀ c ∈ 0 ..^ b ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∃ x ∈ Word T ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
76 51 75 bitrdi ⊢ a = b → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∃ x ∈ Word T ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
77 76 imbi2d ⊢ a = b → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ x ∈ Word T ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
78 eleq1 ⊢ a = b + 1 → a ∈ 0 ..^ L ↔ b + 1 ∈ 0 ..^ L
79 fveq2 ⊢ a = b + 1 → w ⁡ a = w ⁡ b + 1
80 79 difeq1d ⊢ a = b + 1 → w ⁡ a ∖ I = w ⁡ b + 1 ∖ I
81 80 dmeqd ⊢ a = b + 1 → dom ⁡ w ⁡ a ∖ I = dom ⁡ w ⁡ b + 1 ∖ I
82 81 eleq2d ⊢ a = b + 1 → e ∈ dom ⁡ w ⁡ a ∖ I ↔ e ∈ dom ⁡ w ⁡ b + 1 ∖ I
83 oveq2 ⊢ a = b + 1 → 0 ..^ a = 0 ..^ b + 1
84 83 raleqdv ⊢ a = b + 1 → ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
85 78 82 84 3anbi123d ⊢ a = b + 1 → a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
86 85 anbi2d ⊢ a = b + 1 → ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
87 86 rexbidv ⊢ a = b + 1 → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
88 87 imbi2d ⊢ a = b + 1 → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
89 eleq1 ⊢ a = L → a ∈ 0 ..^ L ↔ L ∈ 0 ..^ L
90 fveq2 ⊢ a = L → w ⁡ a = w ⁡ L
91 90 difeq1d ⊢ a = L → w ⁡ a ∖ I = w ⁡ L ∖ I
92 91 dmeqd ⊢ a = L → dom ⁡ w ⁡ a ∖ I = dom ⁡ w ⁡ L ∖ I
93 92 eleq2d ⊢ a = L → e ∈ dom ⁡ w ⁡ a ∖ I ↔ e ∈ dom ⁡ w ⁡ L ∖ I
94 oveq2 ⊢ a = L → 0 ..^ a = 0 ..^ L
95 94 raleqdv ⊢ a = L → ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
96 89 93 95 3anbi123d ⊢ a = L → a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
97 96 anbi2d ⊢ a = L → ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
98 97 rexbidv ⊢ a = L → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
99 98 imbi2d ⊢ a = L → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ a ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ a ∖ I ∧ ∀ c ∈ 0 ..^ a ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
100 4 adantr ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → W ∈ Word T
101 7 5 jca ⊢ φ → ∑ G W = I ↾ D ∧ W = L
102 101 adantr ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∑ G W = I ↾ D ∧ W = L
103 17 adantr ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → 0 ∈ 0 ..^ L
104 simpr ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → e ∈ dom ⁡ W ⁡ 0 ∖ I
105 ral0 ⊢ ∀ c ∈ ∅ ¬ e ∈ dom ⁡ W ⁡ c ∖ I
106 fzo0 ⊢ 0 ..^ 0 = ∅
107 106 raleqi ⊢ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I ↔ ∀ c ∈ ∅ ¬ e ∈ dom ⁡ W ⁡ c ∖ I
108 105 107 mpbir ⊢ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I
109 108 a1i ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I
110 103 104 109 3jca ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I
111 oveq2 ⊢ w = W → ∑ G w = ∑ G W
112 111 eqeq1d ⊢ w = W → ∑ G w = I ↾ D ↔ ∑ G W = I ↾ D
113 fveqeq2 ⊢ w = W → w = L ↔ W = L
114 112 113 anbi12d ⊢ w = W → ∑ G w = I ↾ D ∧ w = L ↔ ∑ G W = I ↾ D ∧ W = L
115 fveq1 ⊢ w = W → w ⁡ 0 = W ⁡ 0
116 115 difeq1d ⊢ w = W → w ⁡ 0 ∖ I = W ⁡ 0 ∖ I
117 116 dmeqd ⊢ w = W → dom ⁡ w ⁡ 0 ∖ I = dom ⁡ W ⁡ 0 ∖ I
118 117 eleq2d ⊢ w = W → e ∈ dom ⁡ w ⁡ 0 ∖ I ↔ e ∈ dom ⁡ W ⁡ 0 ∖ I
119 fveq1 ⊢ w = W → w ⁡ c = W ⁡ c
120 119 difeq1d ⊢ w = W → w ⁡ c ∖ I = W ⁡ c ∖ I
121 120 dmeqd ⊢ w = W → dom ⁡ w ⁡ c ∖ I = dom ⁡ W ⁡ c ∖ I
122 121 eleq2d ⊢ w = W → e ∈ dom ⁡ w ⁡ c ∖ I ↔ e ∈ dom ⁡ W ⁡ c ∖ I
123 122 notbid ⊢ w = W → ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ¬ e ∈ dom ⁡ W ⁡ c ∖ I
124 123 ralbidv ⊢ w = W → ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I
125 118 124 3anbi23d ⊢ w = W → 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I
126 114 125 anbi12d ⊢ w = W → ∑ G w = I ↾ D ∧ w = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I ↔ ∑ G W = I ↾ D ∧ W = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I
127 126 rspcev ⊢ W ∈ Word T ∧ ∑ G W = I ↾ D ∧ W = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ W ⁡ c ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
128 100 102 110 127 syl12anc ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ 0 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ 0 ∖ I ∧ ∀ c ∈ 0 ..^ 0 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
129 3 ad2antrr ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → D ∈ V
130 simprl ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → x ∈ Word T
131 simpll ⊢ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ∑ G x = I ↾ D
132 131 ad2antll ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ∑ G x = I ↾ D
133 simplr ⊢ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → x = L
134 133 ad2antll ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → x = L
135 simpr1 ⊢ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → b ∈ 0 ..^ L
136 135 ad2antll ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → b ∈ 0 ..^ L
137 simpr2 ⊢ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → e ∈ dom ⁡ x ⁡ b ∖ I
138 137 ad2antll ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → e ∈ dom ⁡ x ⁡ b ∖ I
139 simpr3 ⊢ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
140 139 ad2antll ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I
141 fveqeq2 ⊢ x = y → x = L − 2 ↔ y = L − 2
142 oveq2 ⊢ x = y → ∑ G x = ∑ G y
143 142 eqeq1d ⊢ x = y → ∑ G x = I ↾ D ↔ ∑ G y = I ↾ D
144 141 143 anbi12d ⊢ x = y → x = L − 2 ∧ ∑ G x = I ↾ D ↔ y = L − 2 ∧ ∑ G y = I ↾ D
145 144 cbvrexvw ⊢ ∃ x ∈ Word T x = L − 2 ∧ ∑ G x = I ↾ D ↔ ∃ y ∈ Word T y = L − 2 ∧ ∑ G y = I ↾ D
146 8 145 sylnib ⊢ φ → ¬ ∃ y ∈ Word T y = L − 2 ∧ ∑ G y = I ↾ D
147 146 ad2antrr ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ¬ ∃ y ∈ Word T y = L − 2 ∧ ∑ G y = I ↾ D
148 1 2 129 130 132 134 136 138 140 147 psgnunilem2 ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I ∧ x ∈ Word T ∧ ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
149 148 rexlimdvaa ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ x ∈ Word T ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
150 149 a2i ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ x ∈ Word T ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
151 150 a1i ⊢ b ∈ ℕ 0 → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ x ∈ Word T ∑ G x = I ↾ D ∧ x = L ∧ b ∈ 0 ..^ L ∧ e ∈ dom ⁡ x ⁡ b ∖ I ∧ ∀ d ∈ 0 ..^ b ¬ e ∈ dom ⁡ x ⁡ d ∖ I → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ b + 1 ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ b + 1 ∖ I ∧ ∀ c ∈ 0 ..^ b + 1 ¬ e ∈ dom ⁡ w ⁡ c ∖ I
152 41 77 88 99 128 151 nn0ind ⊢ L ∈ ℕ 0 → φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ∃ w ∈ Word T ∑ G w = I ↾ D ∧ w = L ∧ L ∈ 0 ..^ L ∧ e ∈ dom ⁡ w ⁡ L ∖ I ∧ ∀ c ∈ 0 ..^ L ¬ e ∈ dom ⁡ w ⁡ c ∖ I
153 30 152 mtoi ⊢ L ∈ ℕ 0 → ¬ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I
154 153 con2i ⊢ φ ∧ e ∈ dom ⁡ W ⁡ 0 ∖ I → ¬ L ∈ ℕ 0
155 25 154 exlimddv ⊢ φ → ¬ L ∈ ℕ 0
156 10 155 pm2.65i ⊢ ¬ φ