Metamath Proof Explorer

Theorem fargshiftfva

Description: The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017)

Ref Expression
Hypothesis fargshift.g ⊢ 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
Assertion fargshiftfva ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ∀ 𝑙 ∈ ( 0 ..^ 𝑁 ) ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 fargshift.g ⊢ 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
2 fz0add1fz1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) )
3 simpl ⊢ ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) )
4 3 adantr ⊢ ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) )
5 2fveq3 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ ( 𝑙 + 1 ) ) ) )
6 csbeq1 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ⦋ 𝑘 / 𝑥 ⦌ 𝑃 = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 )
7 5 6 eqeq12d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 ↔ ( 𝐸 ‘ ( 𝐹 ‘ ( 𝑙 + 1 ) ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )
8 7 adantl ⊢ ( ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑘 = ( 𝑙 + 1 ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 ↔ ( 𝐸 ‘ ( 𝐹 ‘ ( 𝑙 + 1 ) ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )
9 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
10 9 adantl ⊢ ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
11 10 anim1i ⊢ ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) )
12 11 adantr ⊢ ( ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑘 = ( 𝑙 + 1 ) ) → ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) )
13 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → 𝑙 ∈ ( 0 ..^ 𝑁 ) )
14 13 ad3antlr ⊢ ( ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑘 = ( 𝑙 + 1 ) ) → 𝑙 ∈ ( 0 ..^ 𝑁 ) )
15 1 fargshiftfv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( 𝑙 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑙 ) = ( 𝐹 ‘ ( 𝑙 + 1 ) ) ) )
16 15 imp ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝑙 ) = ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
17 16 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑙 + 1 ) ) = ( 𝐺 ‘ 𝑙 ) )
18 12 14 17 syl2anc ⊢ ( ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑘 = ( 𝑙 + 1 ) ) → ( 𝐹 ‘ ( 𝑙 + 1 ) ) = ( 𝐺 ‘ 𝑙 ) )
19 18 fveqeq2d ⊢ ( ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑘 = ( 𝑙 + 1 ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ ( 𝑙 + 1 ) ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ↔ ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )
20 8 19 bitrd ⊢ ( ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑘 = ( 𝑙 + 1 ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 ↔ ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )
21 4 20 rspcdv ⊢ ( ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )
22 21 ex ⊢ ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) ) )
23 22 com23 ⊢ ( ( ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) ) )
24 2 23 mpancom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) ) )
25 24 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑙 ∈ ( 0 ..^ 𝑁 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) ) ) )
26 25 com24 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ( 𝑙 ∈ ( 0 ..^ 𝑁 ) → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) ) ) )
27 26 imp31 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 ) → ( 𝑙 ∈ ( 0 ..^ 𝑁 ) → ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )
28 27 ralrimiv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 ) → ∀ 𝑙 ∈ ( 0 ..^ 𝑁 ) ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 )
29 28 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ⦋ 𝑘 / 𝑥 ⦌ 𝑃 → ∀ 𝑙 ∈ ( 0 ..^ 𝑁 ) ( 𝐸 ‘ ( 𝐺 ‘ 𝑙 ) ) = ⦋ ( 𝑙 + 1 ) / 𝑥 ⦌ 𝑃 ) )