Step | Hyp | Ref
| Expression |
1 | | ofrn.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | 1 | ffnd 6567 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
3 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝑎 ∈ 𝐴) |
4 | | fnfvelrn 6922 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) |
5 | 2, 3, 4 | syl2an2r 685 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → (𝐹‘𝑎) ∈ ran 𝐹) |
6 | | ofrn.2 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
7 | 6 | ffnd 6567 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn 𝐴) |
8 | | fnfvelrn 6922 |
. . . . . 6
⊢ ((𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) |
9 | 7, 3, 8 | syl2an2r 685 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → (𝐺‘𝑎) ∈ ran 𝐺) |
10 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))) |
11 | | rspceov 7281 |
. . . . 5
⊢ (((𝐹‘𝑎) ∈ ran 𝐹 ∧ (𝐺‘𝑎) ∈ ran 𝐺 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)) |
12 | 5, 9, 10, 11 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)) |
13 | 12 | rexlimdvaa 3213 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
14 | 13 | ss2abdv 3993 |
. 2
⊢ (𝜑 → {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))} ⊆ {𝑧 ∣ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)}) |
15 | | ofrn.4 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
16 | | inidm 4149 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
17 | | eqidd 2740 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) = (𝐹‘𝑎)) |
18 | | eqidd 2740 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) = (𝐺‘𝑎)) |
19 | 2, 7, 15, 15, 16, 17, 18 | offval 7498 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f + 𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
20 | 19 | rneqd 5824 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) = ran (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
21 | | eqid 2739 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) |
22 | 21 | rnmpt 5841 |
. . 3
⊢ ran
(𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))} |
23 | 20, 22 | eqtrdi 2796 |
. 2
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))}) |
24 | | ofrn.3 |
. . . . 5
⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) |
25 | 24 | ffnd 6567 |
. . . 4
⊢ (𝜑 → + Fn (𝐵 × 𝐵)) |
26 | 1 | frnd 6574 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
27 | 6 | frnd 6574 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ⊆ 𝐵) |
28 | | xpss12 5583 |
. . . . 5
⊢ ((ran
𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐵) → (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) |
29 | 26, 27, 28 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) |
30 | | ovelimab 7407 |
. . . 4
⊢ (( + Fn (𝐵 × 𝐵) ∧ (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) → (𝑧 ∈ ( + “ (ran 𝐹 × ran 𝐺)) ↔ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
31 | 25, 29, 30 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ( + “ (ran 𝐹 × ran 𝐺)) ↔ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
32 | 31 | abbi2dv 2876 |
. 2
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) = {𝑧 ∣ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)}) |
33 | 14, 23, 32 | 3sstr4d 3964 |
1
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) |