| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | seqof.2 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 2 |  | fvex 6919 | . . . . . . . . 9
⊢ (𝐺‘𝑥) ∈ V | 
| 3 | 2 | rgenw 3065 | . . . . . . . 8
⊢
∀𝑧 ∈
𝐴 (𝐺‘𝑥) ∈ V | 
| 4 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) | 
| 5 | 4 | fnmpt 6708 | . . . . . . . 8
⊢
(∀𝑧 ∈
𝐴 (𝐺‘𝑥) ∈ V → (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) Fn 𝐴) | 
| 6 | 3, 5 | mp1i 13 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) Fn 𝐴) | 
| 7 |  | seqof.3 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))) | 
| 8 | 7 | fneq1d 6661 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) Fn 𝐴 ↔ (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)) Fn 𝐴)) | 
| 9 | 6, 8 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) Fn 𝐴) | 
| 10 |  | fvex 6919 | . . . . . . 7
⊢ (𝐹‘𝑥) ∈ V | 
| 11 |  | fneq1 6659 | . . . . . . 7
⊢ (𝑧 = (𝐹‘𝑥) → (𝑧 Fn 𝐴 ↔ (𝐹‘𝑥) Fn 𝐴)) | 
| 12 | 10, 11 | elab 3679 | . . . . . 6
⊢ ((𝐹‘𝑥) ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ (𝐹‘𝑥) Fn 𝐴) | 
| 13 | 9, 12 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) | 
| 14 |  | simprl 771 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → 𝑥 Fn 𝐴) | 
| 15 |  | simprr 773 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → 𝑦 Fn 𝐴) | 
| 16 |  | seqof.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → 𝐴 ∈ 𝑉) | 
| 18 |  | inidm 4227 | . . . . . . . . 9
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 19 | 14, 15, 17, 17, 18 | offn 7710 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → (𝑥 ∘f + 𝑦) Fn 𝐴) | 
| 20 | 19 | ex 412 | . . . . . . 7
⊢ (𝜑 → ((𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴) → (𝑥 ∘f + 𝑦) Fn 𝐴)) | 
| 21 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 22 |  | fneq1 6659 | . . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧 Fn 𝐴 ↔ 𝑥 Fn 𝐴)) | 
| 23 | 21, 22 | elab 3679 | . . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ 𝑥 Fn 𝐴) | 
| 24 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑦 ∈ V | 
| 25 |  | fneq1 6659 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 Fn 𝐴 ↔ 𝑦 Fn 𝐴)) | 
| 26 | 24, 25 | elab 3679 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ 𝑦 Fn 𝐴) | 
| 27 | 23, 26 | anbi12i 628 | . . . . . . 7
⊢ ((𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) ↔ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) | 
| 28 |  | ovex 7464 | . . . . . . . 8
⊢ (𝑥 ∘f + 𝑦) ∈ V | 
| 29 |  | fneq1 6659 | . . . . . . . 8
⊢ (𝑧 = (𝑥 ∘f + 𝑦) → (𝑧 Fn 𝐴 ↔ (𝑥 ∘f + 𝑦) Fn 𝐴)) | 
| 30 | 28, 29 | elab 3679 | . . . . . . 7
⊢ ((𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ (𝑥 ∘f + 𝑦) Fn 𝐴) | 
| 31 | 20, 27, 30 | 3imtr4g 296 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) → (𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) | 
| 32 | 31 | imp 406 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) → (𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) | 
| 33 | 1, 13, 32 | seqcl 14063 | . . . 4
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) | 
| 34 |  | fvex 6919 | . . . . 5
⊢ (seq𝑀( ∘f + , 𝐹)‘𝑁) ∈ V | 
| 35 |  | fneq1 6659 | . . . . 5
⊢ (𝑧 = (seq𝑀( ∘f + , 𝐹)‘𝑁) → (𝑧 Fn 𝐴 ↔ (seq𝑀( ∘f + , 𝐹)‘𝑁) Fn 𝐴)) | 
| 36 | 34, 35 | elab 3679 | . . . 4
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁) ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ↔ (seq𝑀( ∘f + , 𝐹)‘𝑁) Fn 𝐴) | 
| 37 | 33, 36 | sylib 218 | . . 3
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) Fn 𝐴) | 
| 38 |  | dffn5 6967 | . . 3
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁) Fn 𝐴 ↔ (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧))) | 
| 39 | 37, 38 | sylib 218 | . 2
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧))) | 
| 40 |  | fveq1 6905 | . . . . . 6
⊢ (𝑤 = (seq𝑀( ∘f + , 𝐹)‘𝑁) → (𝑤‘𝑧) = ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) | 
| 41 |  | eqid 2737 | . . . . . 6
⊢ (𝑤 ∈ V ↦ (𝑤‘𝑧)) = (𝑤 ∈ V ↦ (𝑤‘𝑧)) | 
| 42 |  | fvex 6919 | . . . . . 6
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁)‘𝑧) ∈ V | 
| 43 | 40, 41, 42 | fvmpt 7016 | . . . . 5
⊢
((seq𝑀(
∘f + , 𝐹)‘𝑁) ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(seq𝑀( ∘f + , 𝐹)‘𝑁)) = ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) | 
| 44 | 34, 43 | mp1i 13 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(seq𝑀( ∘f + , 𝐹)‘𝑁)) = ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) | 
| 45 | 32 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) → (𝑥 ∘f + 𝑦) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) | 
| 46 | 13 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ {𝑧 ∣ 𝑧 Fn 𝐴}) | 
| 47 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 48 |  | eqidd 2738 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑥‘𝑧) = (𝑥‘𝑧)) | 
| 49 |  | eqidd 2738 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑦‘𝑧) = (𝑦‘𝑧)) | 
| 50 | 14, 15, 17, 17, 18, 48, 49 | ofval 7708 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∘f + 𝑦)‘𝑧) = ((𝑥‘𝑧) + (𝑦‘𝑧))) | 
| 51 | 50 | an32s 652 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → ((𝑥 ∘f + 𝑦)‘𝑧) = ((𝑥‘𝑧) + (𝑦‘𝑧))) | 
| 52 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑤 = (𝑥 ∘f + 𝑦) → (𝑤‘𝑧) = ((𝑥 ∘f + 𝑦)‘𝑧)) | 
| 53 |  | fvex 6919 | . . . . . . . . 9
⊢ ((𝑥 ∘f + 𝑦)‘𝑧) ∈ V | 
| 54 | 52, 41, 53 | fvmpt 7016 | . . . . . . . 8
⊢ ((𝑥 ∘f + 𝑦) ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = ((𝑥 ∘f + 𝑦)‘𝑧)) | 
| 55 | 28, 54 | ax-mp 5 | . . . . . . 7
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = ((𝑥 ∘f + 𝑦)‘𝑧) | 
| 56 |  | fveq1 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤‘𝑧) = (𝑥‘𝑧)) | 
| 57 |  | fvex 6919 | . . . . . . . . . 10
⊢ (𝑥‘𝑧) ∈ V | 
| 58 | 56, 41, 57 | fvmpt 7016 | . . . . . . . . 9
⊢ (𝑥 ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) = (𝑥‘𝑧)) | 
| 59 | 58 | elv 3485 | . . . . . . . 8
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) = (𝑥‘𝑧) | 
| 60 |  | fveq1 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤‘𝑧) = (𝑦‘𝑧)) | 
| 61 |  | fvex 6919 | . . . . . . . . . 10
⊢ (𝑦‘𝑧) ∈ V | 
| 62 | 60, 41, 61 | fvmpt 7016 | . . . . . . . . 9
⊢ (𝑦 ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦) = (𝑦‘𝑧)) | 
| 63 | 62 | elv 3485 | . . . . . . . 8
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦) = (𝑦‘𝑧) | 
| 64 | 59, 63 | oveq12i 7443 | . . . . . . 7
⊢ (((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) + ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦)) = ((𝑥‘𝑧) + (𝑦‘𝑧)) | 
| 65 | 51, 55, 64 | 3eqtr4g 2802 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴)) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = (((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) + ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦))) | 
| 66 | 27, 65 | sylan2b 594 | . . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ {𝑧 ∣ 𝑧 Fn 𝐴} ∧ 𝑦 ∈ {𝑧 ∣ 𝑧 Fn 𝐴})) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝑥 ∘f + 𝑦)) = (((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑥) + ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘𝑦))) | 
| 67 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑥) → (𝑤‘𝑧) = ((𝐹‘𝑥)‘𝑧)) | 
| 68 |  | fvex 6919 | . . . . . . . 8
⊢ ((𝐹‘𝑥)‘𝑧) ∈ V | 
| 69 | 67, 41, 68 | fvmpt 7016 | . . . . . . 7
⊢ ((𝐹‘𝑥) ∈ V → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝐹‘𝑥)) = ((𝐹‘𝑥)‘𝑧)) | 
| 70 | 10, 69 | ax-mp 5 | . . . . . 6
⊢ ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝐹‘𝑥)) = ((𝐹‘𝑥)‘𝑧) | 
| 71 | 7 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))) | 
| 72 | 71 | fveq1d 6908 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥)‘𝑧) = ((𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))‘𝑧)) | 
| 73 |  | simplr 769 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑧 ∈ 𝐴) | 
| 74 | 4 | fvmpt2 7027 | . . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ (𝐺‘𝑥) ∈ V) → ((𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))‘𝑧) = (𝐺‘𝑥)) | 
| 75 | 73, 2, 74 | sylancl 586 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))‘𝑧) = (𝐺‘𝑥)) | 
| 76 | 72, 75 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥)‘𝑧) = (𝐺‘𝑥)) | 
| 77 | 70, 76 | eqtrid 2789 | . . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(𝐹‘𝑥)) = (𝐺‘𝑥)) | 
| 78 | 45, 46, 47, 66, 77 | seqhomo 14090 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝑤 ∈ V ↦ (𝑤‘𝑧))‘(seq𝑀( ∘f + , 𝐹)‘𝑁)) = (seq𝑀( + , 𝐺)‘𝑁)) | 
| 79 | 44, 78 | eqtr3d 2779 | . . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧) = (seq𝑀( + , 𝐺)‘𝑁)) | 
| 80 | 79 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ ((seq𝑀( ∘f + , 𝐹)‘𝑁)‘𝑧)) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁))) | 
| 81 | 39, 80 | eqtrd 2777 | 1
⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁))) |