Metamath Proof Explorer


Theorem seq1st

Description: A sequence whose iteration function ignores the second argument is only affected by the first point of the initial value function. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses algrf.1 𝑍 = ( ℤ𝑀 )
algrf.2 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
Assertion seq1st ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 algrf.1 𝑍 = ( ℤ𝑀 )
2 algrf.2 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
3 seqfn ( 𝑀 ∈ ℤ → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) Fn ( ℤ𝑀 ) )
4 3 adantr ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) Fn ( ℤ𝑀 ) )
5 seqfn ( 𝑀 ∈ ℤ → seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) Fn ( ℤ𝑀 ) )
6 5 adantr ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) Fn ( ℤ𝑀 ) )
7 fveq2 ( 𝑦 = 𝑀 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) )
8 fveq2 ( 𝑦 = 𝑀 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) )
9 7 8 eqeq12d ( 𝑦 = 𝑀 → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) ) )
10 9 imbi2d ( 𝑦 = 𝑀 → ( ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) ) ) )
11 fveq2 ( 𝑦 = 𝑥 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) )
12 fveq2 ( 𝑦 = 𝑥 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
13 11 12 eqeq12d ( 𝑦 = 𝑥 → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
14 13 imbi2d ( 𝑦 = 𝑥 → ( ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) ) )
15 fveq2 ( 𝑦 = ( 𝑥 + 1 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) )
16 fveq2 ( 𝑦 = ( 𝑥 + 1 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) )
17 15 16 eqeq12d ( 𝑦 = ( 𝑥 + 1 ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) )
18 17 imbi2d ( 𝑦 = ( 𝑥 + 1 ) → ( ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) ) )
19 seq1 ( 𝑀 ∈ ℤ → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
20 19 adantr ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
21 seq1 ( 𝑀 ∈ ℤ → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) = ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) )
22 21 adantr ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) = ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) )
23 id ( 𝐴𝑉𝐴𝑉 )
24 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
25 24 1 eleqtrrdi ( 𝑀 ∈ ℤ → 𝑀𝑍 )
26 fvconst2g ( ( 𝐴𝑉𝑀𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = 𝐴 )
27 23 25 26 syl2anr ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = 𝐴 )
28 fvsng ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) = 𝐴 )
29 27 28 eqtr4d ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) )
30 22 29 eqtr4d ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
31 20 30 eqtr4d ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) )
32 31 ex ( 𝑀 ∈ ℤ → ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) ) )
33 fveq2 ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) → ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
34 seqp1 ( 𝑥 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝑥 + 1 ) ) ) )
35 fvex ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ∈ V
36 fvex ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝑥 + 1 ) ) ∈ V
37 35 36 algrflem ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝑥 + 1 ) ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) )
38 34 37 eqtrdi ( 𝑥 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) )
39 seqp1 ( 𝑥 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ ( 𝑥 + 1 ) ) ) )
40 fvex ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ∈ V
41 fvex ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ ( 𝑥 + 1 ) ) ∈ V
42 40 41 algrflem ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ ( 𝑥 + 1 ) ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
43 39 42 eqtrdi ( 𝑥 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
44 38 43 eqeq12d ( 𝑥 ∈ ( ℤ𝑀 ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ↔ ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) ) )
45 44 adantl ( ( 𝐴𝑉𝑥 ∈ ( ℤ𝑀 ) ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ↔ ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) ) )
46 33 45 syl5ibr ( ( 𝐴𝑉𝑥 ∈ ( ℤ𝑀 ) ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) )
47 46 expcom ( 𝑥 ∈ ( ℤ𝑀 ) → ( 𝐴𝑉 → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) ) )
48 47 a2d ( 𝑥 ∈ ( ℤ𝑀 ) → ( ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) → ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) ) )
49 10 14 18 14 32 48 uzind4 ( 𝑥 ∈ ( ℤ𝑀 ) → ( 𝐴𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
50 49 impcom ( ( 𝐴𝑉𝑥 ∈ ( ℤ𝑀 ) ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
51 50 adantll ( ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) ∧ 𝑥 ∈ ( ℤ𝑀 ) ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
52 4 6 51 eqfnfvd ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) = seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) )
53 2 52 eqtrid ( ( 𝑀 ∈ ℤ ∧ 𝐴𝑉 ) → 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) )