Metamath Proof Explorer

Theorem clwlkclwwlklem2fv1

Description: Lemma 4a for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 22-Jun-2018)

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion clwlkclwwlklem2fv1 ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) → ( 𝐹 ‘ 𝐼 ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
2 breq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ 𝐼 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
3 fveq2 ⊢ ( 𝑥 = 𝐼 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐼 ) )
4 fvoveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
5 3 4 preq12d ⊢ ( 𝑥 = 𝐼 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } )
6 5 fveq2d ⊢ ( 𝑥 = 𝐼 → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )
7 3 preq1d ⊢ ( 𝑥 = 𝐼 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ 0 ) } )
8 7 fveq2d ⊢ ( 𝑥 = 𝐼 → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ 0 ) } ) )
9 2 6 8 ifbieq12d ⊢ ( 𝑥 = 𝐼 → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) = if ( 𝐼 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ 0 ) } ) ) )
10 elfzolt2 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 𝐼 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
11 10 adantl ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) → 𝐼 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
12 11 iftrued ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) → if ( 𝐼 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ 0 ) } ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )
13 9 12 sylan9eqr ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) ∧ 𝑥 = 𝐼 ) → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )
14 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
15 2z ⊢ 2 ∈ ℤ
16 15 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℤ )
17 14 16 zsubcld ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
18 peano2zm ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
19 14 18 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
20 1red ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 1 ∈ ℝ )
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℝ )
23 nn0re ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
24 1le2 ⊢ 1 ≤ 2
25 24 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 1 ≤ 2 )
26 20 22 23 25 lesub2dd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ≤ ( ( ♯ ‘ 𝑃 ) − 1 ) )
27 eluz2 ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) ≤ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
28 17 19 26 27 syl3anbrc ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
29 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
30 28 29 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
31 30 sselda ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
32 fvexd ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) ∈ V )
33 1 13 31 32 fvmptd2 ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) → ( 𝐹 ‘ 𝐼 ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )