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 
|- Z = ( ZZ>= ` M )
algrf.2 
|- R = seq M ( ( F o. 1st ) , ( Z X. { A } ) )
Assertion seq1st 
|- ( ( M e. ZZ /\ A e. V ) -> R = seq M ( ( F o. 1st ) , { <. M , A >. } ) )

Proof

Step Hyp Ref Expression
1 algrf.1 
 |-  Z = ( ZZ>= ` M )
2 algrf.2 
 |-  R = seq M ( ( F o. 1st ) , ( Z X. { A } ) )
3 seqfn 
 |-  ( M e. ZZ -> seq M ( ( F o. 1st ) , ( Z X. { A } ) ) Fn ( ZZ>= ` M ) )
4 3 adantr 
 |-  ( ( M e. ZZ /\ A e. V ) -> seq M ( ( F o. 1st ) , ( Z X. { A } ) ) Fn ( ZZ>= ` M ) )
5 seqfn 
 |-  ( M e. ZZ -> seq M ( ( F o. 1st ) , { <. M , A >. } ) Fn ( ZZ>= ` M ) )
6 5 adantr 
 |-  ( ( M e. ZZ /\ A e. V ) -> seq M ( ( F o. 1st ) , { <. M , A >. } ) Fn ( ZZ>= ` M ) )
7 fveq2 
 |-  ( y = M -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) )
8 fveq2 
 |-  ( y = M -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) )
9 7 8 eqeq12d 
 |-  ( y = M -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) <-> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) ) )
10 9 imbi2d 
 |-  ( y = M -> ( ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) ) <-> ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) ) ) )
11 fveq2 
 |-  ( y = x -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) )
12 fveq2 
 |-  ( y = x -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) )
13 11 12 eqeq12d 
 |-  ( y = x -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) <-> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) )
14 13 imbi2d 
 |-  ( y = x -> ( ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) ) <-> ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) ) )
15 fveq2 
 |-  ( y = ( x + 1 ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) )
16 fveq2 
 |-  ( y = ( x + 1 ) -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) )
17 15 16 eqeq12d 
 |-  ( y = ( x + 1 ) -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) <-> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) ) )
18 17 imbi2d 
 |-  ( y = ( x + 1 ) -> ( ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` y ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` y ) ) <-> ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) ) ) )
19 seq1 
 |-  ( M e. ZZ -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( ( Z X. { A } ) ` M ) )
20 19 adantr 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( ( Z X. { A } ) ` M ) )
21 seq1 
 |-  ( M e. ZZ -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) = ( { <. M , A >. } ` M ) )
22 21 adantr 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) = ( { <. M , A >. } ` M ) )
23 id 
 |-  ( A e. V -> A e. V )
24 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
25 24 1 eleqtrrdi 
 |-  ( M e. ZZ -> M e. Z )
26 fvconst2g 
 |-  ( ( A e. V /\ M e. Z ) -> ( ( Z X. { A } ) ` M ) = A )
27 23 25 26 syl2anr 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( ( Z X. { A } ) ` M ) = A )
28 fvsng 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( { <. M , A >. } ` M ) = A )
29 27 28 eqtr4d 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( ( Z X. { A } ) ` M ) = ( { <. M , A >. } ` M ) )
30 22 29 eqtr4d 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) = ( ( Z X. { A } ) ` M ) )
31 20 30 eqtr4d 
 |-  ( ( M e. ZZ /\ A e. V ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) )
32 31 ex 
 |-  ( M e. ZZ -> ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` M ) ) )
33 fveq2 
 |-  ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) -> ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) ) = ( F ` ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) )
34 seqp1 
 |-  ( x e. ( ZZ>= ` M ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) ( F o. 1st ) ( ( Z X. { A } ) ` ( x + 1 ) ) ) )
35 fvex 
 |-  ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) e. _V
36 fvex 
 |-  ( ( Z X. { A } ) ` ( x + 1 ) ) e. _V
37 35 36 algrflem 
 |-  ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) ( F o. 1st ) ( ( Z X. { A } ) ` ( x + 1 ) ) ) = ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) )
38 34 37 eqtrdi 
 |-  ( x e. ( ZZ>= ` M ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) ) )
39 seqp1 
 |-  ( x e. ( ZZ>= ` M ) -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) = ( ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ( F o. 1st ) ( { <. M , A >. } ` ( x + 1 ) ) ) )
40 fvex 
 |-  ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) e. _V
41 fvex 
 |-  ( { <. M , A >. } ` ( x + 1 ) ) e. _V
42 40 41 algrflem 
 |-  ( ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ( F o. 1st ) ( { <. M , A >. } ` ( x + 1 ) ) ) = ( F ` ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) )
43 39 42 eqtrdi 
 |-  ( x e. ( ZZ>= ` M ) -> ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) = ( F ` ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) )
44 38 43 eqeq12d 
 |-  ( x e. ( ZZ>= ` M ) -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) <-> ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) ) = ( F ` ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) ) )
45 44 adantl 
 |-  ( ( A e. V /\ x e. ( ZZ>= ` M ) ) -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) <-> ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) ) = ( F ` ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) ) )
46 33 45 syl5ibr 
 |-  ( ( A e. V /\ x e. ( ZZ>= ` M ) ) -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) ) )
47 46 expcom 
 |-  ( x e. ( ZZ>= ` M ) -> ( A e. V -> ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) ) ) )
48 47 a2d 
 |-  ( x e. ( ZZ>= ` M ) -> ( ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) -> ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( x + 1 ) ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` ( x + 1 ) ) ) ) )
49 10 14 18 14 32 48 uzind4 
 |-  ( x e. ( ZZ>= ` M ) -> ( A e. V -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) ) )
50 49 impcom 
 |-  ( ( A e. V /\ x e. ( ZZ>= ` M ) ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) )
51 50 adantll 
 |-  ( ( ( M e. ZZ /\ A e. V ) /\ x e. ( ZZ>= ` M ) ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` x ) = ( seq M ( ( F o. 1st ) , { <. M , A >. } ) ` x ) )
52 4 6 51 eqfnfvd 
 |-  ( ( M e. ZZ /\ A e. V ) -> seq M ( ( F o. 1st ) , ( Z X. { A } ) ) = seq M ( ( F o. 1st ) , { <. M , A >. } ) )
53 2 52 syl5eq 
 |-  ( ( M e. ZZ /\ A e. V ) -> R = seq M ( ( F o. 1st ) , { <. M , A >. } ) )