Metamath Proof Explorer

Theorem seqof

Description: Distribute function operation through a sequence. Note that G ( z ) is an implicit function on z . (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses seqof.1 
|- ( ph -> A e. V )
seqof.2 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqof.3 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) = ( z e. A |-> ( G ` x ) ) )
Assertion seqof 
|- ( ph -> ( seq M ( oF .+ , F ) ` N ) = ( z e. A |-> ( seq M ( .+ , G ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 seqof.1 
 |-  ( ph -> A e. V )
2 seqof.2 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 seqof.3 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) = ( z e. A |-> ( G ` x ) ) )
4 fvex 
 |-  ( G ` x ) e. _V
5 4 rgenw 
 |-  A. z e. A ( G ` x ) e. _V
6 eqid 
 |-  ( z e. A |-> ( G ` x ) ) = ( z e. A |-> ( G ` x ) )
7 6 fnmpt 
 |-  ( A. z e. A ( G ` x ) e. _V -> ( z e. A |-> ( G ` x ) ) Fn A )
8 5 7 mp1i 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( z e. A |-> ( G ` x ) ) Fn A )
9 3 fneq1d 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( F ` x ) Fn A <-> ( z e. A |-> ( G ` x ) ) Fn A ) )
10 8 9 mpbird 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) Fn A )
11 fvex 
 |-  ( F ` x ) e. _V
12 fneq1 
 |-  ( z = ( F ` x ) -> ( z Fn A <-> ( F ` x ) Fn A ) )
13 11 12 elab 
 |-  ( ( F ` x ) e. { z | z Fn A } <-> ( F ` x ) Fn A )
14 10 13 sylibr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. { z | z Fn A } )
15 simprl 
 |-  ( ( ph /\ ( x Fn A /\ y Fn A ) ) -> x Fn A )
16 simprr 
 |-  ( ( ph /\ ( x Fn A /\ y Fn A ) ) -> y Fn A )
17 1 adantr 
 |-  ( ( ph /\ ( x Fn A /\ y Fn A ) ) -> A e. V )
18 inidm 
 |-  ( A i^i A ) = A
19 15 16 17 17 18 offn 
 |-  ( ( ph /\ ( x Fn A /\ y Fn A ) ) -> ( x oF .+ y ) Fn A )
20 19 ex 
 |-  ( ph -> ( ( x Fn A /\ y Fn A ) -> ( x oF .+ y ) Fn A ) )
21 vex 
 |-  x e. _V
22 fneq1 
 |-  ( z = x -> ( z Fn A <-> x Fn A ) )
23 21 22 elab 
 |-  ( x e. { z | z Fn A } <-> x Fn A )
24 vex 
 |-  y e. _V
25 fneq1 
 |-  ( z = y -> ( z Fn A <-> y Fn A ) )
26 24 25 elab 
 |-  ( y e. { z | z Fn A } <-> y Fn A )
27 23 26 anbi12i 
 |-  ( ( x e. { z | z Fn A } /\ y e. { z | z Fn A } ) <-> ( x Fn A /\ y Fn A ) )
28 ovex 
 |-  ( x oF .+ y ) e. _V
29 fneq1 
 |-  ( z = ( x oF .+ y ) -> ( z Fn A <-> ( x oF .+ y ) Fn A ) )
30 28 29 elab 
 |-  ( ( x oF .+ y ) e. { z | z Fn A } <-> ( x oF .+ y ) Fn A )
31 20 27 30 3imtr4g 
 |-  ( ph -> ( ( x e. { z | z Fn A } /\ y e. { z | z Fn A } ) -> ( x oF .+ y ) e. { z | z Fn A } ) )
32 31 imp 
 |-  ( ( ph /\ ( x e. { z | z Fn A } /\ y e. { z | z Fn A } ) ) -> ( x oF .+ y ) e. { z | z Fn A } )
33 2 14 32 seqcl 
 |-  ( ph -> ( seq M ( oF .+ , F ) ` N ) e. { z | z Fn A } )
