Metamath Proof Explorer

Theorem psgnunilem2

Description: Lemma for psgnuni . Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses psgnunilem2.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnunilem2.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnunilem2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
psgnunilem2.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
psgnunilem2.id ⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
psgnunilem2.l ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝐿 )
psgnunilem2.ix ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝐿 ) )
psgnunilem2.a ⊢ ( 𝜑 → 𝐴 ∈ dom ( ( 𝑊 ‘ 𝐼 ) ∖ I ) )
psgnunilem2.al ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝐼 ) ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) )
psgnunilem2.in ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
Assertion psgnunilem2 ( 𝜑 → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnunilem2.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnunilem2.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnunilem2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4 psgnunilem2.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
5 psgnunilem2.id ⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
6 psgnunilem2.l ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝐿 )
7 psgnunilem2.ix ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝐿 ) )
8 psgnunilem2.a ⊢ ( 𝜑 → 𝐴 ∈ dom ( ( 𝑊 ‘ 𝐼 ) ∖ I ) )
9 psgnunilem2.al ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝐼 ) ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) )
10 psgnunilem2.in ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
11 wrd0 ⊢ ∅ ∈ Word 𝑇
12 splcl ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇 ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ∈ Word 𝑇 )
13 4 11 12 sylancl ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ∈ Word 𝑇 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ∈ Word 𝑇 )
15 fzossfz ⊢ ( 0 ..^ 𝐿 ) ⊆ ( 0 ... 𝐿 )
16 15 7 sseldi ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝐿 ) )
17 elfznn0 ⊢ ( 𝐼 ∈ ( 0 ... 𝐿 ) → 𝐼 ∈ ℕ0 )
18 16 17 syl ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
19 2nn0 ⊢ 2 ∈ ℕ0
20 nn0addcl ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 𝐼 + 2 ) ∈ ℕ0 )
21 18 19 20 sylancl ⊢ ( 𝜑 → ( 𝐼 + 2 ) ∈ ℕ0 )
22 18 nn0red ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
23 nn0addge1 ⊢ ( ( 𝐼 ∈ ℝ ∧ 2 ∈ ℕ0 ) → 𝐼 ≤ ( 𝐼 + 2 ) )
24 22 19 23 sylancl ⊢ ( 𝜑 → 𝐼 ≤ ( 𝐼 + 2 ) )
25 elfz2nn0 ⊢ ( 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( 𝐼 + 2 ) ∈ ℕ0 ∧ 𝐼 ≤ ( 𝐼 + 2 ) ) )
26 18 21 24 25 syl3anbrc ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
27 1 2 3 4 5 6 7 8 9 psgnunilem5 ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) )
28 fzofzp1 ⊢ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) → ( ( 𝐼 + 1 ) + 1 ) ∈ ( 0 ... 𝐿 ) )
29 27 28 syl ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) + 1 ) ∈ ( 0 ... 𝐿 ) )
30 df-2 ⊢ 2 = ( 1 + 1 )
31 30 oveq2i ⊢ ( 𝐼 + 2 ) = ( 𝐼 + ( 1 + 1 ) )
32 18 nn0cnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
33 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
34 32 33 33 addassd ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) + 1 ) = ( 𝐼 + ( 1 + 1 ) ) )
35 31 34 eqtr4id ⊢ ( 𝜑 → ( 𝐼 + 2 ) = ( ( 𝐼 + 1 ) + 1 ) )
36 6 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... 𝐿 ) )
37 29 35 36 3eltr4d ⊢ ( 𝜑 → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
38 11 a1i ⊢ ( 𝜑 → ∅ ∈ Word 𝑇 )
39 4 26 37 38 spllen ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ∅ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) )
40 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
41 40 oveq1i ⊢ ( ( ♯ ‘ ∅ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = ( 0 − ( ( 𝐼 + 2 ) − 𝐼 ) )
42 df-neg ⊢ - ( ( 𝐼 + 2 ) − 𝐼 ) = ( 0 − ( ( 𝐼 + 2 ) − 𝐼 ) )
43 41 42 eqtr4i ⊢ ( ( ♯ ‘ ∅ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = - ( ( 𝐼 + 2 ) − 𝐼 )
44 2cn ⊢ 2 ∈ ℂ
45 pncan2 ⊢ ( ( 𝐼 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝐼 + 2 ) − 𝐼 ) = 2 )
46 32 44 45 sylancl ⊢ ( 𝜑 → ( ( 𝐼 + 2 ) − 𝐼 ) = 2 )
47 46 negeqd ⊢ ( 𝜑 → - ( ( 𝐼 + 2 ) − 𝐼 ) = - 2 )
48 43 47 syl5eq ⊢ ( 𝜑 → ( ( ♯ ‘ ∅ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = - 2 )
49 6 48 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ∅ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = ( 𝐿 + - 2 ) )
50 elfzel2 ⊢ ( 𝐼 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ℤ )
51 16 50 syl ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
52 51 zcnd ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
53 negsub ⊢ ( ( 𝐿 ∈ ℂ ∧ 2 ∈ ℂ ) → ( 𝐿 + - 2 ) = ( 𝐿 − 2 ) )
54 52 44 53 sylancl ⊢ ( 𝜑 → ( 𝐿 + - 2 ) = ( 𝐿 − 2 ) )
55 39 49 54 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) )
57 splid ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) ∧ ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) = 𝑊 )
58 4 26 37 57 syl12anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) = 𝑊 )
59 58 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) = ( 𝐺 Σg 𝑊 ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) = ( 𝐺 Σg 𝑊 ) )
61 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
62 1 symggrp ⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Grp )
63 3 62 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
64 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
65 63 64 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
66 65 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → 𝐺 ∈ Mnd )
67 2 1 61 symgtrf ⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
68 sswrd ⊢ ( 𝑇 ⊆ ( Base ‘ 𝐺 ) → Word 𝑇 ⊆ Word ( Base ‘ 𝐺 ) )
69 67 68 ax-mp ⊢ Word 𝑇 ⊆ Word ( Base ‘ 𝐺 )
70 69 4 sseldi ⊢ ( 𝜑 → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
72 26 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
73 37 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
74 swrdcl ⊢ ( 𝑊 ∈ Word ( Base ‘ 𝐺 ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
75 70 74 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
77 wrd0 ⊢ ∅ ∈ Word ( Base ‘ 𝐺 )
78 77 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ∅ ∈ Word ( Base ‘ 𝐺 ) )
79 6 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝐿 ) )
80 27 79 eleqtrrd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
81 swrds2 ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ ( 𝐼 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ )
82 4 18 80 81 syl3anc ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ )
83 82 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( 𝐺 Σg ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ ) )
84 wrdf ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
85 4 84 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
86 79 feq2d ⊢ ( 𝜑 → ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 ↔ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑇 ) )
87 85 86 mpbid ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑇 )
88 87 7 ffvelrnd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐼 ) ∈ 𝑇 )
89 67 88 sseldi ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐼 ) ∈ ( Base ‘ 𝐺 ) )
90 87 27 ffvelrnd ⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ 𝑇 )
91 67 90 sseldi ⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ ( Base ‘ 𝐺 ) )
92 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
93 61 92 gsumws2 ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑊 ‘ 𝐼 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ ) = ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
94 65 89 91 93 syl3anc ⊢ ( 𝜑 → ( 𝐺 Σg ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ ) = ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
95 1 61 92 symgov ⊢ ( ( ( 𝑊 ‘ 𝐼 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
96 89 91 95 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
97 83 94 96 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
99 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) )
100 1 symgid ⊢ ( 𝐷 ∈ 𝑉 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
101 3 100 syl ⊢ ( 𝜑 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
102 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
103 102 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
104 101 103 eqtr4di ⊢ ( 𝜑 → ( I ↾ 𝐷 ) = ( 𝐺 Σg ∅ ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( I ↾ 𝐷 ) = ( 𝐺 Σg ∅ ) )
106 98 99 105 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( 𝐺 Σg ∅ ) )
107 61 66 71 72 73 76 78 106 gsumspl ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) )
108 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
109 60 107 108 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) )
110 fveqeq2 ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ↔ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) ) )
111 oveq2 ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( 𝐺 Σg 𝑥 ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) )
112 111 eqeq1d ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) ) )
113 110 112 anbi12d ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ( ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) ) ) )
114 113 rspcev ⊢ ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ∈ Word 𝑇 ∧ ( ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
115 14 56 109 114 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
116 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
117 115 116 pm2.21dd ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )
118 117 ex ⊢ ( 𝜑 → ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
119 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑊 ∈ Word 𝑇 )
120 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑟 ∈ 𝑇 )
121 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑠 ∈ 𝑇 )
122 120 121 s2cld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word 𝑇 )
123 splcl ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ⟨“ 𝑟 𝑠 ”⟩ ∈ Word 𝑇 ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 )
124 119 122 123 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 )
125 124 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 )
126 65 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐺 ∈ Mnd )
127 70 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
128 26 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
129 37 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
130 69 122 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word ( Base ‘ 𝐺 ) )
131 130 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word ( Base ‘ 𝐺 ) )
132 75 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
133 simprr1 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) )
134 97 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
135 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝐺 ∈ Mnd )
136 67 a1i ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
137 136 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑇 ) → 𝑟 ∈ ( Base ‘ 𝐺 ) )
138 137 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑟 ∈ ( Base ‘ 𝐺 ) )
139 136 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → 𝑠 ∈ ( Base ‘ 𝐺 ) )
140 139 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑠 ∈ ( Base ‘ 𝐺 ) )
141 61 92 gsumws2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑟 ∈ ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) )
142 135 138 140 141 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) )
143 1 61 92 symgov ⊢ ( ( 𝑟 ∈ ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑟 ∘ 𝑠 ) )
144 138 140 143 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑟 ∘ 𝑠 ) )
145 142 144 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ∘ 𝑠 ) )
146 145 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ∘ 𝑠 ) )
147 133 134 146 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) )
148 61 126 127 128 129 131 132 147 gsumspl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) )
149 59 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) = ( 𝐺 Σg 𝑊 ) )
150 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
151 148 149 150 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) )
152 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
153 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
154 119 152 153 122 spllen ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) )
155 s2len ⊢ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) = 2
156 155 oveq1i ⊢ ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = ( 2 − ( ( 𝐼 + 2 ) − 𝐼 ) )
157 46 oveq2d ⊢ ( 𝜑 → ( 2 − ( ( 𝐼 + 2 ) − 𝐼 ) ) = ( 2 − 2 ) )
158 44 subidi ⊢ ( 2 − 2 ) = 0
159 157 158 eqtrdi ⊢ ( 𝜑 → ( 2 − ( ( 𝐼 + 2 ) − 𝐼 ) ) = 0 )
160 156 159 syl5eq ⊢ ( 𝜑 → ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = 0 )
161 160 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = ( ( ♯ ‘ 𝑊 ) + 0 ) )
162 6 52 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
163 162 addid1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + 0 ) = ( ♯ ‘ 𝑊 ) )
164 161 163 6 3eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = 𝐿 )
165 164 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = 𝐿 )
166 154 165 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 )
167 166 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 )
168 151 167 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) )
169 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) )
170 simprr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐴 ∈ dom ( 𝑠 ∖ I ) )
171 1nn0 ⊢ 1 ∈ ℕ0
172 2nn ⊢ 2 ∈ ℕ
173 1lt2 ⊢ 1 < 2
174 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) )
175 171 172 173 174 mpbir3an ⊢ 1 ∈ ( 0 ..^ 2 )
176 155 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) ) = ( 0 ..^ 2 )
177 175 176 eleqtrri ⊢ 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) )
178 177 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) ) )
179 119 152 153 122 178 splfv2a ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) = ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 1 ) )
180 s2fv1 ⊢ ( 𝑠 ∈ 𝑇 → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 1 ) = 𝑠 )
181 180 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 1 ) = 𝑠 )
182 179 181 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) = 𝑠 )
183 182 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) = 𝑠 )
184 183 difeq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) = ( 𝑠 ∖ I ) )
185 184 dmeqd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) = dom ( 𝑠 ∖ I ) )
186 170 185 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) )
187 fzosplitsni ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
188 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
189 187 188 eleq2s ⊢ ( 𝐼 ∈ ℕ0 → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
190 18 189 syl ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
191 190 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
192 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ 𝑗 ) )
193 192 difeq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑊 ‘ 𝑘 ) ∖ I ) = ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
194 193 dmeqd ⊢ ( 𝑘 = 𝑗 → dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
195 194 eleq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) ↔ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) ) )
196 195 notbid ⊢ ( 𝑘 = 𝑗 → ( ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) ) )
197 196 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ 𝐼 ) ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
198 9 197 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
199 198 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
200 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → 𝑊 ∈ Word 𝑇 )
201 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
202 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
203 122 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word 𝑇 )
204 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → 𝑗 ∈ ( 0 ..^ 𝐼 ) )
205 200 201 202 203 204 splfv1 ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) = ( 𝑊 ‘ 𝑗 ) )
206 205 difeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
207 206 dmeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
208 199 207 neleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
209 208 ex ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝑗 ∈ ( 0 ..^ 𝐼 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
210 209 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ 𝐼 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
211 simprr3 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) )
212 0nn0 ⊢ 0 ∈ ℕ0
213 2pos ⊢ 0 < 2
214 elfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2 ) )
215 212 172 213 214 mpbir3an ⊢ 0 ∈ ( 0 ..^ 2 )
216 215 176 eleqtrri ⊢ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) )
217 216 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) ) )
218 119 152 153 122 217 splfv2a ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 0 ) ) = ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 0 ) )
219 32 addid1d ⊢ ( 𝜑 → ( 𝐼 + 0 ) = 𝐼 )
220 219 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐼 + 0 ) = 𝐼 )
221 220 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 0 ) ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) )
222 s2fv0 ⊢ ( 𝑟 ∈ 𝑇 → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 0 ) = 𝑟 )
223 222 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 0 ) = 𝑟 )
224 218 221 223 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) = 𝑟 )
225 224 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) = ( 𝑟 ∖ I ) )
226 225 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) = dom ( 𝑟 ∖ I ) )
227 226 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ↔ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
228 227 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ↔ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
229 211 228 mtbird ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) )
230 fveq2 ⊢ ( 𝑗 = 𝐼 → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) )
231 230 difeq1d ⊢ ( 𝑗 = 𝐼 → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) )
232 231 dmeqd ⊢ ( 𝑗 = 𝐼 → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) )
233 232 eleq2d ⊢ ( 𝑗 = 𝐼 → ( 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ) )
234 233 notbid ⊢ ( 𝑗 = 𝐼 → ( ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ) )
235 229 234 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 = 𝐼 → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
236 210 235 jaod ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
237 191 236 sylbid ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
238 237 ralrimiv ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
239 169 186 238 3jca ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
240 oveq2 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) )
241 240 eqeq1d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ) )
242 fveqeq2 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( ♯ ‘ 𝑤 ) = 𝐿 ↔ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) )
243 241 242 anbi12d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ↔ ( ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) ) )
244 fveq1 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝑤 ‘ ( 𝐼 + 1 ) ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) )
245 244 difeq1d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) = ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) )
246 245 dmeqd ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) = dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) )
247 246 eleq2d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ) )
248 fveq1 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝑤 ‘ 𝑗 ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) )
249 248 difeq1d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( 𝑤 ‘ 𝑗 ) ∖ I ) = ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
250 249 dmeqd ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) = dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
251 250 eleq2d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
252 251 notbid ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
253 252 ralbidv ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
254 247 253 3anbi23d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ↔ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) ) )
255 243 254 anbi12d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) ) ) )
256 255 rspcev ⊢ ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )
257 125 168 239 256 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )
258 257 expr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
259 258 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
260 2 3 88 90 8 psgnunilem1 ⊢ ( 𝜑 → ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )
261 118 259 260 mpjaod ⊢ ( 𝜑 → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )