Metamath Proof Explorer


Theorem seqf1olem2a

Description: Lemma for seqf1o . (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses seqf1o.1
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqf1o.2
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
seqf1o.3
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqf1o.4
|- ( ph -> N e. ( ZZ>= ` M ) )
seqf1o.5
|- ( ph -> C C_ S )
seqf1olem2a.1
|- ( ph -> G : A --> C )
seqf1olem2a.3
|- ( ph -> K e. A )
seqf1olem2a.4
|- ( ph -> ( M ... N ) C_ A )
Assertion seqf1olem2a
|- ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqf1o.2
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
3 seqf1o.3
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
4 seqf1o.4
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 seqf1o.5
 |-  ( ph -> C C_ S )
6 seqf1olem2a.1
 |-  ( ph -> G : A --> C )
7 seqf1olem2a.3
 |-  ( ph -> K e. A )
8 seqf1olem2a.4
 |-  ( ph -> ( M ... N ) C_ A )
9 eluzfz2
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
10 4 9 syl
 |-  ( ph -> N e. ( M ... N ) )
11 fveq2
 |-  ( m = M -> ( seq M ( .+ , G ) ` m ) = ( seq M ( .+ , G ) ` M ) )
12 11 oveq2d
 |-  ( m = M -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( G ` K ) .+ ( seq M ( .+ , G ) ` M ) ) )
13 11 oveq1d
 |-  ( m = M -> ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) = ( ( seq M ( .+ , G ) ` M ) .+ ( G ` K ) ) )
14 12 13 eqeq12d
 |-  ( m = M -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) <-> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` M ) ) = ( ( seq M ( .+ , G ) ` M ) .+ ( G ` K ) ) ) )
15 14 imbi2d
 |-  ( m = M -> ( ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) ) <-> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` M ) ) = ( ( seq M ( .+ , G ) ` M ) .+ ( G ` K ) ) ) ) )
16 fveq2
 |-  ( m = n -> ( seq M ( .+ , G ) ` m ) = ( seq M ( .+ , G ) ` n ) )
17 16 oveq2d
 |-  ( m = n -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) )
18 16 oveq1d
 |-  ( m = n -> ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) )
19 17 18 eqeq12d
 |-  ( m = n -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) <-> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) ) )
20 19 imbi2d
 |-  ( m = n -> ( ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) ) <-> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) ) ) )
21 fveq2
 |-  ( m = ( n + 1 ) -> ( seq M ( .+ , G ) ` m ) = ( seq M ( .+ , G ) ` ( n + 1 ) ) )
22 21 oveq2d
 |-  ( m = ( n + 1 ) -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) )
23 21 oveq1d
 |-  ( m = ( n + 1 ) -> ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) )
24 22 23 eqeq12d
 |-  ( m = ( n + 1 ) -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) <-> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) ) )
25 24 imbi2d
 |-  ( m = ( n + 1 ) -> ( ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) ) <-> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) ) ) )
26 fveq2
 |-  ( m = N -> ( seq M ( .+ , G ) ` m ) = ( seq M ( .+ , G ) ` N ) )
27 26 oveq2d
 |-  ( m = N -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) )
28 26 oveq1d
 |-  ( m = N -> ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) )
29 27 28 eqeq12d
 |-  ( m = N -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) <-> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) ) )
30 29 imbi2d
 |-  ( m = N -> ( ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` m ) ) = ( ( seq M ( .+ , G ) ` m ) .+ ( G ` K ) ) ) <-> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) ) ) )
31 6 7 ffvelrnd
 |-  ( ph -> ( G ` K ) e. C )
32 eluzel2
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
33 seq1
 |-  ( M e. ZZ -> ( seq M ( .+ , G ) ` M ) = ( G ` M ) )
34 4 32 33 3syl
 |-  ( ph -> ( seq M ( .+ , G ) ` M ) = ( G ` M ) )
35 eluzfz1
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
36 4 35 syl
 |-  ( ph -> M e. ( M ... N ) )
37 8 36 sseldd
 |-  ( ph -> M e. A )
38 6 37 ffvelrnd
 |-  ( ph -> ( G ` M ) e. C )
39 34 38 eqeltrd
 |-  ( ph -> ( seq M ( .+ , G ) ` M ) e. C )
40 2 31 39 caovcomd
 |-  ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` M ) ) = ( ( seq M ( .+ , G ) ` M ) .+ ( G ` K ) ) )
