Step | Hyp | Ref
| Expression |
1 | | ofrn.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | 1 | ffnd 6280 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
3 | 2 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝐹 Fn 𝐴) |
4 | | simprl 789 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝑎 ∈ 𝐴) |
5 | | fnfvelrn 6606 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) |
6 | 3, 4, 5 | syl2anc 581 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → (𝐹‘𝑎) ∈ ran 𝐹) |
7 | | ofrn.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
8 | 7 | ffnd 6280 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn 𝐴) |
9 | 8 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝐺 Fn 𝐴) |
10 | | fnfvelrn 6606 |
. . . . . 6
⊢ ((𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) |
11 | 9, 4, 10 | syl2anc 581 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → (𝐺‘𝑎) ∈ ran 𝐺) |
12 | | simprr 791 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))) |
13 | | rspceov 6952 |
. . . . 5
⊢ (((𝐹‘𝑎) ∈ ran 𝐹 ∧ (𝐺‘𝑎) ∈ ran 𝐺 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)) |
14 | 6, 11, 12, 13 | syl3anc 1496 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)) |
15 | 14 | rexlimdvaa 3242 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
16 | 15 | ss2abdv 3901 |
. 2
⊢ (𝜑 → {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))} ⊆ {𝑧 ∣ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)}) |
17 | | ofrn.4 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
18 | | inidm 4048 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
19 | | eqidd 2827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) = (𝐹‘𝑎)) |
20 | | eqidd 2827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) = (𝐺‘𝑎)) |
21 | 2, 8, 17, 17, 18, 19, 20 | offval 7165 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
22 | 21 | rneqd 5586 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) = ran (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
23 | | eqid 2826 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) |
24 | 23 | rnmpt 5605 |
. . 3
⊢ ran
(𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))} |
25 | 22, 24 | syl6eq 2878 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))}) |
26 | | ofrn.3 |
. . . . 5
⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) |
27 | 26 | ffnd 6280 |
. . . 4
⊢ (𝜑 → + Fn (𝐵 × 𝐵)) |
28 | 1 | frnd 6286 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
29 | 7 | frnd 6286 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ⊆ 𝐵) |
30 | | xpss12 5358 |
. . . . 5
⊢ ((ran
𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐵) → (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) |
31 | 28, 29, 30 | syl2anc 581 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) |
32 | | ovelimab 7073 |
. . . 4
⊢ (( + Fn (𝐵 × 𝐵) ∧ (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) → (𝑧 ∈ ( + “ (ran 𝐹 × ran 𝐺)) ↔ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
33 | 27, 31, 32 | syl2anc 581 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ( + “ (ran 𝐹 × ran 𝐺)) ↔ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
34 | 33 | abbi2dv 2948 |
. 2
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) = {𝑧 ∣ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)}) |
35 | 16, 25, 34 | 3sstr4d 3874 |
1
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) |