Metamath Proof Explorer

Theorem clwlkclwwlklem2a

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

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢F=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
Assertion clwlkclwwlklem2a ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1∧P⁡0=P⁡F

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢F=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
2 simpl ⊢x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→x<P−2
3 f1f1orn ⊢E:dom⁡E⟶1-1R→E:dom⁡E⟶1-1 ontoran⁡E
4 3 3ad2ant1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→E:dom⁡E⟶1-1 ontoran⁡E
5 4 adantr ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→E:dom⁡E⟶1-1 ontoran⁡E
6 5 ad2antrl ⊢x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→E:dom⁡E⟶1-1 ontoran⁡E
7 elfzo0 ⊢x∈0..^P−1↔x∈ℕ0∧P−1∈ℕ∧x<P−1
8 lencl ⊢P∈WordV→P∈ℕ0
9 simpl ⊢x∈ℕ0∧P∈ℕ0→x∈ℕ0
10 9 adantr ⊢x∈ℕ0∧P∈ℕ0∧x<P−2∧2≤P→x∈ℕ0
11 elnn0z ⊢x∈ℕ0↔x∈ℤ∧0≤x
12 0red ⊢x∈ℤ∧P∈ℕ0→0∈ℝ
13 zre ⊢x∈ℤ→x∈ℝ
14 13 adantr ⊢x∈ℤ∧P∈ℕ0→x∈ℝ
15 nn0re ⊢P∈ℕ0→P∈ℝ
16 2re ⊢2∈ℝ
17 16 a1i ⊢P∈ℕ0→2∈ℝ
18 15 17 resubcld ⊢P∈ℕ0→P−2∈ℝ
19 18 adantl ⊢x∈ℤ∧P∈ℕ0→P−2∈ℝ
20 lelttr ⊢0∈ℝ∧x∈ℝ∧P−2∈ℝ→0≤x∧x<P−2→0<P−2
21 12 14 19 20 syl3anc ⊢x∈ℤ∧P∈ℕ0→0≤x∧x<P−2→0<P−2
22 nn0z ⊢P∈ℕ0→P∈ℤ
23 2z ⊢2∈ℤ
24 23 a1i ⊢P∈ℕ0→2∈ℤ
25 22 24 zsubcld ⊢P∈ℕ0→P−2∈ℤ
26 25 anim1i ⊢P∈ℕ0∧0<P−2→P−2∈ℤ∧0<P−2
27 elnnz ⊢P−2∈ℕ↔P−2∈ℤ∧0<P−2
28 26 27 sylibr ⊢P∈ℕ0∧0<P−2→P−2∈ℕ
29 nn0cn ⊢P∈ℕ0→P∈ℂ
30 peano2cnm ⊢P∈ℂ→P−1∈ℂ
31 29 30 syl ⊢P∈ℕ0→P−1∈ℂ
32 31 subid1d ⊢P∈ℕ0→P-1-0=P−1
33 32 oveq1d ⊢P∈ℕ0→P−1-0-1=P-1-1
34 1cnd ⊢P∈ℕ0→1∈ℂ
35 29 34 34 subsub4d ⊢P∈ℕ0→P-1-1=P−1+1
36 1p1e2 ⊢1+1=2
37 36 a1i ⊢P∈ℕ0→1+1=2
38 37 oveq2d ⊢P∈ℕ0→P−1+1=P−2
39 35 38 eqtrd ⊢P∈ℕ0→P-1-1=P−2
40 33 39 eqtrd ⊢P∈ℕ0→P−1-0-1=P−2
41 40 eleq1d ⊢P∈ℕ0→P−1-0-1∈ℕ↔P−2∈ℕ
42 41 adantr ⊢P∈ℕ0∧0<P−2→P−1-0-1∈ℕ↔P−2∈ℕ
43 28 42 mpbird ⊢P∈ℕ0∧0<P−2→P−1-0-1∈ℕ
44 43 ex ⊢P∈ℕ0→0<P−2→P−1-0-1∈ℕ
45 44 adantl ⊢x∈ℤ∧P∈ℕ0→0<P−2→P−1-0-1∈ℕ
46 21 45 syld ⊢x∈ℤ∧P∈ℕ0→0≤x∧x<P−2→P−1-0-1∈ℕ
47 46 exp4b ⊢x∈ℤ→P∈ℕ0→0≤x→x<P−2→P−1-0-1∈ℕ
48 47 com23 ⊢x∈ℤ→0≤x→P∈ℕ0→x<P−2→P−1-0-1∈ℕ
49 48 imp ⊢x∈ℤ∧0≤x→P∈ℕ0→x<P−2→P−1-0-1∈ℕ
50 11 49 sylbi ⊢x∈ℕ0→P∈ℕ0→x<P−2→P−1-0-1∈ℕ
51 50 imp ⊢x∈ℕ0∧P∈ℕ0→x<P−2→P−1-0-1∈ℕ
52 51 com12 ⊢x<P−2→x∈ℕ0∧P∈ℕ0→P−1-0-1∈ℕ
53 52 adantr ⊢x<P−2∧2≤P→x∈ℕ0∧P∈ℕ0→P−1-0-1∈ℕ
54 53 impcom ⊢x∈ℕ0∧P∈ℕ0∧x<P−2∧2≤P→P−1-0-1∈ℕ
55 df-2 ⊢2=1+1
56 55 a1i ⊢P∈ℕ0→2=1+1
57 56 oveq2d ⊢P∈ℕ0→P−2=P−1+1
58 32 eqcomd ⊢P∈ℕ0→P−1=P-1-0
59 58 oveq1d ⊢P∈ℕ0→P-1-1=P−1-0-1
60 57 35 59 3eqtr2d ⊢P∈ℕ0→P−2=P−1-0-1
61 60 adantl ⊢x∈ℕ0∧P∈ℕ0→P−2=P−1-0-1
62 61 breq2d ⊢x∈ℕ0∧P∈ℕ0→x<P−2↔x<P−1-0-1
63 62 biimpcd ⊢x<P−2→x∈ℕ0∧P∈ℕ0→x<P−1-0-1
64 63 adantr ⊢x<P−2∧2≤P→x∈ℕ0∧P∈ℕ0→x<P−1-0-1
65 64 impcom ⊢x∈ℕ0∧P∈ℕ0∧x<P−2∧2≤P→x<P−1-0-1
66 elfzo0 ⊢x∈0..^P−1-0-1↔x∈ℕ0∧P−1-0-1∈ℕ∧x<P−1-0-1
67 10 54 65 66 syl3anbrc ⊢x∈ℕ0∧P∈ℕ0∧x<P−2∧2≤P→x∈0..^P−1-0-1
68 67 exp32 ⊢x∈ℕ0∧P∈ℕ0→x<P−2→2≤P→x∈0..^P−1-0-1
69 68 a1d ⊢x∈ℕ0∧P∈ℕ0→x<P−1→x<P−2→2≤P→x∈0..^P−1-0-1
70 69 com24 ⊢x∈ℕ0∧P∈ℕ0→2≤P→x<P−2→x<P−1→x∈0..^P−1-0-1
71 70 ex ⊢x∈ℕ0→P∈ℕ0→2≤P→x<P−2→x<P−1→x∈0..^P−1-0-1
72 71 com25 ⊢x∈ℕ0→x<P−1→2≤P→x<P−2→P∈ℕ0→x∈0..^P−1-0-1
73 72 imp ⊢x∈ℕ0∧x<P−1→2≤P→x<P−2→P∈ℕ0→x∈0..^P−1-0-1
74 73 3adant2 ⊢x∈ℕ0∧P−1∈ℕ∧x<P−1→2≤P→x<P−2→P∈ℕ0→x∈0..^P−1-0-1
75 74 com14 ⊢P∈ℕ0→2≤P→x<P−2→x∈ℕ0∧P−1∈ℕ∧x<P−1→x∈0..^P−1-0-1
76 8 75 syl ⊢P∈WordV→2≤P→x<P−2→x∈ℕ0∧P−1∈ℕ∧x<P−1→x∈0..^P−1-0-1
77 76 imp ⊢P∈WordV∧2≤P→x<P−2→x∈ℕ0∧P−1∈ℕ∧x<P−1→x∈0..^P−1-0-1
78 77 3adant1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x<P−2→x∈ℕ0∧P−1∈ℕ∧x<P−1→x∈0..^P−1-0-1
79 7 78 syl7bi ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x<P−2→x∈0..^P−1→x∈0..^P−1-0-1
80 79 com13 ⊢x∈0..^P−1→x<P−2→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1-0-1
81 80 imp31 ⊢x∈0..^P−1∧x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1-0-1
82 fveq2 ⊢i=x→P⁡i=P⁡x
83 fvoveq1 ⊢i=x→P⁡i+1=P⁡x+1
84 82 83 preq12d ⊢i=x→P⁡iP⁡i+1=P⁡xP⁡x+1
85 84 eleq1d ⊢i=x→P⁡iP⁡i+1∈ran⁡E↔P⁡xP⁡x+1∈ran⁡E
86 85 adantl ⊢x∈0..^P−1∧x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧i=x→P⁡iP⁡i+1∈ran⁡E↔P⁡xP⁡x+1∈ran⁡E
87 81 86 rspcdv ⊢x∈0..^P−1∧x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E→P⁡xP⁡x+1∈ran⁡E
88 87 ex ⊢x∈0..^P−1∧x<P−2→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E→P⁡xP⁡x+1∈ran⁡E
89 88 com13 ⊢∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1∧x<P−2→P⁡xP⁡x+1∈ran⁡E
90 89 ad2antrl ⊢lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1∧x<P−2→P⁡xP⁡x+1∈ran⁡E
91 90 impcom ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→x∈0..^P−1∧x<P−2→P⁡xP⁡x+1∈ran⁡E
92 91 expdimp ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→x<P−2→P⁡xP⁡x+1∈ran⁡E
93 92 impcom ⊢x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→P⁡xP⁡x+1∈ran⁡E
94 f1ocnvdm ⊢E:dom⁡E⟶1-1 ontoran⁡E∧P⁡xP⁡x+1∈ran⁡E→E-1⁡P⁡xP⁡x+1∈dom⁡E
95 6 93 94 syl2anc ⊢x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→E-1⁡P⁡xP⁡x+1∈dom⁡E
96 2 95 jca ⊢x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→x<P−2∧E-1⁡P⁡xP⁡x+1∈dom⁡E
97 96 orcd ⊢x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→x<P−2∧E-1⁡P⁡xP⁡x+1∈dom⁡E∨¬x<P−2∧E-1⁡P⁡xP⁡0∈dom⁡E
98 simpl ⊢¬x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→¬x<P−2
99 5 ad2antrl ⊢¬x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→E:dom⁡E⟶1-1 ontoran⁡E
100 nn0z ⊢x∈ℕ0→x∈ℤ
101 peano2zm ⊢P∈ℤ→P−1∈ℤ
102 22 101 syl ⊢P∈ℕ0→P−1∈ℤ
103 100 102 anim12i ⊢x∈ℕ0∧P∈ℕ0→x∈ℤ∧P−1∈ℤ
104 zltlem1 ⊢x∈ℤ∧P−1∈ℤ→x<P−1↔x≤P-1-1
105 103 104 syl ⊢x∈ℕ0∧P∈ℕ0→x<P−1↔x≤P-1-1
106 39 adantl ⊢x∈ℕ0∧P∈ℕ0→P-1-1=P−2
107 106 breq2d ⊢x∈ℕ0∧P∈ℕ0→x≤P-1-1↔x≤P−2
108 107 biimpd ⊢x∈ℕ0∧P∈ℕ0→x≤P-1-1→x≤P−2
109 105 108 sylbid ⊢x∈ℕ0∧P∈ℕ0→x<P−1→x≤P−2
110 109 impancom ⊢x∈ℕ0∧x<P−1→P∈ℕ0→x≤P−2
111 110 imp ⊢x∈ℕ0∧x<P−1∧P∈ℕ0→x≤P−2
112 nn0re ⊢x∈ℕ0→x∈ℝ
113 112 adantr ⊢x∈ℕ0∧x<P−1→x∈ℝ
114 113 18 anim12i ⊢x∈ℕ0∧x<P−1∧P∈ℕ0→x∈ℝ∧P−2∈ℝ
115 lenlt ⊢x∈ℝ∧P−2∈ℝ→x≤P−2↔¬P−2<x
116 114 115 syl ⊢x∈ℕ0∧x<P−1∧P∈ℕ0→x≤P−2↔¬P−2<x
117 111 116 mpbid ⊢x∈ℕ0∧x<P−1∧P∈ℕ0→¬P−2<x
118 117 anim1i ⊢x∈ℕ0∧x<P−1∧P∈ℕ0∧¬x<P−2→¬P−2<x∧¬x<P−2
119 114 ancomd ⊢x∈ℕ0∧x<P−1∧P∈ℕ0→P−2∈ℝ∧x∈ℝ
120 119 adantr ⊢x∈ℕ0∧x<P−1∧P∈ℕ0∧¬x<P−2→P−2∈ℝ∧x∈ℝ
121 lttri3 ⊢P−2∈ℝ∧x∈ℝ→P−2=x↔¬P−2<x∧¬x<P−2
122 120 121 syl ⊢x∈ℕ0∧x<P−1∧P∈ℕ0∧¬x<P−2→P−2=x↔¬P−2<x∧¬x<P−2
123 118 122 mpbird ⊢x∈ℕ0∧x<P−1∧P∈ℕ0∧¬x<P−2→P−2=x
124 123 exp31 ⊢x∈ℕ0∧x<P−1→P∈ℕ0→¬x<P−2→P−2=x
125 124 com23 ⊢x∈ℕ0∧x<P−1→¬x<P−2→P∈ℕ0→P−2=x
126 125 3adant2 ⊢x∈ℕ0∧P−1∈ℕ∧x<P−1→¬x<P−2→P∈ℕ0→P−2=x
127 7 126 sylbi ⊢x∈0..^P−1→¬x<P−2→P∈ℕ0→P−2=x
128 127 impcom ⊢¬x<P−2∧x∈0..^P−1→P∈ℕ0→P−2=x
129 8 128 syl5com ⊢P∈WordV→¬x<P−2∧x∈0..^P−1→P−2=x
130 129 3ad2ant2 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→¬x<P−2∧x∈0..^P−1→P−2=x
131 130 imp ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧¬x<P−2∧x∈0..^P−1→P−2=x
132 131 fveq2d ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧¬x<P−2∧x∈0..^P−1→P⁡P−2=P⁡x
133 132 preq1d ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧¬x<P−2∧x∈0..^P−1→P⁡P−2P⁡0=P⁡xP⁡0
134 133 eleq1d ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧¬x<P−2∧x∈0..^P−1→P⁡P−2P⁡0∈ran⁡E↔P⁡xP⁡0∈ran⁡E
135 134 biimpd ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧¬x<P−2∧x∈0..^P−1→P⁡P−2P⁡0∈ran⁡E→P⁡xP⁡0∈ran⁡E
136 135 exp32 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→¬x<P−2→x∈0..^P−1→P⁡P−2P⁡0∈ran⁡E→P⁡xP⁡0∈ran⁡E
137 136 com12 ⊢¬x<P−2→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1→P⁡P−2P⁡0∈ran⁡E→P⁡xP⁡0∈ran⁡E
138 137 com14 ⊢P⁡P−2P⁡0∈ran⁡E→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1→¬x<P−2→P⁡xP⁡0∈ran⁡E
139 138 adantl ⊢∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1→¬x<P−2→P⁡xP⁡0∈ran⁡E
140 139 adantl ⊢lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1→¬x<P−2→P⁡xP⁡0∈ran⁡E
141 140 com12 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→x∈0..^P−1→¬x<P−2→P⁡xP⁡0∈ran⁡E
142 141 imp31 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→¬x<P−2→P⁡xP⁡0∈ran⁡E
143 142 impcom ⊢¬x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→P⁡xP⁡0∈ran⁡E
144 f1ocnvdm ⊢E:dom⁡E⟶1-1 ontoran⁡E∧P⁡xP⁡0∈ran⁡E→E-1⁡P⁡xP⁡0∈dom⁡E
145 99 143 144 syl2anc ⊢¬x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→E-1⁡P⁡xP⁡0∈dom⁡E
146 98 145 jca ⊢¬x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→¬x<P−2∧E-1⁡P⁡xP⁡0∈dom⁡E
147 146 olcd ⊢¬x<P−2∧E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→x<P−2∧E-1⁡P⁡xP⁡x+1∈dom⁡E∨¬x<P−2∧E-1⁡P⁡xP⁡0∈dom⁡E
148 97 147 pm2.61ian ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→x<P−2∧E-1⁡P⁡xP⁡x+1∈dom⁡E∨¬x<P−2∧E-1⁡P⁡xP⁡0∈dom⁡E
149 ifel ⊢ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈dom⁡E↔x<P−2∧E-1⁡P⁡xP⁡x+1∈dom⁡E∨¬x<P−2∧E-1⁡P⁡xP⁡0∈dom⁡E
150 148 149 sylibr ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E∧x∈0..^P−1→ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈dom⁡E
151 150 1 fmptd ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→F:0..^P−1⟶dom⁡E
152 iswrdi ⊢F:0..^P−1⟶dom⁡E→F∈Worddom⁡E
153 151 152 syl ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→F∈Worddom⁡E
154 wrdf ⊢P∈WordV→P:0..^P⟶V
155 154 adantr ⊢P∈WordV∧2≤P→P:0..^P⟶V
156 1 clwlkclwwlklem2a2 ⊢P∈WordV∧2≤P→F=P−1
157 fzoval ⊢P∈ℤ→0..^P=0…P−1
158 8 22 157 3syl ⊢P∈WordV→0..^P=0…P−1
159 oveq2 ⊢P−1=F→0…P−1=0…F
160 159 eqcoms ⊢F=P−1→0…P−1=0…F
161 158 160 sylan9eq ⊢P∈WordV∧F=P−1→0..^P=0…F
162 156 161 syldan ⊢P∈WordV∧2≤P→0..^P=0…F
163 162 feq2d ⊢P∈WordV∧2≤P→P:0..^P⟶V↔P:0…F⟶V
164 155 163 mpbid ⊢P∈WordV∧2≤P→P:0…F⟶V
165 164 3adant1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→P:0…F⟶V
166 165 adantr ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P:0…F⟶V
167 clwlkclwwlklem2a1 ⊢P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E
168 167 3adant1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E
169 168 imp ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E
170 156 3adant1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→F=P−1
171 170 adantr ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0→F=P−1
172 1 clwlkclwwlklem2a4 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧i∈0..^P−1→P⁡iP⁡i+1∈ran⁡E→E⁡F⁡i=P⁡iP⁡i+1
173 172 impl ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧i∈0..^P−1→P⁡iP⁡i+1∈ran⁡E→E⁡F⁡i=P⁡iP⁡i+1
174 173 ralimdva ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^P−1E⁡F⁡i=P⁡iP⁡i+1
175 oveq2 ⊢F=P−1→0..^F=0..^P−1
176 175 raleqdv ⊢F=P−1→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1↔∀i∈0..^P−1E⁡F⁡i=P⁡iP⁡i+1
177 176 imbi2d ⊢F=P−1→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1↔∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^P−1E⁡F⁡i=P⁡iP⁡i+1
178 174 177 imbitrrid ⊢F=P−1→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
179 171 178 mpcom ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
180 179 adantrr ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
181 169 180 mpd ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
182 153 166 181 3jca ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
183 1 clwlkclwwlklem2a3 ⊢P∈WordV∧2≤P→P⁡F=lastS⁡P
184 183 3adant1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→P⁡F=lastS⁡P
185 184 eqcomd ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡F
186 185 eqeq2d ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→P⁡0=lastS⁡P↔P⁡0=P⁡F
187 186 biimpcd ⊢P⁡0=lastS⁡P→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→P⁡0=P⁡F
188 187 eqcoms ⊢lastS⁡P=P⁡0→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→P⁡0=P⁡F
189 188 adantr ⊢lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→P⁡0=P⁡F
190 189 impcom ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P⁡0=P⁡F
191 182 190 jca ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1∧P⁡0=P⁡F
192 191 ex ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1∧P⁡0=P⁡F