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 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑤 ∈ 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 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )