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 sselid ⊢ ( 𝜑 → 𝐼 ∈ ( 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 eqtrid ⊢ ( 𝜑 → ( ( ♯ ‘ ∅ ) − ( ( 𝐼 + 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 63 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
65 64 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → 𝐺 ∈ Mnd )
66 2 1 61 symgtrf ⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
67 sswrd ⊢ ( 𝑇 ⊆ ( Base ‘ 𝐺 ) → Word 𝑇 ⊆ Word ( Base ‘ 𝐺 ) )
68 66 67 ax-mp ⊢ Word 𝑇 ⊆ Word ( Base ‘ 𝐺 )
69 68 4 sselid ⊢ ( 𝜑 → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
71 26 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
72 37 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
73 swrdcl ⊢ ( 𝑊 ∈ Word ( Base ‘ 𝐺 ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
74 69 73 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
76 wrd0 ⊢ ∅ ∈ Word ( Base ‘ 𝐺 )
77 76 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ∅ ∈ Word ( Base ‘ 𝐺 ) )
78 6 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝐿 ) )
79 27 78 eleqtrrd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
80 swrds2 ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ ( 𝐼 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ )
81 4 18 79 80 syl3anc ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ )
82 81 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( 𝐺 Σg ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ ) )
83 wrdf ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
84 4 83 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
85 78 feq2d ⊢ ( 𝜑 → ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 ↔ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑇 ) )
86 84 85 mpbid ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑇 )
87 86 7 ffvelrnd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐼 ) ∈ 𝑇 )
88 66 87 sselid ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐼 ) ∈ ( Base ‘ 𝐺 ) )
89 86 27 ffvelrnd ⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ 𝑇 )
90 66 89 sselid ⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ ( Base ‘ 𝐺 ) )
91 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
92 61 91 gsumws2 ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑊 ‘ 𝐼 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ ) = ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
93 64 88 90 92 syl3anc ⊢ ( 𝜑 → ( 𝐺 Σg ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ ) = ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
94 1 61 91 symgov ⊢ ( ( ( 𝑊 ‘ 𝐼 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
95 88 90 94 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐼 ) ( +g ‘ 𝐺 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
96 82 93 95 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
97 96 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
98 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) )
99 1 symgid ⊢ ( 𝐷 ∈ 𝑉 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
100 3 99 syl ⊢ ( 𝜑 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
101 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
102 101 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
103 100 102 eqtr4di ⊢ ( 𝜑 → ( I ↾ 𝐷 ) = ( 𝐺 Σg ∅ ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( I ↾ 𝐷 ) = ( 𝐺 Σg ∅ ) )
105 97 98 104 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( 𝐺 Σg ∅ ) )
106 61 65 70 71 72 75 77 105 gsumspl ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) )
107 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
108 60 106 107 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) )
109 fveqeq2 ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ↔ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) ) )
110 oveq2 ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( 𝐺 Σg 𝑥 ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) )
111 110 eqeq1d ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) ) )
112 109 111 anbi12d ⊢ ( 𝑥 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ( ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) ) ) )
113 112 rspcev ⊢ ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ∈ Word 𝑇 ∧ ( ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ∅ ⟩ ) ) = ( I ↾ 𝐷 ) ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
114 14 56 108 113 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
115 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
116 114 115 pm2.21dd ⊢ ( ( 𝜑 ∧ ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )
117 116 ex ⊢ ( 𝜑 → ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
118 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑊 ∈ Word 𝑇 )
119 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑟 ∈ 𝑇 )
120 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑠 ∈ 𝑇 )
121 119 120 s2cld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word 𝑇 )
122 splcl ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ⟨“ 𝑟 𝑠 ”⟩ ∈ Word 𝑇 ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 )
123 118 121 122 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 )
124 123 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ∈ Word 𝑇 )
125 64 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐺 ∈ Mnd )
126 69 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
127 26 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
128 37 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
129 68 121 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word ( Base ‘ 𝐺 ) )
130 129 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word ( Base ‘ 𝐺 ) )
131 74 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ∈ Word ( Base ‘ 𝐺 ) )
132 simprr1 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) )
133 96 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) = ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) )
134 64 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝐺 ∈ Mnd )
135 66 a1i ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
136 135 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑇 ) → 𝑟 ∈ ( Base ‘ 𝐺 ) )
137 136 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑟 ∈ ( Base ‘ 𝐺 ) )
138 135 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → 𝑠 ∈ ( Base ‘ 𝐺 ) )
139 138 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝑠 ∈ ( Base ‘ 𝐺 ) )
140 61 91 gsumws2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑟 ∈ ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) )
141 134 137 139 140 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) )
142 1 61 91 symgov ⊢ ( ( 𝑟 ∈ ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑟 ∘ 𝑠 ) )
143 137 139 142 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝑟 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑟 ∘ 𝑠 ) )
144 141 143 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ∘ 𝑠 ) )
145 144 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝑟 ∘ 𝑠 ) )
146 132 133 145 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑟 𝑠 ”⟩ ) = ( 𝐺 Σg ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ) )
147 61 125 126 127 128 130 131 146 gsumspl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) )
148 59 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) ⟩ ) ) = ( 𝐺 Σg 𝑊 ) )
149 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
150 147 148 149 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) )
151 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
152 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
153 118 151 152 121 spllen ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) )
154 s2len ⊢ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) = 2
155 154 oveq1i ⊢ ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = ( 2 − ( ( 𝐼 + 2 ) − 𝐼 ) )
156 46 oveq2d ⊢ ( 𝜑 → ( 2 − ( ( 𝐼 + 2 ) − 𝐼 ) ) = ( 2 − 2 ) )
157 44 subidi ⊢ ( 2 − 2 ) = 0
158 156 157 eqtrdi ⊢ ( 𝜑 → ( 2 − ( ( 𝐼 + 2 ) − 𝐼 ) ) = 0 )
159 155 158 eqtrid ⊢ ( 𝜑 → ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) = 0 )
160 159 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = ( ( ♯ ‘ 𝑊 ) + 0 ) )
161 6 52 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
162 161 addid1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + 0 ) = ( ♯ ‘ 𝑊 ) )
163 160 162 6 3eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = 𝐿 )
164 163 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( ♯ ‘ 𝑊 ) + ( ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) − ( ( 𝐼 + 2 ) − 𝐼 ) ) ) = 𝐿 )
165 153 164 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 )
166 165 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 )
167 150 166 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) )
168 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) )
169 simprr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐴 ∈ dom ( 𝑠 ∖ I ) )
170 1nn0 ⊢ 1 ∈ ℕ0
171 2nn ⊢ 2 ∈ ℕ
172 1lt2 ⊢ 1 < 2
173 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) )
174 170 171 172 173 mpbir3an ⊢ 1 ∈ ( 0 ..^ 2 )
175 154 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) ) = ( 0 ..^ 2 )
176 174 175 eleqtrri ⊢ 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) )
177 176 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) ) )
178 118 151 152 121 177 splfv2a ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) = ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 1 ) )
179 s2fv1 ⊢ ( 𝑠 ∈ 𝑇 → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 1 ) = 𝑠 )
180 179 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 1 ) = 𝑠 )
181 178 180 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) = 𝑠 )
182 181 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) = 𝑠 )
183 182 difeq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) = ( 𝑠 ∖ I ) )
184 183 dmeqd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) = dom ( 𝑠 ∖ I ) )
185 169 184 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) )
186 fzosplitsni ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
187 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
188 186 187 eleq2s ⊢ ( 𝐼 ∈ ℕ0 → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
189 18 188 syl ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
190 189 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) ) )
191 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ 𝑗 ) )
192 191 difeq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑊 ‘ 𝑘 ) ∖ I ) = ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
193 192 dmeqd ⊢ ( 𝑘 = 𝑗 → dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
194 193 eleq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) ↔ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) ) )
195 194 notbid ⊢ ( 𝑘 = 𝑗 → ( ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) ) )
196 195 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ 𝐼 ) ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
197 9 196 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
198 197 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
199 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → 𝑊 ∈ Word 𝑇 )
200 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 2 ) ) )
201 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ( 𝐼 + 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
202 121 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ⟨“ 𝑟 𝑠 ”⟩ ∈ Word 𝑇 )
203 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → 𝑗 ∈ ( 0 ..^ 𝐼 ) )
204 199 200 201 202 203 splfv1 ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) = ( 𝑊 ‘ 𝑗 ) )
205 204 difeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
206 205 dmeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑗 ) ∖ I ) )
207 198 206 neleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝐼 ) ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
208 207 ex ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝑗 ∈ ( 0 ..^ 𝐼 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
209 208 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ 𝐼 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
210 simprr3 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) )
211 0nn0 ⊢ 0 ∈ ℕ0
212 2pos ⊢ 0 < 2
213 elfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2 ) )
214 211 171 212 213 mpbir3an ⊢ 0 ∈ ( 0 ..^ 2 )
215 214 175 eleqtrri ⊢ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) )
216 215 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑟 𝑠 ”⟩ ) ) )
217 118 151 152 121 216 splfv2a ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 0 ) ) = ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 0 ) )
218 32 addid1d ⊢ ( 𝜑 → ( 𝐼 + 0 ) = 𝐼 )
219 218 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐼 + 0 ) = 𝐼 )
220 219 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 0 ) ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) )
221 s2fv0 ⊢ ( 𝑟 ∈ 𝑇 → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 0 ) = 𝑟 )
222 221 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ⟨“ 𝑟 𝑠 ”⟩ ‘ 0 ) = 𝑟 )
223 217 220 222 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) = 𝑟 )
224 223 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) = ( 𝑟 ∖ I ) )
225 224 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) = dom ( 𝑟 ∖ I ) )
226 225 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ↔ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
227 226 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ↔ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
228 210 227 mtbird ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) )
229 fveq2 ⊢ ( 𝑗 = 𝐼 → ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) )
230 229 difeq1d ⊢ ( 𝑗 = 𝐼 → ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) )
231 230 dmeqd ⊢ ( 𝑗 = 𝐼 → dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) = dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) )
232 231 eleq2d ⊢ ( 𝑗 = 𝐼 → ( 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ) )
233 232 notbid ⊢ ( 𝑗 = 𝐼 → ( ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝐼 ) ∖ I ) ) )
234 228 233 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 = 𝐼 → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
235 209 234 jaod ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝑗 ∈ ( 0 ..^ 𝐼 ) ∨ 𝑗 = 𝐼 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
236 190 235 sylbid ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) → ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
237 236 ralrimiv ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
238 168 185 237 3jca ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
239 oveq2 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) )
240 239 eqeq1d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ) )
241 fveqeq2 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( ♯ ‘ 𝑤 ) = 𝐿 ↔ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) )
242 240 241 anbi12d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ↔ ( ( 𝐺 Σg ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ) = 𝐿 ) ) )
243 fveq1 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝑤 ‘ ( 𝐼 + 1 ) ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) )
244 243 difeq1d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) = ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) )
245 244 dmeqd ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) = dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) )
246 245 eleq2d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ ( 𝐼 + 1 ) ) ∖ I ) ) )
247 fveq1 ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝑤 ‘ 𝑗 ) = ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) )
248 247 difeq1d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ( 𝑤 ‘ 𝑗 ) ∖ I ) = ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
249 248 dmeqd ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) = dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) )
250 249 eleq2d ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
251 250 notbid ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
252 251 ralbidv ⊢ ( 𝑤 = ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( ( 𝑊 splice ⟨ 𝐼 , ( 𝐼 + 2 ) , ⟨“ 𝑟 𝑠 ”⟩ ⟩ ) ‘ 𝑗 ) ∖ I ) ) )
253 246 252 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 ) ) ) )
254 242 253 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 ) ) ) ) )
255 254 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 ) ) ) )
256 124 167 238 255 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )
257 256 expr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇 ) ) → ( ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
258 257 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
259 2 3 87 89 8 psgnunilem1 ⊢ ( 𝜑 → ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( ( 𝑊 ‘ 𝐼 ) ∘ ( 𝑊 ‘ ( 𝐼 + 1 ) ) ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )
260 117 258 259 mpjaod ⊢ ( 𝜑 → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝐴 ∈ dom ( ( 𝑤 ‘ ( 𝐼 + 1 ) ) ∖ I ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ¬ 𝐴 ∈ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) )