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 ) ) )