MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  clwwlknonex2lem2 Structured version   Visualization version   GIF version

Theorem clwwlknonex2lem2 27253
Description: Lemma 2 for clwwlknonex2 27254: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.)
Hypotheses
Ref Expression
clwwlknonex2.v 𝑉 = (Vtx‘𝐺)
clwwlknonex2.e 𝐸 = (Edg‘𝐺)
Assertion
Ref Expression
clwwlknonex2lem2 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
Distinct variable groups:   𝑖,𝐸   𝑖,𝑉   𝑖,𝑊   𝑖,𝑋   𝑖,𝑌
Allowed substitution hints:   𝐺(𝑖)   𝑁(𝑖)

Proof of Theorem clwwlknonex2lem2
StepHypRef Expression
1 simpll 807 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉)
2 elfzonn0 12703 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 ∈ ℕ0)
32adantl 473 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ ℕ0)
4 lencl 13506 . . . . . . . . . . . . . . . . . 18 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ0)
5 elfzo0 12699 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^((♯‘𝑊) − 1)) ↔ (𝑖 ∈ ℕ0 ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)))
6 nn0re 11489 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
76adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → 𝑖 ∈ ℝ)
8 nn0re 11489 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝑊) ∈ ℕ0 → (♯‘𝑊) ∈ ℝ)
9 peano2rem 10536 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝑊) ∈ ℝ → ((♯‘𝑊) − 1) ∈ ℝ)
108, 9syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘𝑊) ∈ ℕ0 → ((♯‘𝑊) − 1) ∈ ℝ)
1110adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → ((♯‘𝑊) − 1) ∈ ℝ)
128adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → (♯‘𝑊) ∈ ℝ)
137, 11, 123jca 1123 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → (𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ))
148ltm1d 11144 . . . . . . . . . . . . . . . . . . . . . . 23 ((♯‘𝑊) ∈ ℕ0 → ((♯‘𝑊) − 1) < (♯‘𝑊))
1514adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → ((♯‘𝑊) − 1) < (♯‘𝑊))
16 lttr 10302 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → ((𝑖 < ((♯‘𝑊) − 1) ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)) → 𝑖 < (♯‘𝑊)))
1716expcomd 453 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → (((♯‘𝑊) − 1) < (♯‘𝑊) → (𝑖 < ((♯‘𝑊) − 1) → 𝑖 < (♯‘𝑊))))
1813, 15, 17sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → (𝑖 < ((♯‘𝑊) − 1) → 𝑖 < (♯‘𝑊)))
1918impancom 455 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℕ0𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0𝑖 < (♯‘𝑊)))
20193adant2 1126 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ ℕ0 ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0𝑖 < (♯‘𝑊)))
215, 20sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0𝑖 < (♯‘𝑊)))
224, 21syl5com 31 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ Word 𝑉 → (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 < (♯‘𝑊)))
2322adantr 472 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) → (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 < (♯‘𝑊)))
2423imp 444 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 < (♯‘𝑊))
25 simplr 809 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑋𝑉𝑌𝑉))
26 ccat2s1fvw 13610 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (♯‘𝑊)) ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (𝑊𝑖))
271, 3, 24, 25, 26syl31anc 1480 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (𝑊𝑖))
2827eqcomd 2762 . . . . . . . . . . . . 13 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖))
29 simpl 474 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉)
30 peano2nn0 11521 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
31303ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ ℕ0 ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → (𝑖 + 1) ∈ ℕ0)
325, 31sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → (𝑖 + 1) ∈ ℕ0)
3332adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ ℕ0)
34 1red 10243 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → 1 ∈ ℝ)
357, 34, 12ltaddsubd 10815 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → ((𝑖 + 1) < (♯‘𝑊) ↔ 𝑖 < ((♯‘𝑊) − 1)))
3635biimprd 238 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → (𝑖 < ((♯‘𝑊) − 1) → (𝑖 + 1) < (♯‘𝑊)))
3736impancom 455 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℕ0𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0 → (𝑖 + 1) < (♯‘𝑊)))
38373adant2 1126 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ ℕ0 ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0 → (𝑖 + 1) < (♯‘𝑊)))
395, 38sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0 → (𝑖 + 1) < (♯‘𝑊)))
404, 39mpan9 487 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) < (♯‘𝑊))
4129, 33, 403jca 1123 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Word 𝑉𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (♯‘𝑊)))
4241adantlr 753 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (♯‘𝑊)))
43 ccat2s1fvw 13610 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (♯‘𝑊)) ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
4442, 25, 43syl2anc 696 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
4544eqcomd 2762 . . . . . . . . . . . . 13 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)))
4628, 45preq12d 4416 . . . . . . . . . . . 12 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → {(𝑊𝑖), (𝑊‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))})
4746eleq1d 2820 . . . . . . . . . . 11 (((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
4847ralbidva 3119 . . . . . . . . . 10 ((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
4948biimpd 219 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5049impancom 455 . . . . . . . 8 ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑋𝑉𝑌𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
51503adant3 1127 . . . . . . 7 ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋𝑉𝑌𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
52513ad2ant1 1128 . . . . . 6 (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋𝑉𝑌𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5352com12 32 . . . . 5 ((𝑋𝑉𝑌𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5453a1dd 50 . . . 4 ((𝑋𝑉𝑌𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
55543adant3 1127 . . 3 ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
5655imp31 447 . 2 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
57 ax-1 6 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → (𝑋𝑉𝑌𝑉)))
58573adant3 1127 . . . . . . . . . 10 ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → (𝑋𝑉𝑌𝑉)))
59 simpl 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → 𝑊 ∈ Word 𝑉)
60 oveq1 6816 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝑊) = (𝑁 − 2) → ((♯‘𝑊) − 1) = ((𝑁 − 2) − 1))
6160adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((♯‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((♯‘𝑊) − 1) = ((𝑁 − 2) − 1))
62 eluzelcn 11887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℂ)
63 2cnd 11281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℂ)
64 1cnd 10244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → 1 ∈ ℂ)
6562, 63, 64subsub4d 10611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
66 2p1e3 11339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 + 1) = 3
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → (2 + 1) = 3)
6867oveq2d 6825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
69 uznn0sub 11908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ∈ ℕ0)
7068, 69eqeltrd 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) ∈ ℕ0)
7165, 70eqeltrd 2835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) ∈ ℕ0)
7271adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((♯‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑁 − 2) − 1) ∈ ℕ0)
7361, 72eqeltrd 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (((♯‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((♯‘𝑊) − 1) ∈ ℕ0)
7473ancoms 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → ((♯‘𝑊) − 1) ∈ ℕ0)
7574adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → ((♯‘𝑊) − 1) ∈ ℕ0)
764, 8syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℝ)
7776adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (♯‘𝑊) ∈ ℝ)
7877ltm1d 11144 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → ((♯‘𝑊) − 1) < (♯‘𝑊))
7959, 75, 783jca 1123 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))
8079ex 449 . . . . . . . . . . . . . . . . . . 19 (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))))
8180adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))))
82813ad2ant1 1128 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → ((𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))))
8382imp 444 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))
84 simpl2 1230 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (𝑋𝑉𝑌𝑉))
85 ccat2s1fvw 13610 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)) ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
8683, 84, 85syl2anc 696 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
87 nn0cn 11490 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝑊) ∈ ℕ0 → (♯‘𝑊) ∈ ℂ)
88 ax-1cn 10182 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
89 npcan 10478 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑊) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
9087, 88, 89sylancl 697 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝑊) ∈ ℕ0 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
914, 90syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ Word 𝑉 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
9291adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
93923ad2ant1 1128 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
9493fveq2d 6352 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)))
95 eqid 2756 . . . . . . . . . . . . . . . . . . . . 21 (♯‘𝑊) = (♯‘𝑊)
96952a1i 12 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ Word 𝑉 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → (♯‘𝑊) = (♯‘𝑊)))
9796imdistani 728 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)))
98973ad2ant1 1128 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)))
99 simp2l 1242 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → 𝑋𝑉)
100 simp2r 1243 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → 𝑌𝑉)
101 ccatw2s1p1 13608 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
10298, 99, 100, 101syl12anc 1475 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
10394, 102eqtrd 2790 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)) = 𝑋)
104103adantr 472 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)) = 𝑋)
10586, 104preq12d 4416 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} = {(𝑊‘((♯‘𝑊) − 1)), 𝑋})
106 lsw 13534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
107106adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊‘0) = 𝑋𝑊 ∈ Word 𝑉) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
108 simpl 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊‘0) = 𝑋𝑊 ∈ Word 𝑉) → (𝑊‘0) = 𝑋)
109107, 108preq12d 4416 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊‘0) = 𝑋𝑊 ∈ Word 𝑉) → {(lastS‘𝑊), (𝑊‘0)} = {(𝑊‘((♯‘𝑊) − 1)), 𝑋})
110109eleq1d 2820 . . . . . . . . . . . . . . . . . . . 20 (((𝑊‘0) = 𝑋𝑊 ∈ Word 𝑉) → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 ↔ {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸))
111110biimpd 219 . . . . . . . . . . . . . . . . . . 19 (((𝑊‘0) = 𝑋𝑊 ∈ Word 𝑉) → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸))
112111expcom 450 . . . . . . . . . . . . . . . . . 18 (𝑊 ∈ Word 𝑉 → ((𝑊‘0) = 𝑋 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)))
113112com23 86 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ Word 𝑉 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)))
114113imp31 447 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)
1151143adant2 1126 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)
116115adantr 472 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)
117105, 116eqeltrd 2835 . . . . . . . . . . . . 13 ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋𝑉𝑌𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)
118117exp520 1451 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋𝑉𝑌𝑉) → ((𝑊‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
119118com14 96 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘3) → ((𝑋𝑉𝑌𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
1201193ad2ant3 1130 . . . . . . . . . 10 ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ((𝑋𝑉𝑌𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
12158, 120syld 47 . . . . . . . . 9 ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
122121com25 99 . . . . . . . 8 ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
123122com14 96 . . . . . . 7 ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
1241233adant2 1126 . . . . . 6 ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
1251243imp 1102 . . . . 5 (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))
126125impcom 445 . . . 4 (((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))
127126imp 444 . . 3 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)
12895, 101mpanl2 719 . . . . . . . . . . . . 13 ((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
129 ccatw2s1p2 13609 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1)) = 𝑌)
13095, 129mpanl2 719 . . . . . . . . . . . . 13 ((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1)) = 𝑌)
131128, 130preq12d 4416 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝑉 ∧ (𝑋𝑉𝑌𝑉)) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})
132131expcom 450 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))
133132a1i 11 . . . . . . . . . 10 ({𝑋, 𝑌} ∈ 𝐸 → ((𝑋𝑉𝑌𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
134133com13 88 . . . . . . . . 9 (𝑊 ∈ Word 𝑉 → ((𝑋𝑉𝑌𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
1351343ad2ant1 1128 . . . . . . . 8 ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋𝑉𝑌𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
1361353ad2ant1 1128 . . . . . . 7 (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋𝑉𝑌𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
137136com12 32 . . . . . 6 ((𝑋𝑉𝑌𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
1381373adant3 1127 . . . . 5 ((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
139138imp31 447 . . . 4 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})
140 simpr 479 . . . 4 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {𝑋, 𝑌} ∈ 𝐸)
141139, 140eqeltrd 2835 . . 3 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)
142 ovex 6837 . . . 4 ((♯‘𝑊) − 1) ∈ V
143 fvex 6358 . . . 4 (♯‘𝑊) ∈ V
144 fveq2 6348 . . . . . 6 (𝑖 = ((♯‘𝑊) − 1) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)))
145 oveq1 6816 . . . . . . 7 (𝑖 = ((♯‘𝑊) − 1) → (𝑖 + 1) = (((♯‘𝑊) − 1) + 1))
146145fveq2d 6352 . . . . . 6 (𝑖 = ((♯‘𝑊) − 1) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)))
147144, 146preq12d 4416 . . . . 5 (𝑖 = ((♯‘𝑊) − 1) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))})
148147eleq1d 2820 . . . 4 (𝑖 = ((♯‘𝑊) − 1) → ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))
149 fveq2 6348 . . . . . 6 (𝑖 = (♯‘𝑊) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)))
150 oveq1 6816 . . . . . . 7 (𝑖 = (♯‘𝑊) → (𝑖 + 1) = ((♯‘𝑊) + 1))
151150fveq2d 6352 . . . . . 6 (𝑖 = (♯‘𝑊) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1)))
152149, 151preq12d 4416 . . . . 5 (𝑖 = (♯‘𝑊) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))})
153152eleq1d 2820 . . . 4 (𝑖 = (♯‘𝑊) → ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸))
154142, 143, 148, 153ralpr 4378 . . 3 (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸))
155127, 141, 154sylanbrc 701 . 2 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
156 ralunb 3933 . 2 (∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
15756, 155, 156sylanbrc 701 1 ((((𝑋𝑉𝑌𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1628  wcel 2135  wral 3046  cun 3709  {cpr 4319   class class class wbr 4800  cfv 6045  (class class class)co 6809  cc 10122  cr 10123  0cc0 10124  1c1 10125   + caddc 10127   < clt 10262  cmin 10454  cn 11208  2c2 11258  3c3 11259  0cn0 11480  cuz 11875  ..^cfzo 12655  chash 13307  Word cword 13473  lastSclsw 13474   ++ cconcat 13475  ⟨“cs1 13476  Vtxcvtx 26069  Edgcedg 26134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-card 8951  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-nn 11209  df-2 11267  df-3 11268  df-n0 11481  df-z 11566  df-uz 11876  df-fz 12516  df-fzo 12656  df-hash 13308  df-word 13481  df-lsw 13482  df-concat 13483  df-s1 13484
This theorem is referenced by:  clwwlknonex2  27254
  Copyright terms: Public domain W3C validator