Metamath Proof Explorer

Theorem clwlkclwwlklem3

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

Ref Expression
Assertion clwlkclwwlklem3 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E

Proof

Step Hyp Ref Expression
1 simp1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→E:dom⁡E⟶1-1R
2 simp1 ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1→f∈Worddom⁡E
3 2 adantr ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→f∈Worddom⁡E
4 1 3 anim12i ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→E:dom⁡E⟶1-1R∧f∈Worddom⁡E
5 simp3 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→2≤P
6 simpl2 ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→P:0…f⟶V
7 5 6 anim12ci ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→P:0…f⟶V∧2≤P
8 simp3 ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1→∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1
9 8 anim1i ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
10 9 adantl ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
11 clwlkclwwlklem2 ⊢E:dom⁡E⟶1-1R∧f∈Worddom⁡E∧P:0…f⟶V∧2≤P∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
12 4 7 10 11 syl3anc ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
13 lencl ⊢P∈WordV→P∈ℕ0
14 lencl ⊢f∈Worddom⁡E→f∈ℕ0
15 ffz0hash ⊢f∈ℕ0∧P:0…f⟶V→P=f+1
16 oveq1 ⊢P=f+1→P−1=f+1-1
17 16 oveq1d ⊢P=f+1→P-1-0=f+1-1-0
18 nn0cn ⊢f∈ℕ0→f∈ℂ
19 peano2cn ⊢f∈ℂ→f+1∈ℂ
20 peano2cnm ⊢f+1∈ℂ→f+1-1∈ℂ
21 18 19 20 3syl ⊢f∈ℕ0→f+1-1∈ℂ
22 21 subid1d ⊢f∈ℕ0→f+1-1-0=f+1-1
23 1cnd ⊢f∈ℕ0→1∈ℂ
24 18 23 pncand ⊢f∈ℕ0→f+1-1=f
25 22 24 eqtrd ⊢f∈ℕ0→f+1-1-0=f
26 25 adantr ⊢f∈ℕ0∧P∈ℕ0→f+1-1-0=f
27 17 26 sylan9eqr ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→P-1-0=f
28 27 oveq1d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→P−1-0-1=f−1
29 28 oveq2d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→0..^P−1-0-1=0..^f−1
30 29 raleqdv ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E↔∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E
31 oveq1 ⊢P=f+1→P−2=f+1-2
32 2cnd ⊢f∈ℕ0→2∈ℂ
33 18 32 23 subsub3d ⊢f∈ℕ0→f−2−1=f+1-2
34 2m1e1 ⊢2−1=1
35 34 a1i ⊢f∈ℕ0→2−1=1
36 35 oveq2d ⊢f∈ℕ0→f−2−1=f−1
37 33 36 eqtr3d ⊢f∈ℕ0→f+1-2=f−1
38 37 adantr ⊢f∈ℕ0∧P∈ℕ0→f+1-2=f−1
39 31 38 sylan9eqr ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→P−2=f−1
40 39 fveq2d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→P⁡P−2=P⁡f−1
41 40 preq1d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→P⁡P−2P⁡0=P⁡f−1P⁡0
42 41 eleq1d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→P⁡P−2P⁡0∈ran⁡E↔P⁡f−1P⁡0∈ran⁡E
43 30 42 anbi12d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
44 43 anbi2d ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
45 3anass ⊢lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
46 44 45 bitr4di ⊢f∈ℕ0∧P∈ℕ0∧P=f+1→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
47 46 expcom ⊢P=f+1→f∈ℕ0∧P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
48 47 expd ⊢P=f+1→f∈ℕ0→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
49 15 48 syl ⊢f∈ℕ0∧P:0…f⟶V→f∈ℕ0→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
50 49 ex ⊢f∈ℕ0→P:0…f⟶V→f∈ℕ0→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
51 50 com23 ⊢f∈ℕ0→f∈ℕ0→P:0…f⟶V→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
52 14 14 51 sylc ⊢f∈Worddom⁡E→P:0…f⟶V→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
53 52 imp ⊢f∈Worddom⁡E∧P:0…f⟶V→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
54 53 3adant3 ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
55 54 adantr ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→P∈ℕ0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
56 13 55 syl5com ⊢P∈WordV→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
57 56 3ad2ant2 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
58 57 imp ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧∀i∈0..^f−1P⁡iP⁡i+1∈ran⁡E∧P⁡f−1P⁡0∈ran⁡E
59 12 58 mpbird ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E
60 59 ex ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E
61 60 exlimdv ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E
62 clwlkclwwlklem1 ⊢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→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
63 61 62 impbid ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E