# Metamath Proof Explorer

## Theorem clwlkclwwlklem2a4

Description: Lemma 4 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Hypothesis clwlkclwwlklem2.f ${⊢}{F}=\left({x}\in \left(0..^\left|{P}\right|-1\right)⟼if\left({x}<\left|{P}\right|-2,{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left({x}+1\right)\right\}\right),{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left(0\right)\right\}\right)\right)\right)$
Assertion clwlkclwwlklem2a4 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(\left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\to \left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\to {E}\left({F}\left({I}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ${⊢}{F}=\left({x}\in \left(0..^\left|{P}\right|-1\right)⟼if\left({x}<\left|{P}\right|-2,{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left({x}+1\right)\right\}\right),{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left(0\right)\right\}\right)\right)\right)$
2 fveq2 ${⊢}{I}=\left|{P}\right|-2\to {F}\left({I}\right)={F}\left(\left|{P}\right|-2\right)$
3 lencl ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|\in {ℕ}_{0}$
4 1 clwlkclwwlklem2fv2 ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to {F}\left(\left|{P}\right|-2\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)$
5 3 4 sylan ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to {F}\left(\left|{P}\right|-2\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)$
6 2 5 sylan9eqr ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge {I}=\left|{P}\right|-2\right)\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)$
7 6 ex ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left({I}=\left|{P}\right|-2\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)\right)$
8 7 3adant1 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left({I}=\left|{P}\right|-2\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)\right)$
9 8 ad2antrr ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to \left({I}=\left|{P}\right|-2\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)\right)$
10 9 impcom ${⊢}\left({I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)$
11 10 fveq2d ${⊢}\left({I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {E}\left({F}\left({I}\right)\right)={E}\left({{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)\right)$
12 f1f1orn ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\to {E}:\mathrm{dom}{E}\underset{1-1 onto}{⟶}\mathrm{ran}{E}$
13 12 3ad2ant1 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to {E}:\mathrm{dom}{E}\underset{1-1 onto}{⟶}\mathrm{ran}{E}$
14 13 ad2antrr ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to {E}:\mathrm{dom}{E}\underset{1-1 onto}{⟶}\mathrm{ran}{E}$
15 lsw ${⊢}{P}\in \mathrm{Word}{V}\to \mathrm{lastS}\left({P}\right)={P}\left(\left|{P}\right|-1\right)$
16 15 eqeq1d ${⊢}{P}\in \mathrm{Word}{V}\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)↔{P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\right)$
17 nn0cn ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left|{P}\right|\in ℂ$
18 id ${⊢}\left|{P}\right|\in ℂ\to \left|{P}\right|\in ℂ$
19 2cnd ${⊢}\left|{P}\right|\in ℂ\to 2\in ℂ$
20 1cnd ${⊢}\left|{P}\right|\in ℂ\to 1\in ℂ$
21 18 19 20 subsubd ${⊢}\left|{P}\right|\in ℂ\to \left|{P}\right|-\left(2-1\right)=\left|{P}\right|-2+1$
22 2m1e1 ${⊢}2-1=1$
23 22 a1i ${⊢}\left|{P}\right|\in ℂ\to 2-1=1$
24 23 oveq2d ${⊢}\left|{P}\right|\in ℂ\to \left|{P}\right|-\left(2-1\right)=\left|{P}\right|-1$
25 21 24 eqtr3d ${⊢}\left|{P}\right|\in ℂ\to \left|{P}\right|-2+1=\left|{P}\right|-1$
26 3 17 25 3syl ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|-2+1=\left|{P}\right|-1$
27 26 adantr ${⊢}\left({P}\in \mathrm{Word}{V}\wedge {P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\right)\to \left|{P}\right|-2+1=\left|{P}\right|-1$
28 27 fveq2d ${⊢}\left({P}\in \mathrm{Word}{V}\wedge {P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(\left|{P}\right|-1\right)$
29 eqeq2 ${⊢}{P}\left(0\right)={P}\left(\left|{P}\right|-1\right)\to \left({P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)↔{P}\left(\left|{P}\right|-2+1\right)={P}\left(\left|{P}\right|-1\right)\right)$
30 29 eqcoms ${⊢}{P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\to \left({P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)↔{P}\left(\left|{P}\right|-2+1\right)={P}\left(\left|{P}\right|-1\right)\right)$
31 30 adantl ${⊢}\left({P}\in \mathrm{Word}{V}\wedge {P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\right)\to \left({P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)↔{P}\left(\left|{P}\right|-2+1\right)={P}\left(\left|{P}\right|-1\right)\right)$
32 28 31 mpbird ${⊢}\left({P}\in \mathrm{Word}{V}\wedge {P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)$
33 32 ex ${⊢}{P}\in \mathrm{Word}{V}\to \left({P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)\right)$
34 16 33 sylbid ${⊢}{P}\in \mathrm{Word}{V}\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)\right)$
35 34 3ad2ant2 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)\right)$
36 35 com12 ${⊢}\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to \left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)\right)$
37 36 adantr ${⊢}\left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\to \left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)\right)$
38 37 impcom ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)$
39 38 adantr ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to {P}\left(\left|{P}\right|-2+1\right)={P}\left(0\right)$
40 39 preq2d ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}$
41 fveq2 ${⊢}{I}=\left|{P}\right|-2\to {P}\left({I}\right)={P}\left(\left|{P}\right|-2\right)$
42 fvoveq1 ${⊢}{I}=\left|{P}\right|-2\to {P}\left({I}+1\right)={P}\left(\left|{P}\right|-2+1\right)$
43 41 42 preq12d ${⊢}{I}=\left|{P}\right|-2\to \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}$
44 43 eqeq1d ${⊢}{I}=\left|{P}\right|-2\to \left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}↔\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)$
45 44 adantl ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}↔\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)$
46 40 45 mpbird ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}$
47 46 eleq1d ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}↔\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)$
48 47 biimpd ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)$
49 48 impancom ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)$
50 49 impcom ${⊢}\left({I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}$
51 f1ocnvfv2 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1 onto}{⟶}\mathrm{ran}{E}\wedge \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\to {E}\left({{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)\right)=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}$
52 14 50 51 syl2an2 ${⊢}\left({I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {E}\left({{E}}^{-1}\left(\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}\right)\right)=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}$
53 eqcom ${⊢}{P}\left(\left|{P}\right|-1\right)={P}\left(0\right)↔{P}\left(0\right)={P}\left(\left|{P}\right|-1\right)$
54 53 biimpi ${⊢}{P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\to {P}\left(0\right)={P}\left(\left|{P}\right|-1\right)$
55 1e2m1 ${⊢}1=2-1$
56 55 a1i ${⊢}{P}\in \mathrm{Word}{V}\to 1=2-1$
57 56 oveq2d ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|-1=\left|{P}\right|-\left(2-1\right)$
58 3 17 syl ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|\in ℂ$
59 2cnd ${⊢}{P}\in \mathrm{Word}{V}\to 2\in ℂ$
60 1cnd ${⊢}{P}\in \mathrm{Word}{V}\to 1\in ℂ$
61 58 59 60 subsubd ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|-\left(2-1\right)=\left|{P}\right|-2+1$
62 57 61 eqtrd ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|-1=\left|{P}\right|-2+1$
63 62 fveq2d ${⊢}{P}\in \mathrm{Word}{V}\to {P}\left(\left|{P}\right|-1\right)={P}\left(\left|{P}\right|-2+1\right)$
64 54 63 sylan9eqr ${⊢}\left({P}\in \mathrm{Word}{V}\wedge {P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\right)\to {P}\left(0\right)={P}\left(\left|{P}\right|-2+1\right)$
65 64 ex ${⊢}{P}\in \mathrm{Word}{V}\to \left({P}\left(\left|{P}\right|-1\right)={P}\left(0\right)\to {P}\left(0\right)={P}\left(\left|{P}\right|-2+1\right)\right)$
66 16 65 sylbid ${⊢}{P}\in \mathrm{Word}{V}\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to {P}\left(0\right)={P}\left(\left|{P}\right|-2+1\right)\right)$
67 66 imp ${⊢}\left({P}\in \mathrm{Word}{V}\wedge \mathrm{lastS}\left({P}\right)={P}\left(0\right)\right)\to {P}\left(0\right)={P}\left(\left|{P}\right|-2+1\right)$
68 67 preq2d ${⊢}\left({P}\in \mathrm{Word}{V}\wedge \mathrm{lastS}\left({P}\right)={P}\left(0\right)\right)\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}$
69 68 adantr ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge \mathrm{lastS}\left({P}\right)={P}\left(0\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}$
70 43 adantl ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge \mathrm{lastS}\left({P}\right)={P}\left(0\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}=\left\{{P}\left(\left|{P}\right|-2\right),{P}\left(\left|{P}\right|-2+1\right)\right\}$
71 69 70 eqtr4d ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge \mathrm{lastS}\left({P}\right)={P}\left(0\right)\right)\wedge {I}=\left|{P}\right|-2\right)\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
72 71 exp31 ${⊢}{P}\in \mathrm{Word}{V}\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$
73 72 3ad2ant2 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$
74 73 com12 ${⊢}\mathrm{lastS}\left({P}\right)={P}\left(0\right)\to \left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$
75 74 adantr ${⊢}\left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\to \left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$
76 75 impcom ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)$
77 76 adantr ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to \left({I}=\left|{P}\right|-2\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)$
78 77 impcom ${⊢}\left({I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to \left\{{P}\left(\left|{P}\right|-2\right),{P}\left(0\right)\right\}=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
79 11 52 78 3eqtrd ${⊢}\left({I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {E}\left({F}\left({I}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
80 simpll ${⊢}\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to \left|{P}\right|\in {ℕ}_{0}$
81 oveq1 ${⊢}\left|{P}\right|=2\to \left|{P}\right|-1=2-1$
82 81 22 syl6eq ${⊢}\left|{P}\right|=2\to \left|{P}\right|-1=1$
83 82 oveq2d ${⊢}\left|{P}\right|=2\to \left(0..^\left|{P}\right|-1\right)=\left(0..^1\right)$
84 83 eleq2d ${⊢}\left|{P}\right|=2\to \left({I}\in \left(0..^\left|{P}\right|-1\right)↔{I}\in \left(0..^1\right)\right)$
85 oveq1 ${⊢}\left|{P}\right|=2\to \left|{P}\right|-2=2-2$
86 2cn ${⊢}2\in ℂ$
87 86 subidi ${⊢}2-2=0$
88 85 87 syl6eq ${⊢}\left|{P}\right|=2\to \left|{P}\right|-2=0$
89 88 eqeq2d ${⊢}\left|{P}\right|=2\to \left({I}=\left|{P}\right|-2↔{I}=0\right)$
90 89 notbid ${⊢}\left|{P}\right|=2\to \left(¬{I}=\left|{P}\right|-2↔¬{I}=0\right)$
91 84 90 anbi12d ${⊢}\left|{P}\right|=2\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)↔\left({I}\in \left(0..^1\right)\wedge ¬{I}=0\right)\right)$
92 elsni ${⊢}{I}\in \left\{0\right\}\to {I}=0$
93 92 pm2.24d ${⊢}{I}\in \left\{0\right\}\to \left(¬{I}=0\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
94 fzo01 ${⊢}\left(0..^1\right)=\left\{0\right\}$
95 93 94 eleq2s ${⊢}{I}\in \left(0..^1\right)\to \left(¬{I}=0\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
96 95 imp ${⊢}\left({I}\in \left(0..^1\right)\wedge ¬{I}=0\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)$
97 91 96 syl6bi ${⊢}\left|{P}\right|=2\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
98 97 adantld ${⊢}\left|{P}\right|=2\to \left(\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
99 df-ne ${⊢}\left|{P}\right|\ne 2↔¬\left|{P}\right|=2$
100 2re ${⊢}2\in ℝ$
101 100 a1i ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to 2\in ℝ$
102 nn0re ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left|{P}\right|\in ℝ$
103 102 adantr ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to \left|{P}\right|\in ℝ$
104 simpr ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to 2\le \left|{P}\right|$
105 101 103 104 leltned ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to \left(2<\left|{P}\right|↔\left|{P}\right|\ne 2\right)$
106 elfzo0 ${⊢}{I}\in \left(0..^\left|{P}\right|-1\right)↔\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-1\in ℕ\wedge {I}<\left|{P}\right|-1\right)$
107 simp-4l ${⊢}\left(\left(\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\wedge 2<\left|{P}\right|\right)\wedge {I}<\left|{P}\right|-1\right)\to {I}\in {ℕ}_{0}$
108 nn0z ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left|{P}\right|\in ℤ$
109 2z ${⊢}2\in ℤ$
110 109 a1i ${⊢}\left|{P}\right|\in {ℕ}_{0}\to 2\in ℤ$
111 108 110 zsubcld ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left|{P}\right|-2\in ℤ$
112 111 adantr ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2<\left|{P}\right|\right)\to \left|{P}\right|-2\in ℤ$
113 100 a1i ${⊢}\left|{P}\right|\in {ℕ}_{0}\to 2\in ℝ$
114 113 102 posdifd ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left(2<\left|{P}\right|↔0<\left|{P}\right|-2\right)$
115 114 biimpa ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2<\left|{P}\right|\right)\to 0<\left|{P}\right|-2$
116 elnnz ${⊢}\left|{P}\right|-2\in ℕ↔\left(\left|{P}\right|-2\in ℤ\wedge 0<\left|{P}\right|-2\right)$
117 112 115 116 sylanbrc ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2<\left|{P}\right|\right)\to \left|{P}\right|-2\in ℕ$
118 117 ad5ant24 ${⊢}\left(\left(\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\wedge 2<\left|{P}\right|\right)\wedge {I}<\left|{P}\right|-1\right)\to \left|{P}\right|-2\in ℕ$
119 nn0z ${⊢}{I}\in {ℕ}_{0}\to {I}\in ℤ$
120 peano2zm ${⊢}\left|{P}\right|\in ℤ\to \left|{P}\right|-1\in ℤ$
121 108 120 syl ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left|{P}\right|-1\in ℤ$
122 zltlem1 ${⊢}\left({I}\in ℤ\wedge \left|{P}\right|-1\in ℤ\right)\to \left({I}<\left|{P}\right|-1↔{I}\le \left|{P}\right|-1-1\right)$
123 119 121 122 syl2an ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left({I}<\left|{P}\right|-1↔{I}\le \left|{P}\right|-1-1\right)$
124 17 adantl ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left|{P}\right|\in ℂ$
125 1cnd ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to 1\in ℂ$
126 124 125 125 subsub4d ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left|{P}\right|-1-1=\left|{P}\right|-\left(1+1\right)$
127 1p1e2 ${⊢}1+1=2$
128 127 a1i ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to 1+1=2$
129 128 oveq2d ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left|{P}\right|-\left(1+1\right)=\left|{P}\right|-2$
130 126 129 eqtrd ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left|{P}\right|-1-1=\left|{P}\right|-2$
131 130 breq2d ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left({I}\le \left|{P}\right|-1-1↔{I}\le \left|{P}\right|-2\right)$
132 123 131 bitrd ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left({I}<\left|{P}\right|-1↔{I}\le \left|{P}\right|-2\right)$
133 necom ${⊢}\left|{P}\right|-2\ne {I}↔{I}\ne \left|{P}\right|-2$
134 df-ne ${⊢}{I}\ne \left|{P}\right|-2↔¬{I}=\left|{P}\right|-2$
135 133 134 bitr2i ${⊢}¬{I}=\left|{P}\right|-2↔\left|{P}\right|-2\ne {I}$
136 nn0re ${⊢}{I}\in {ℕ}_{0}\to {I}\in ℝ$
137 136 ad2antrr ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge {I}\le \left|{P}\right|-2\right)\to {I}\in ℝ$
138 102 113 resubcld ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left|{P}\right|-2\in ℝ$
139 138 ad2antlr ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge {I}\le \left|{P}\right|-2\right)\to \left|{P}\right|-2\in ℝ$
140 simpr ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge {I}\le \left|{P}\right|-2\right)\to {I}\le \left|{P}\right|-2$
141 leltne ${⊢}\left({I}\in ℝ\wedge \left|{P}\right|-2\in ℝ\wedge {I}\le \left|{P}\right|-2\right)\to \left({I}<\left|{P}\right|-2↔\left|{P}\right|-2\ne {I}\right)$
142 141 bicomd ${⊢}\left({I}\in ℝ\wedge \left|{P}\right|-2\in ℝ\wedge {I}\le \left|{P}\right|-2\right)\to \left(\left|{P}\right|-2\ne {I}↔{I}<\left|{P}\right|-2\right)$
143 137 139 140 142 syl3anc ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge {I}\le \left|{P}\right|-2\right)\to \left(\left|{P}\right|-2\ne {I}↔{I}<\left|{P}\right|-2\right)$
144 143 biimpd ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge {I}\le \left|{P}\right|-2\right)\to \left(\left|{P}\right|-2\ne {I}\to {I}<\left|{P}\right|-2\right)$
145 135 144 syl5bi ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge {I}\le \left|{P}\right|-2\right)\to \left(¬{I}=\left|{P}\right|-2\to {I}<\left|{P}\right|-2\right)$
146 145 ex ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left({I}\le \left|{P}\right|-2\to \left(¬{I}=\left|{P}\right|-2\to {I}<\left|{P}\right|-2\right)\right)$
147 132 146 sylbid ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left({I}<\left|{P}\right|-1\to \left(¬{I}=\left|{P}\right|-2\to {I}<\left|{P}\right|-2\right)\right)$
148 147 com23 ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\to \left(¬{I}=\left|{P}\right|-2\to \left({I}<\left|{P}\right|-1\to {I}<\left|{P}\right|-2\right)\right)$
149 148 imp ${⊢}\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left({I}<\left|{P}\right|-1\to {I}<\left|{P}\right|-2\right)$
150 149 adantr ${⊢}\left(\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\wedge 2<\left|{P}\right|\right)\to \left({I}<\left|{P}\right|-1\to {I}<\left|{P}\right|-2\right)$
151 150 imp ${⊢}\left(\left(\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\wedge 2<\left|{P}\right|\right)\wedge {I}<\left|{P}\right|-1\right)\to {I}<\left|{P}\right|-2$
152 107 118 151 3jca ${⊢}\left(\left(\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\wedge 2<\left|{P}\right|\right)\wedge {I}<\left|{P}\right|-1\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)$
153 152 ex ${⊢}\left(\left(\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|\in {ℕ}_{0}\right)\wedge ¬{I}=\left|{P}\right|-2\right)\wedge 2<\left|{P}\right|\right)\to \left({I}<\left|{P}\right|-1\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
154 153 exp41 ${⊢}{I}\in {ℕ}_{0}\to \left(\left|{P}\right|\in {ℕ}_{0}\to \left(¬{I}=\left|{P}\right|-2\to \left(2<\left|{P}\right|\to \left({I}<\left|{P}\right|-1\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)\right)\right)$
155 154 com25 ${⊢}{I}\in {ℕ}_{0}\to \left({I}<\left|{P}\right|-1\to \left(¬{I}=\left|{P}\right|-2\to \left(2<\left|{P}\right|\to \left(\left|{P}\right|\in {ℕ}_{0}\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)\right)\right)$
156 155 imp ${⊢}\left({I}\in {ℕ}_{0}\wedge {I}<\left|{P}\right|-1\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(2<\left|{P}\right|\to \left(\left|{P}\right|\in {ℕ}_{0}\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)\right)$
157 156 3adant2 ${⊢}\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-1\in ℕ\wedge {I}<\left|{P}\right|-1\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(2<\left|{P}\right|\to \left(\left|{P}\right|\in {ℕ}_{0}\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)\right)$
158 106 157 sylbi ${⊢}{I}\in \left(0..^\left|{P}\right|-1\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(2<\left|{P}\right|\to \left(\left|{P}\right|\in {ℕ}_{0}\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)\right)$
159 158 imp ${⊢}\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left(2<\left|{P}\right|\to \left(\left|{P}\right|\in {ℕ}_{0}\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)$
160 159 com13 ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left(2<\left|{P}\right|\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)$
161 160 adantr ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to \left(2<\left|{P}\right|\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)$
162 105 161 sylbird ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to \left(\left|{P}\right|\ne 2\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)$
163 99 162 syl5bir ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to \left(¬\left|{P}\right|=2\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)$
164 163 com23 ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left(¬\left|{P}\right|=2\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)\right)$
165 164 imp ${⊢}\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to \left(¬\left|{P}\right|=2\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
166 165 com12 ${⊢}¬\left|{P}\right|=2\to \left(\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)\right)$
167 98 166 pm2.61i ${⊢}\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to \left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)$
168 elfzo0 ${⊢}{I}\in \left(0..^\left|{P}\right|-2\right)↔\left({I}\in {ℕ}_{0}\wedge \left|{P}\right|-2\in ℕ\wedge {I}<\left|{P}\right|-2\right)$
169 167 168 sylibr ${⊢}\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to {I}\in \left(0..^\left|{P}\right|-2\right)$
170 80 169 jca ${⊢}\left(\left(\left|{P}\right|\in {ℕ}_{0}\wedge 2\le \left|{P}\right|\right)\wedge \left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\right)\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)$
171 170 exp31 ${⊢}\left|{P}\right|\in {ℕ}_{0}\to \left(2\le \left|{P}\right|\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)\right)$
172 3 171 syl ${⊢}{P}\in \mathrm{Word}{V}\to \left(2\le \left|{P}\right|\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)\right)$
173 172 imp ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)$
174 173 3adant1 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(\left({I}\in \left(0..^\left|{P}\right|-1\right)\wedge ¬{I}=\left|{P}\right|-2\right)\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)$
175 174 expd ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left({I}\in \left(0..^\left|{P}\right|-1\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)\right)$
176 175 com12 ${⊢}{I}\in \left(0..^\left|{P}\right|-1\right)\to \left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)\right)$
177 176 adantl ${⊢}\left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\to \left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)\right)$
178 177 impcom ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)$
179 178 adantr ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to \left(¬{I}=\left|{P}\right|-2\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\right)$
180 179 impcom ${⊢}\left(¬{I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to \left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)$
181 1 clwlkclwwlklem2fv1 ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge {I}\in \left(0..^\left|{P}\right|-2\right)\right)\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)$
182 180 181 syl ${⊢}\left(¬{I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {F}\left({I}\right)={{E}}^{-1}\left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)$
183 182 fveq2d ${⊢}\left(¬{I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {E}\left({F}\left({I}\right)\right)={E}\left({{E}}^{-1}\left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$
184 simprr ${⊢}\left(¬{I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}$
185 f1ocnvfv2 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1 onto}{⟶}\mathrm{ran}{E}\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to {E}\left({{E}}^{-1}\left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
186 14 184 185 syl2an2 ${⊢}\left(¬{I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {E}\left({{E}}^{-1}\left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
187 183 186 eqtrd ${⊢}\left(¬{I}=\left|{P}\right|-2\wedge \left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\right)\to {E}\left({F}\left({I}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
188 79 187 pm2.61ian ${⊢}\left(\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\right)\wedge \left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\right)\to {E}\left({F}\left({I}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}$
189 188 exp31 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {P}\in \mathrm{Word}{V}\wedge 2\le \left|{P}\right|\right)\to \left(\left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge {I}\in \left(0..^\left|{P}\right|-1\right)\right)\to \left(\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\in \mathrm{ran}{E}\to {E}\left({F}\left({I}\right)\right)=\left\{{P}\left({I}\right),{P}\left({I}+1\right)\right\}\right)\right)$