Step | Hyp | Ref
| Expression |
1 | | ofrn.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝐹 Fn 𝐴) |
5 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝑎 ∈ 𝐴) |
6 | | fnfvelrn 6264 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) |
7 | 4, 5, 6 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → (𝐹‘𝑎) ∈ ran 𝐹) |
8 | | ofrn.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
9 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn 𝐴) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝐺 Fn 𝐴) |
12 | | fnfvelrn 6264 |
. . . . . 6
⊢ ((𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) |
13 | 11, 5, 12 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → (𝐺‘𝑎) ∈ ran 𝐺) |
14 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))) |
15 | | rspceov 6590 |
. . . . 5
⊢ (((𝐹‘𝑎) ∈ ran 𝐹 ∧ (𝐺‘𝑎) ∈ ran 𝐺 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)) |
16 | 7, 13, 14, 15 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)))) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)) |
17 | 16 | rexlimdvaa 3014 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎)) → ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
18 | 17 | ss2abdv 3638 |
. 2
⊢ (𝜑 → {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))} ⊆ {𝑧 ∣ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)}) |
19 | | ofrn.4 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
20 | | inidm 3784 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
21 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) = (𝐹‘𝑎)) |
22 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) = (𝐺‘𝑎)) |
23 | 3, 10, 19, 19, 20, 21, 22 | offval 6802 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
24 | 23 | rneqd 5274 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) = ran (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
25 | | eqid 2610 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) |
26 | 25 | rnmpt 5292 |
. . 3
⊢ ran
(𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))} |
27 | 24, 26 | syl6eq 2660 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = ((𝐹‘𝑎) + (𝐺‘𝑎))}) |
28 | | ofrn.3 |
. . . . 5
⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) |
29 | | ffn 5958 |
. . . . 5
⊢ ( + :(𝐵 × 𝐵)⟶𝐶 → + Fn (𝐵 × 𝐵)) |
30 | 28, 29 | syl 17 |
. . . 4
⊢ (𝜑 → + Fn (𝐵 × 𝐵)) |
31 | | frn 5966 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
32 | 1, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
33 | | frn 5966 |
. . . . . 6
⊢ (𝐺:𝐴⟶𝐵 → ran 𝐺 ⊆ 𝐵) |
34 | 8, 33 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ⊆ 𝐵) |
35 | | xpss12 5148 |
. . . . 5
⊢ ((ran
𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐵) → (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) |
36 | 32, 34, 35 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) |
37 | | ovelimab 6710 |
. . . 4
⊢ (( + Fn (𝐵 × 𝐵) ∧ (ran 𝐹 × ran 𝐺) ⊆ (𝐵 × 𝐵)) → (𝑧 ∈ ( + “ (ran 𝐹 × ran 𝐺)) ↔ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
38 | 30, 36, 37 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ( + “ (ran 𝐹 × ran 𝐺)) ↔ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦))) |
39 | 38 | abbi2dv 2729 |
. 2
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) = {𝑧 ∣ ∃𝑥 ∈ ran 𝐹∃𝑦 ∈ ran 𝐺 𝑧 = (𝑥 + 𝑦)}) |
40 | 18, 27, 39 | 3sstr4d 3611 |
1
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) |