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 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) )