This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem algrp1

Description: The value of the algorithm iterator R at ( K + 1 ) . (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses algrf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
algrf.2 ⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
algrf.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
algrf.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
algrf.5 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ 𝑆 )
Assertion algrp1 ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → ( 𝑅 ‘ ( 𝐾 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 algrf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 algrf.2 ⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
3 algrf.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 algrf.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
5 algrf.5 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ 𝑆 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → 𝐾 ∈ 𝑍 )
7 6 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 seqp1 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝐾 + 1 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝐾 + 1 ) ) ) )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝐾 + 1 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝐾 + 1 ) ) ) )
10 2 fveq1i ⊢ ( 𝑅 ‘ ( 𝐾 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝐾 + 1 ) )
11 2 fveq1i ⊢ ( 𝑅 ‘ 𝐾 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 )
12 11 fveq2i ⊢ ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) )
13 fvex ⊢ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) ∈ V
14 fvex ⊢ ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝐾 + 1 ) ) ∈ V
15 13 14 opco1i ⊢ ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝐾 + 1 ) ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) )
16 12 15 eqtr4i ⊢ ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝐾 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝐾 + 1 ) ) )
17 9 10 16 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → ( 𝑅 ‘ ( 𝐾 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) )