41 40 a1i
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` M ) ) = ( ( seq M ( .+ , G ) ` M ) .+ ( G ` K ) ) ) )
42 oveq1
 |-  ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) .+ ( G ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) .+ ( G ` ( n + 1 ) ) ) )
43 elfzouz
 |-  ( n e. ( M ..^ N ) -> n e. ( ZZ>= ` M ) )
44 43 adantl
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> n e. ( ZZ>= ` M ) )
45 seqp1
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , G ) ` ( n + 1 ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) )
46 44 45 syl
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( seq M ( .+ , G ) ` ( n + 1 ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) )
47 46 oveq2d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( G ` K ) .+ ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )
48 3 adantlr
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
49 5 31 sseldd
 |-  ( ph -> ( G ` K ) e. S )
50 49 adantr
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( G ` K ) e. S )
51 5 adantr
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> C C_ S )
52 51 adantr
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ x e. ( M ... n ) ) -> C C_ S )
53 6 adantr
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> G : A --> C )
54 53 adantr
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ x e. ( M ... n ) ) -> G : A --> C )
55 elfzouz2
 |-  ( n e. ( M ..^ N ) -> N e. ( ZZ>= ` n ) )
56 55 adantl
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> N e. ( ZZ>= ` n ) )
57 fzss2
 |-  ( N e. ( ZZ>= ` n ) -> ( M ... n ) C_ ( M ... N ) )
58 56 57 syl
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( M ... n ) C_ ( M ... N ) )
59 8 adantr
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( M ... N ) C_ A )
60 58 59 sstrd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( M ... n ) C_ A )
61 60 sselda
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ x e. ( M ... n ) ) -> x e. A )
62 54 61 ffvelrnd
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ x e. ( M ... n ) ) -> ( G ` x ) e. C )
63 52 62 sseldd
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ x e. ( M ... n ) ) -> ( G ` x ) e. S )
64 1 adantlr
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
65 44 63 64 seqcl
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( seq M ( .+ , G ) ` n ) e. S )
66 fzofzp1
 |-  ( n e. ( M ..^ N ) -> ( n + 1 ) e. ( M ... N ) )
67 66 adantl
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( n + 1 ) e. ( M ... N ) )
68 59 67 sseldd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( n + 1 ) e. A )
69 53 68 ffvelrnd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( G ` ( n + 1 ) ) e. C )
70 51 69 sseldd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( G ` ( n + 1 ) ) e. S )
71 48 50 65 70 caovassd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) .+ ( G ` ( n + 1 ) ) ) = ( ( G ` K ) .+ ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )
72 47 71 eqtr4d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) .+ ( G ` ( n + 1 ) ) ) )
73 48 65 70 50 caovassd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) .+ ( G ` K ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( ( G ` ( n + 1 ) ) .+ ( G ` K ) ) ) )
74 46 oveq1d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) = ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) .+ ( G ` K ) ) )
75 48 65 50 70 caovassd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) .+ ( G ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( ( G ` K ) .+ ( G ` ( n + 1 ) ) ) ) )
76 2 adantlr
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
77 31 adantr
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( G ` K ) e. C )
78 76 69 77 caovcomd
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( G ` ( n + 1 ) ) .+ ( G ` K ) ) = ( ( G ` K ) .+ ( G ` ( n + 1 ) ) ) )
79 78 oveq2d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , G ) ` n ) .+ ( ( G ` ( n + 1 ) ) .+ ( G ` K ) ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( ( G ` K ) .+ ( G ` ( n + 1 ) ) ) ) )
80 75 79 eqtr4d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) .+ ( G ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( ( G ` ( n + 1 ) ) .+ ( G ` K ) ) ) )
81 73 74 80 3eqtr4d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) = ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) .+ ( G ` ( n + 1 ) ) ) )
82 72 81 eqeq12d
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) <-> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) .+ ( G ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) .+ ( G ` ( n + 1 ) ) ) ) )
83 42 82 syl5ibr
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) ) )
84 83 expcom
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) ) ) )
85 84 a2d
 |-  ( n e. ( M ..^ N ) -> ( ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` n ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` K ) ) ) -> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( seq M ( .+ , G ) ` ( n + 1 ) ) .+ ( G ` K ) ) ) ) )
86 15 20 25 30 41 85 fzind2
 |-  ( N e. ( M ... N ) -> ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) ) )
87 10 86 mpcom
 |-  ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) )