Metamath Proof Explorer

Theorem crctcshwlkn0lem2

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s ⊢ ( 𝜑 → 𝑆 ∈ ( 1 ..^ 𝑁 ) )
crctcshwlkn0lem.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion crctcshwlkn0lem2 ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → ( 𝑄 ‘ 𝐽 ) = ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ⊢ ( 𝜑 → 𝑆 ∈ ( 1 ..^ 𝑁 ) )
2 crctcshwlkn0lem.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
3 breq1 ⊢ ( 𝑥 = 𝐽 → ( 𝑥 ≤ ( 𝑁 − 𝑆 ) ↔ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
4 fvoveq1 ⊢ ( 𝑥 = 𝐽 → ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) = ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) )
5 oveq1 ⊢ ( 𝑥 = 𝐽 → ( 𝑥 + 𝑆 ) = ( 𝐽 + 𝑆 ) )
6 5 fvoveq1d ⊢ ( 𝑥 = 𝐽 → ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) = ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) )
7 3 4 6 ifbieq12d ⊢ ( 𝑥 = 𝐽 → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) = if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) )
8 fzo0ss1 ⊢ ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 )
9 8 sseli ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
10 elfzoel2 ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
11 elfzonn0 ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℕ0 )
12 eluzmn ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝑆 ) ) )
13 10 11 12 syl2anc ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝑆 ) ) )
14 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝑆 ) ) → ( 0 ... ( 𝑁 − 𝑆 ) ) ⊆ ( 0 ... 𝑁 ) )
15 13 14 syl ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → ( 0 ... ( 𝑁 − 𝑆 ) ) ⊆ ( 0 ... 𝑁 ) )
16 15 sseld ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) → 𝐽 ∈ ( 0 ... 𝑁 ) ) )
17 1 9 16 3syl ⊢ ( 𝜑 → ( 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) → 𝐽 ∈ ( 0 ... 𝑁 ) ) )
18 17 imp ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
19 fvex ⊢ ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) ∈ V
20 fvex ⊢ ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ∈ V
21 19 20 ifex ⊢ if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) ∈ V
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) ∈ V )
23 2 7 18 22 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → ( 𝑄 ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) )
24 elfzle2 ⊢ ( 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) → 𝐽 ≤ ( 𝑁 − 𝑆 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → 𝐽 ≤ ( 𝑁 − 𝑆 ) )
26 25 iftrued ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) = ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) )
27 23 26 eqtrd ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → ( 𝑄 ‘ 𝐽 ) = ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) )