Metamath Proof Explorer

Theorem clwlkclwwlklem1

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

Ref Expression
Assertion clwlkclwwlklem1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∃ f f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f

Proof

Step Hyp Ref Expression
1 ovex ⊢ 0 ..^ P − 1 ∈ V
2 mptexg ⊢ 0 ..^ P − 1 ∈ V → x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ V
3 1 2 mp1i ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ V
4 eqid ⊢ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
5 4 clwlkclwwlklem2a ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E ∧ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V ∧ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
6 5 adantr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E ∧ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V ∧ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
7 eleq1 ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → f ∈ Word dom ⁡ E ↔ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E
8 fveq2 ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
9 8 oveq2d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → 0 … f = 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
10 9 feq2d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → P : 0 … f ⟶ V ↔ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V
11 8 oveq2d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → 0 ..^ f = 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
12 fveq1 ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → f ⁡ i = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i
13 12 fveqeq2d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ↔ E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1
14 11 13 raleqbidv ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ↔ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1
15 7 10 14 3anbi123d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ↔ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E ∧ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V ∧ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1
16 2fveq3 ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → P ⁡ f = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
17 16 eqeq2d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → P ⁡ 0 = P ⁡ f ↔ P ⁡ 0 = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
18 15 17 anbi12d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f ↔ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E ∧ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V ∧ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
19 18 imbi2d ⊢ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E ∧ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V ∧ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
20 19 adantl ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ Word dom ⁡ E ∧ P : 0 … x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⟶ V ∧ ∀ i ∈ 0 ..^ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 E ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
21 6 20 mpbird ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
22 3 21 spcimedv ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∃ f f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f