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 ( 𝜑𝐴𝑉 )
seqof.2 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
seqof.3 ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) = ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) )
Assertion seqof ( 𝜑 → ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) = ( 𝑧𝐴 ↦ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 seqof.1 ( 𝜑𝐴𝑉 )
2 seqof.2 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
3 seqof.3 ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) = ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) )
4 fvex ( 𝐺𝑥 ) ∈ V
5 4 rgenw 𝑧𝐴 ( 𝐺𝑥 ) ∈ V
6 eqid ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) = ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) )
7 6 fnmpt ( ∀ 𝑧𝐴 ( 𝐺𝑥 ) ∈ V → ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) Fn 𝐴 )
8 5 7 mp1i ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) Fn 𝐴 )
9 3 fneq1d ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) Fn 𝐴 ↔ ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) Fn 𝐴 ) )
10 8 9 mpbird ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) Fn 𝐴 )
11 fvex ( 𝐹𝑥 ) ∈ V
12 fneq1 ( 𝑧 = ( 𝐹𝑥 ) → ( 𝑧 Fn 𝐴 ↔ ( 𝐹𝑥 ) Fn 𝐴 ) )
13 11 12 elab ( ( 𝐹𝑥 ) ∈ { 𝑧𝑧 Fn 𝐴 } ↔ ( 𝐹𝑥 ) Fn 𝐴 )
14 10 13 sylibr ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) ∈ { 𝑧𝑧 Fn 𝐴 } )
15 simprl ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) → 𝑥 Fn 𝐴 )
16 simprr ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) → 𝑦 Fn 𝐴 )
17 1 adantr ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) → 𝐴𝑉 )
18 inidm ( 𝐴𝐴 ) = 𝐴
19 15 16 17 17 18 offn ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) → ( 𝑥f + 𝑦 ) Fn 𝐴 )
20 19 ex ( 𝜑 → ( ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) → ( 𝑥f + 𝑦 ) Fn 𝐴 ) )
21 vex 𝑥 ∈ V
22 fneq1 ( 𝑧 = 𝑥 → ( 𝑧 Fn 𝐴𝑥 Fn 𝐴 ) )
23 21 22 elab ( 𝑥 ∈ { 𝑧𝑧 Fn 𝐴 } ↔ 𝑥 Fn 𝐴 )
24 vex 𝑦 ∈ V
25 fneq1 ( 𝑧 = 𝑦 → ( 𝑧 Fn 𝐴𝑦 Fn 𝐴 ) )
26 24 25 elab ( 𝑦 ∈ { 𝑧𝑧 Fn 𝐴 } ↔ 𝑦 Fn 𝐴 )
27 23 26 anbi12i ( ( 𝑥 ∈ { 𝑧𝑧 Fn 𝐴 } ∧ 𝑦 ∈ { 𝑧𝑧 Fn 𝐴 } ) ↔ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) )
28 ovex ( 𝑥f + 𝑦 ) ∈ V
29 fneq1 ( 𝑧 = ( 𝑥f + 𝑦 ) → ( 𝑧 Fn 𝐴 ↔ ( 𝑥f + 𝑦 ) Fn 𝐴 ) )
30 28 29 elab ( ( 𝑥f + 𝑦 ) ∈ { 𝑧𝑧 Fn 𝐴 } ↔ ( 𝑥f + 𝑦 ) Fn 𝐴 )
31 20 27 30 3imtr4g ( 𝜑 → ( ( 𝑥 ∈ { 𝑧𝑧 Fn 𝐴 } ∧ 𝑦 ∈ { 𝑧𝑧 Fn 𝐴 } ) → ( 𝑥f + 𝑦 ) ∈ { 𝑧𝑧 Fn 𝐴 } ) )
32 31 imp ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑧𝑧 Fn 𝐴 } ∧ 𝑦 ∈ { 𝑧𝑧 Fn 𝐴 } ) ) → ( 𝑥f + 𝑦 ) ∈ { 𝑧𝑧 Fn 𝐴 } )
33 2 14 32 seqcl ( 𝜑 → ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑧𝑧 Fn 𝐴 } )
34 fvex ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ∈ V
35 fneq1 ( 𝑧 = ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) → ( 𝑧 Fn 𝐴 ↔ ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) Fn 𝐴 ) )
36 34 35 elab ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑧𝑧 Fn 𝐴 } ↔ ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) Fn 𝐴 )
37 33 36 sylib ( 𝜑 → ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) Fn 𝐴 )
38 dffn5 ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) Fn 𝐴 ↔ ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) = ( 𝑧𝐴 ↦ ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) ) )
39 37 38 sylib ( 𝜑 → ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) = ( 𝑧𝐴 ↦ ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) ) )
40 fveq1 ( 𝑤 = ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) → ( 𝑤𝑧 ) = ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) )
41 eqid ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) = ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) )
42 fvex ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) ∈ V
43 40 41 42 fvmpt ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ∈ V → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) )
44 34 43 mp1i ( ( 𝜑𝑧𝐴 ) → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) )
45 32 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ ( 𝑥 ∈ { 𝑧𝑧 Fn 𝐴 } ∧ 𝑦 ∈ { 𝑧𝑧 Fn 𝐴 } ) ) → ( 𝑥f + 𝑦 ) ∈ { 𝑧𝑧 Fn 𝐴 } )
46 14 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) ∈ { 𝑧𝑧 Fn 𝐴 } )
47 2 adantr ( ( 𝜑𝑧𝐴 ) → 𝑁 ∈ ( ℤ𝑀 ) )
48 eqidd ( ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) ∧ 𝑧𝐴 ) → ( 𝑥𝑧 ) = ( 𝑥𝑧 ) )
49 eqidd ( ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) ∧ 𝑧𝐴 ) → ( 𝑦𝑧 ) = ( 𝑦𝑧 ) )
50 15 16 17 17 18 48 49 ofval ( ( ( 𝜑 ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) ∧ 𝑧𝐴 ) → ( ( 𝑥f + 𝑦 ) ‘ 𝑧 ) = ( ( 𝑥𝑧 ) + ( 𝑦𝑧 ) ) )
51 50 an32s ( ( ( 𝜑𝑧𝐴 ) ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) → ( ( 𝑥f + 𝑦 ) ‘ 𝑧 ) = ( ( 𝑥𝑧 ) + ( 𝑦𝑧 ) ) )
52 fveq1 ( 𝑤 = ( 𝑥f + 𝑦 ) → ( 𝑤𝑧 ) = ( ( 𝑥f + 𝑦 ) ‘ 𝑧 ) )
53 fvex ( ( 𝑥f + 𝑦 ) ‘ 𝑧 ) ∈ V
54 52 41 53 fvmpt ( ( 𝑥f + 𝑦 ) ∈ V → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝑥f + 𝑦 ) ) = ( ( 𝑥f + 𝑦 ) ‘ 𝑧 ) )
55 28 54 ax-mp ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝑥f + 𝑦 ) ) = ( ( 𝑥f + 𝑦 ) ‘ 𝑧 )
56 fveq1 ( 𝑤 = 𝑥 → ( 𝑤𝑧 ) = ( 𝑥𝑧 ) )
57 fvex ( 𝑥𝑧 ) ∈ V
58 56 41 57 fvmpt ( 𝑥 ∈ V → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑥 ) = ( 𝑥𝑧 ) )
59 58 elv ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑥 ) = ( 𝑥𝑧 )
60 fveq1 ( 𝑤 = 𝑦 → ( 𝑤𝑧 ) = ( 𝑦𝑧 ) )
61 fvex ( 𝑦𝑧 ) ∈ V
62 60 41 61 fvmpt ( 𝑦 ∈ V → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑦 ) = ( 𝑦𝑧 ) )
63 62 elv ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑦 ) = ( 𝑦𝑧 )
64 59 63 oveq12i ( ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑥 ) + ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑦 ) ) = ( ( 𝑥𝑧 ) + ( 𝑦𝑧 ) )
65 51 55 64 3eqtr4g ( ( ( 𝜑𝑧𝐴 ) ∧ ( 𝑥 Fn 𝐴𝑦 Fn 𝐴 ) ) → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝑥f + 𝑦 ) ) = ( ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑥 ) + ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑦 ) ) )
66 27 65 sylan2b ( ( ( 𝜑𝑧𝐴 ) ∧ ( 𝑥 ∈ { 𝑧𝑧 Fn 𝐴 } ∧ 𝑦 ∈ { 𝑧𝑧 Fn 𝐴 } ) ) → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝑥f + 𝑦 ) ) = ( ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑥 ) + ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ 𝑦 ) ) )
67 fveq1 ( 𝑤 = ( 𝐹𝑥 ) → ( 𝑤𝑧 ) = ( ( 𝐹𝑥 ) ‘ 𝑧 ) )
68 fvex ( ( 𝐹𝑥 ) ‘ 𝑧 ) ∈ V
69 67 41 68 fvmpt ( ( 𝐹𝑥 ) ∈ V → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝐹𝑥 ) ) = ( ( 𝐹𝑥 ) ‘ 𝑧 ) )
70 11 69 ax-mp ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝐹𝑥 ) ) = ( ( 𝐹𝑥 ) ‘ 𝑧 )
71 3 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) = ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) )
72 71 fveq1d ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) ‘ 𝑧 ) = ( ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) ‘ 𝑧 ) )
73 simplr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑧𝐴 )
74 6 fvmpt2 ( ( 𝑧𝐴 ∧ ( 𝐺𝑥 ) ∈ V ) → ( ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) ‘ 𝑧 ) = ( 𝐺𝑥 ) )
75 73 4 74 sylancl ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑧𝐴 ↦ ( 𝐺𝑥 ) ) ‘ 𝑧 ) = ( 𝐺𝑥 ) )
76 72 75 eqtrd ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) ‘ 𝑧 ) = ( 𝐺𝑥 ) )
77 70 76 eqtrid ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( 𝐹𝑥 ) ) = ( 𝐺𝑥 ) )
78 45 46 47 66 77 seqhomo ( ( 𝜑𝑧𝐴 ) → ( ( 𝑤 ∈ V ↦ ( 𝑤𝑧 ) ) ‘ ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
79 44 78 eqtr3d ( ( 𝜑𝑧𝐴 ) → ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
80 79 mpteq2dva ( 𝜑 → ( 𝑧𝐴 ↦ ( ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) ‘ 𝑧 ) ) = ( 𝑧𝐴 ↦ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
81 39 80 eqtrd ( 𝜑 → ( seq 𝑀 ( ∘f + , 𝐹 ) ‘ 𝑁 ) = ( 𝑧𝐴 ↦ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )