| Step | Hyp | Ref
| Expression |
| 1 | | i1fadd.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
| 2 | | i1ff 25711 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 4 | 3 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) |
| 5 | | i1fadd.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
| 6 | | i1ff 25711 |
. . . . . . . . 9
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
| 7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
| 8 | 7 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) |
| 9 | | reex 11246 |
. . . . . . . 8
⊢ ℝ
∈ V |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
| 11 | | inidm 4227 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
| 12 | 4, 8, 10, 10, 11 | offn 7710 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘f + 𝐺) Fn ℝ) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝐹 ∘f + 𝐺) Fn ℝ) |
| 14 | | fniniseg 7080 |
. . . . 5
⊢ ((𝐹 ∘f + 𝐺) Fn ℝ → (𝑧 ∈ (◡(𝐹 ∘f + 𝐺) “ {𝐴}) ↔ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 15 | 13, 14 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝑧 ∈ (◡(𝐹 ∘f + 𝐺) “ {𝐴}) ↔ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 16 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝐺 Fn ℝ) |
| 17 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝑧 ∈ ℝ) |
| 18 | | fnfvelrn 7100 |
. . . . . . . 8
⊢ ((𝐺 Fn ℝ ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) ∈ ran 𝐺) |
| 19 | 16, 17, 18 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝐺‘𝑧) ∈ ran 𝐺) |
| 20 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴) |
| 21 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
| 22 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
| 23 | 4, 8, 10, 10, 11, 21, 22 | ofval 7708 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ((𝐹 ∘f + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧))) |
| 24 | 23 | ad2ant2r 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → ((𝐹 ∘f + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧))) |
| 25 | 20, 24 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝐴 = ((𝐹‘𝑧) + (𝐺‘𝑧))) |
| 26 | 25 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝐴 − (𝐺‘𝑧)) = (((𝐹‘𝑧) + (𝐺‘𝑧)) − (𝐺‘𝑧))) |
| 27 | | ax-resscn 11212 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
| 28 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶ℝ ∧
ℝ ⊆ ℂ) → 𝐹:ℝ⟶ℂ) |
| 29 | 3, 27, 28 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝐹:ℝ⟶ℂ) |
| 31 | 30, 17 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝐹‘𝑧) ∈ ℂ) |
| 32 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℝ⟶ℝ ∧
ℝ ⊆ ℂ) → 𝐺:ℝ⟶ℂ) |
| 33 | 7, 27, 32 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:ℝ⟶ℂ) |
| 34 | 33 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝐺:ℝ⟶ℂ) |
| 35 | 34, 17 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝐺‘𝑧) ∈ ℂ) |
| 36 | 31, 35 | pncand 11621 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (((𝐹‘𝑧) + (𝐺‘𝑧)) − (𝐺‘𝑧)) = (𝐹‘𝑧)) |
| 37 | 26, 36 | eqtr2d 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝐹‘𝑧) = (𝐴 − (𝐺‘𝑧))) |
| 38 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝐹 Fn ℝ) |
| 39 | | fniniseg 7080 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐴 − (𝐺‘𝑧))}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − (𝐺‘𝑧))))) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝑧 ∈ (◡𝐹 “ {(𝐴 − (𝐺‘𝑧))}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − (𝐺‘𝑧))))) |
| 41 | 17, 37, 40 | mpbir2and 713 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝑧 ∈ (◡𝐹 “ {(𝐴 − (𝐺‘𝑧))})) |
| 42 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
| 43 | | fniniseg 7080 |
. . . . . . . . . 10
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = (𝐺‘𝑧)))) |
| 44 | 16, 43 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → (𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = (𝐺‘𝑧)))) |
| 45 | 17, 42, 44 | mpbir2and 713 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)})) |
| 46 | 41, 45 | elind 4200 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → 𝑧 ∈ ((◡𝐹 “ {(𝐴 − (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) |
| 47 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐺‘𝑧) → (𝐴 − 𝑦) = (𝐴 − (𝐺‘𝑧))) |
| 48 | 47 | sneqd 4638 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘𝑧) → {(𝐴 − 𝑦)} = {(𝐴 − (𝐺‘𝑧))}) |
| 49 | 48 | imaeq2d 6078 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (◡𝐹 “ {(𝐴 − 𝑦)}) = (◡𝐹 “ {(𝐴 − (𝐺‘𝑧))})) |
| 50 | | sneq 4636 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘𝑧) → {𝑦} = {(𝐺‘𝑧)}) |
| 51 | 50 | imaeq2d 6078 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (◡𝐺 “ {𝑦}) = (◡𝐺 “ {(𝐺‘𝑧)})) |
| 52 | 49, 51 | ineq12d 4221 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})) = ((◡𝐹 “ {(𝐴 − (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) |
| 53 | 52 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ 𝑧 ∈ ((◡𝐹 “ {(𝐴 − (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)})))) |
| 54 | 53 | rspcev 3622 |
. . . . . . 7
⊢ (((𝐺‘𝑧) ∈ ran 𝐺 ∧ 𝑧 ∈ ((◡𝐹 “ {(𝐴 − (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) → ∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |
| 55 | 19, 46, 54 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) → ∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |
| 56 | 55 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴) → ∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
| 57 | | elin 3967 |
. . . . . . 7
⊢ (𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ (◡𝐹 “ {(𝐴 − 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦}))) |
| 58 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → 𝐹 Fn ℝ) |
| 59 | | fniniseg 7080 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐴 − 𝑦)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − 𝑦)))) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝑧 ∈ (◡𝐹 “ {(𝐴 − 𝑦)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − 𝑦)))) |
| 61 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → 𝐺 Fn ℝ) |
| 62 | | fniniseg 7080 |
. . . . . . . . . 10
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
| 64 | 60, 63 | anbi12d 632 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((𝑧 ∈ (◡𝐹 “ {(𝐴 − 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦})) ↔ ((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦)))) |
| 65 | | anandi 676 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦)) ↔ ((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
| 66 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → 𝑧 ∈ ℝ) |
| 67 | 23 | ad2ant2r 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → ((𝐹 ∘f + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧))) |
| 68 | | simprrl 781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → (𝐹‘𝑧) = (𝐴 − 𝑦)) |
| 69 | | simprrr 782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → (𝐺‘𝑧) = 𝑦) |
| 70 | 68, 69 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → ((𝐹‘𝑧) + (𝐺‘𝑧)) = ((𝐴 − 𝑦) + 𝑦)) |
| 71 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → 𝐴 ∈ ℂ) |
| 72 | 33 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → 𝐺:ℝ⟶ℂ) |
| 73 | 72, 66 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → (𝐺‘𝑧) ∈ ℂ) |
| 74 | 69, 73 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → 𝑦 ∈ ℂ) |
| 75 | 71, 74 | npcand 11624 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → ((𝐴 − 𝑦) + 𝑦) = 𝐴) |
| 76 | 67, 70, 75 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴) |
| 77 | 66, 76 | jca 511 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦))) → (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴)) |
| 78 | 77 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 − 𝑦) ∧ (𝐺‘𝑧) = 𝑦)) → (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 79 | 65, 78 | biimtrrid 243 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 − 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦)) → (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 80 | 64, 79 | sylbid 240 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((𝑧 ∈ (◡𝐹 “ {(𝐴 − 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 81 | 57, 80 | biimtrid 242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 82 | 81 | rexlimdvw 3160 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴))) |
| 83 | 56, 82 | impbid 212 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((𝑧 ∈ ℝ ∧ ((𝐹 ∘f + 𝐺)‘𝑧) = 𝐴) ↔ ∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
| 84 | 15, 83 | bitrd 279 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝑧 ∈ (◡(𝐹 ∘f + 𝐺) “ {𝐴}) ↔ ∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
| 85 | | eliun 4995 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ ∃𝑦 ∈ ran 𝐺 𝑧 ∈ ((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |
| 86 | 84, 85 | bitr4di 289 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝑧 ∈ (◡(𝐹 ∘f + 𝐺) “ {𝐴}) ↔ 𝑧 ∈ ∪
𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
| 87 | 86 | eqrdv 2735 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝐴}) = ∪
𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |