Step | Hyp | Ref
| Expression |
1 | | seqof.2 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | fvex 6787 |
. . . . . . . . 9
⊢ (𝐺‘𝑥) ∈ V |
3 | 2 | rgenw 3076 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝐴 (𝐺‘𝑥) ∈ V |
4 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) |
5 | 4 | fnmpt 6573 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝐴 (𝐺‘𝑥) ∈ V → (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) Fn 𝐴) |
6 | 3, 5 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) Fn 𝐴) |
7 | | seqof.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))) |
8 | 7 | fneq1d 6526 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) Fn 𝐴 ↔ (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) Fn 𝐴)) |
9 | 6, 8 | mpbird 256 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) Fn 𝐴) |
10 | | fvex 6787 |
. . . . . . 7
⊢ (𝐹‘𝑥) ∈ V |
11 | | fneq1 6524 |
. . . . . . 7
⊢ (𝑧 = (𝐹‘𝑥) → (𝑧 Fn 𝐴 ↔ (𝐹‘𝑥) Fn 𝐴)) |
12 | 10, 11 | elab 3609 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ (𝐹‘𝑥) Fn 𝐴) |
13 | 9, 12 | sylibr 233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) |
14 | | simprl 768 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → 𝑥 Fn 𝐴) |
15 | | simprr 770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → 𝑦 Fn 𝐴) |
16 | | seqof.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
17 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → 𝐴 ∈ 𝑉) |
18 | | inidm 4152 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
19 | 14, 15, 17, 17, 18 | offn 7546 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → (𝑥 ∘f + 𝑦) Fn 𝐴) |
20 | 19 | ex 413 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴) → (𝑥 ∘f + 𝑦) Fn 𝐴)) |
21 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
22 | | fneq1 6524 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧 Fn 𝐴 ↔ 𝑥 Fn 𝐴)) |
23 | 21, 22 | elab 3609 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ 𝑥 Fn 𝐴) |
24 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
25 | | fneq1 6524 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 Fn 𝐴 ↔ 𝑦 Fn 𝐴)) |
26 | 24, 25 | elab 3609 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ 𝑦 Fn 𝐴) |
27 | 23, 26 | anbi12i 627 |
. . . . . . 7
⊢ ((𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) ↔ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) |
28 | | ovex 7308 |
. . . . . . . 8
⊢ (𝑥 ∘f + 𝑦) ∈ V |
29 | | fneq1 6524 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 ∘f + 𝑦) → (𝑧 Fn 𝐴 ↔ (𝑥 ∘f + 𝑦) Fn 𝐴)) |
30 | 28, 29 | elab 3609 |
. . . . . . 7
⊢ ((𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ (𝑥 ∘f + 𝑦) Fn 𝐴) |
31 | 20, 27, 30 | 3imtr4g 296 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) → (𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) |
32 | 31 | imp 407 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) → (𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) |
33 | 1, 13, 32 | seqcl 13743 |
. . . 4
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) |
34 | | fvex 6787 |
. . . . 5
⊢ (seq𝑀( ∘f + , 𝐹)‘𝑁) ∈ V |
35 | | fneq1 6524 |
. . . . 5
⊢ (𝑧 = (seq𝑀( ∘f + , 𝐹)‘𝑁) → (𝑧 Fn 𝐴 ↔ (seq𝑀( ∘f + , 𝐹)‘𝑁) Fn 𝐴)) |
36 | 34, 35 | elab 3609 |
. . . 4
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁) ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ (seq𝑀( ∘f + , 𝐹)‘𝑁) Fn 𝐴) |
37 | 33, 36 | sylib 217 |
. . 3
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) Fn 𝐴) |
38 | | dffn5 6828 |
. . 3
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁) Fn 𝐴 ↔ (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧))) |
39 | 37, 38 | sylib 217 |
. 2
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧))) |
40 | | fveq1 6773 |
. . . . . 6
⊢ (𝑤 = (seq𝑀( ∘f + , 𝐹)‘𝑁) → (𝑤‘𝑧) = ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) |
41 | | eqid 2738 |
. . . . . 6
⊢ (𝑤 ∈ V ↦ (𝑤‘𝑧)) = (𝑤 ∈ V ↦ (𝑤‘𝑧)) |
42 | | fvex 6787 |
. . . . . 6
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁)‘𝑧) ∈ V |
43 | 40, 41, 42 | fvmpt 6875 |
. . . . 5
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁) ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(seq𝑀( ∘f + , 𝐹)‘𝑁)) = ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) |
44 | 34, 43 | mp1i 13 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(seq𝑀( ∘f + , 𝐹)‘𝑁)) = ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) |
45 | 32 | adantlr 712 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) → (𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) |
46 | 13 | adantlr 712 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) |
47 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑁 ∈ (ℤ≥‘𝑀)) |
48 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑥‘𝑧) = (𝑥‘𝑧)) |
49 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑦‘𝑧) = (𝑦‘𝑧)) |
50 | 14, 15, 17, 17, 18, 48, 49 | ofval 7544 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∘f + 𝑦)‘𝑧) = ((𝑥‘𝑧) + (𝑦‘𝑧))) |
51 | 50 | an32s 649 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → ((𝑥 ∘f + 𝑦)‘𝑧) = ((𝑥‘𝑧) + (𝑦‘𝑧))) |
52 | | fveq1 6773 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 ∘f + 𝑦) → (𝑤‘𝑧) = ((𝑥 ∘f + 𝑦)‘𝑧)) |
53 | | fvex 6787 |
. . . . . . . . 9
⊢ ((𝑥 ∘f + 𝑦)‘𝑧) ∈ V |
54 | 52, 41, 53 | fvmpt 6875 |
. . . . . . . 8
⊢ ((𝑥 ∘f + 𝑦) ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = ((𝑥 ∘f + 𝑦)‘𝑧)) |
55 | 28, 54 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = ((𝑥 ∘f + 𝑦)‘𝑧) |
56 | | fveq1 6773 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤‘𝑧) = (𝑥‘𝑧)) |
57 | | fvex 6787 |
. . . . . . . . . 10
⊢ (𝑥‘𝑧) ∈ V |
58 | 56, 41, 57 | fvmpt 6875 |
. . . . . . . . 9
⊢ (𝑥 ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) = (𝑥‘𝑧)) |
59 | 58 | elv 3438 |
. . . . . . . 8
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) = (𝑥‘𝑧) |
60 | | fveq1 6773 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤‘𝑧) = (𝑦‘𝑧)) |
61 | | fvex 6787 |
. . . . . . . . . 10
⊢ (𝑦‘𝑧) ∈ V |
62 | 60, 41, 61 | fvmpt 6875 |
. . . . . . . . 9
⊢ (𝑦 ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦) = (𝑦‘𝑧)) |
63 | 62 | elv 3438 |
. . . . . . . 8
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦) = (𝑦‘𝑧) |
64 | 59, 63 | oveq12i 7287 |
. . . . . . 7
⊢ (((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) + ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦)) = ((𝑥‘𝑧) + (𝑦‘𝑧)) |
65 | 51, 55, 64 | 3eqtr4g 2803 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = (((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) + ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦))) |
66 | 27, 65 | sylan2b 594 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = (((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) + ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦))) |
67 | | fveq1 6773 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑥) → (𝑤‘𝑧) = ((𝐹‘𝑥)‘𝑧)) |
68 | | fvex 6787 |
. . . . . . . 8
⊢ ((𝐹‘𝑥)‘𝑧) ∈ V |
69 | 67, 41, 68 | fvmpt 6875 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝐹‘𝑥)) = ((𝐹‘𝑥)‘𝑧)) |
70 | 10, 69 | ax-mp 5 |
. . . . . 6
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝐹‘𝑥)) = ((𝐹‘𝑥)‘𝑧) |
71 | 7 | adantlr 712 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))) |
72 | 71 | fveq1d 6776 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥)‘𝑧) = ((𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))‘𝑧)) |
73 | | simplr 766 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑧 ∈ 𝐴) |
74 | 4 | fvmpt2 6886 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ (𝐺‘𝑥) ∈ V) → ((𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))‘𝑧) = (𝐺‘𝑥)) |
75 | 73, 2, 74 | sylancl 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))‘𝑧) = (𝐺‘𝑥)) |
76 | 72, 75 | eqtrd 2778 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥)‘𝑧) = (𝐺‘𝑥)) |
77 | 70, 76 | eqtrid 2790 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
78 | 45, 46, 47, 66, 77 | seqhomo 13770 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(seq𝑀( ∘f + , 𝐹)‘𝑁)) = (seq𝑀( + , 𝐺)‘𝑁)) |
79 | 44, 78 | eqtr3d 2780 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧) = (seq𝑀( + , 𝐺)‘𝑁)) |
80 | 79 | mpteq2dva 5174 |
. 2
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁))) |
81 | 39, 80 | eqtrd 2778 |
1
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁))) |