34 fvex 
 |-  ( seq M ( oF .+ , F ) ` N ) e. _V
35 fneq1 
 |-  ( z = ( seq M ( oF .+ , F ) ` N ) -> ( z Fn A <-> ( seq M ( oF .+ , F ) ` N ) Fn A ) )
36 34 35 elab 
 |-  ( ( seq M ( oF .+ , F ) ` N ) e. { z | z Fn A } <-> ( seq M ( oF .+ , F ) ` N ) Fn A )
37 33 36 sylib 
 |-  ( ph -> ( seq M ( oF .+ , F ) ` N ) Fn A )
38 dffn5 
 |-  ( ( seq M ( oF .+ , F ) ` N ) Fn A <-> ( seq M ( oF .+ , F ) ` N ) = ( z e. A |-> ( ( seq M ( oF .+ , F ) ` N ) ` z ) ) )
39 37 38 sylib 
 |-  ( ph -> ( seq M ( oF .+ , F ) ` N ) = ( z e. A |-> ( ( seq M ( oF .+ , F ) ` N ) ` z ) ) )
40 fveq1 
 |-  ( w = ( seq M ( oF .+ , F ) ` N ) -> ( w ` z ) = ( ( seq M ( oF .+ , F ) ` N ) ` z ) )
41 eqid 
 |-  ( w e. _V |-> ( w ` z ) ) = ( w e. _V |-> ( w ` z ) )
42 fvex 
 |-  ( ( seq M ( oF .+ , F ) ` N ) ` z ) e. _V
43 40 41 42 fvmpt 
 |-  ( ( seq M ( oF .+ , F ) ` N ) e. _V -> ( ( w e. _V |-> ( w ` z ) ) ` ( seq M ( oF .+ , F ) ` N ) ) = ( ( seq M ( oF .+ , F ) ` N ) ` z ) )
44 34 43 mp1i 
 |-  ( ( ph /\ z e. A ) -> ( ( w e. _V |-> ( w ` z ) ) ` ( seq M ( oF .+ , F ) ` N ) ) = ( ( seq M ( oF .+ , F ) ` N ) ` z ) )
45 32 adantlr 
 |-  ( ( ( ph /\ z e. A ) /\ ( x e. { z | z Fn A } /\ y e. { z | z Fn A } ) ) -> ( x oF .+ y ) e. { z | z Fn A } )
46 14 adantlr 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. { z | z Fn A } )
47 2 adantr 
 |-  ( ( ph /\ z e. A ) -> N e. ( ZZ>= ` M ) )
48 eqidd 
 |-  ( ( ( ph /\ ( x Fn A /\ y Fn A ) ) /\ z e. A ) -> ( x ` z ) = ( x ` z ) )
49 eqidd 
 |-  ( ( ( ph /\ ( x Fn A /\ y Fn A ) ) /\ z e. A ) -> ( y ` z ) = ( y ` z ) )
50 15 16 17 17 18 48 49 ofval 
 |-  ( ( ( ph /\ ( x Fn A /\ y Fn A ) ) /\ z e. A ) -> ( ( x oF .+ y ) ` z ) = ( ( x ` z ) .+ ( y ` z ) ) )
51 50 an32s 
 |-  ( ( ( ph /\ z e. A ) /\ ( x Fn A /\ y Fn A ) ) -> ( ( x oF .+ y ) ` z ) = ( ( x ` z ) .+ ( y ` z ) ) )
52 fveq1 
 |-  ( w = ( x oF .+ y ) -> ( w ` z ) = ( ( x oF .+ y ) ` z ) )
53 fvex 
 |-  ( ( x oF .+ y ) ` z ) e. _V
54 52 41 53 fvmpt 
 |-  ( ( x oF .+ y ) e. _V -> ( ( w e. _V |-> ( w ` z ) ) ` ( x oF .+ y ) ) = ( ( x oF .+ y ) ` z ) )
55 28 54 ax-mp 
 |-  ( ( w e. _V |-> ( w ` z ) ) ` ( x oF .+ y ) ) = ( ( x oF .+ y ) ` z )
56 fveq1 
 |-  ( w = x -> ( w ` z ) = ( x ` z ) )
57 fvex 
 |-  ( x ` z ) e. _V
58 56 41 57 fvmpt 
 |-  ( x e. _V -> ( ( w e. _V |-> ( w ` z ) ) ` x ) = ( x ` z ) )
