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=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
Assertion 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

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