59 58 elv 
 |-  ( ( w e. _V |-> ( w ` z ) ) ` x ) = ( x ` z )
60 fveq1 
 |-  ( w = y -> ( w ` z ) = ( y ` z ) )
61 fvex 
 |-  ( y ` z ) e. _V
62 60 41 61 fvmpt 
 |-  ( y e. _V -> ( ( w e. _V |-> ( w ` z ) ) ` y ) = ( y ` z ) )
63 62 elv 
 |-  ( ( w e. _V |-> ( w ` z ) ) ` y ) = ( y ` z )
64 59 63 oveq12i 
 |-  ( ( ( w e. _V |-> ( w ` z ) ) ` x ) .+ ( ( w e. _V |-> ( w ` z ) ) ` y ) ) = ( ( x ` z ) .+ ( y ` z ) )
65 51 55 64 3eqtr4g 
 |-  ( ( ( ph /\ z e. A ) /\ ( x Fn A /\ y Fn A ) ) -> ( ( w e. _V |-> ( w ` z ) ) ` ( x oF .+ y ) ) = ( ( ( w e. _V |-> ( w ` z ) ) ` x ) .+ ( ( w e. _V |-> ( w ` z ) ) ` y ) ) )
66 27 65 sylan2b 
 |-  ( ( ( ph /\ z e. A ) /\ ( x e. { z | z Fn A } /\ y e. { z | z Fn A } ) ) -> ( ( w e. _V |-> ( w ` z ) ) ` ( x oF .+ y ) ) = ( ( ( w e. _V |-> ( w ` z ) ) ` x ) .+ ( ( w e. _V |-> ( w ` z ) ) ` y ) ) )
67 fveq1 
 |-  ( w = ( F ` x ) -> ( w ` z ) = ( ( F ` x ) ` z ) )
68 fvex 
 |-  ( ( F ` x ) ` z ) e. _V
69 67 41 68 fvmpt 
 |-  ( ( F ` x ) e. _V -> ( ( w e. _V |-> ( w ` z ) ) ` ( F ` x ) ) = ( ( F ` x ) ` z ) )
70 11 69 ax-mp 
 |-  ( ( w e. _V |-> ( w ` z ) ) ` ( F ` x ) ) = ( ( F ` x ) ` z )
71 3 adantlr 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> ( F ` x ) = ( z e. A |-> ( G ` x ) ) )
72 71 fveq1d 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) ` z ) = ( ( z e. A |-> ( G ` x ) ) ` z ) )
73 simplr 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> z e. A )
74 6 fvmpt2 
 |-  ( ( z e. A /\ ( G ` x ) e. _V ) -> ( ( z e. A |-> ( G ` x ) ) ` z ) = ( G ` x ) )
75 73 4 74 sylancl 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> ( ( z e. A |-> ( G ` x ) ) ` z ) = ( G ` x ) )
76 72 75 eqtrd 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) ` z ) = ( G ` x ) )
77 70 76 eqtrid 
 |-  ( ( ( ph /\ z e. A ) /\ x e. ( M ... N ) ) -> ( ( w e. _V |-> ( w ` z ) ) ` ( F ` x ) ) = ( G ` x ) )
78 45 46 47 66 77 seqhomo 
 |-  ( ( ph /\ z e. A ) -> ( ( w e. _V |-> ( w ` z ) ) ` ( seq M ( oF .+ , F ) ` N ) ) = ( seq M ( .+ , G ) ` N ) )
79 44 78 eqtr3d 
 |-  ( ( ph /\ z e. A ) -> ( ( seq M ( oF .+ , F ) ` N ) ` z ) = ( seq M ( .+ , G ) ` N ) )
80 79 mpteq2dva 
 |-  ( ph -> ( z e. A |-> ( ( seq M ( oF .+ , F ) ` N ) ` z ) ) = ( z e. A |-> ( seq M ( .+ , G ) ` N ) ) )
81 39 80 eqtrd 
 |-  ( ph -> ( seq M ( oF .+ , F ) ` N ) = ( z e. A |-> ( seq M ( .+ , G ) ` N ) ) )