Step | Hyp | Ref
| Expression |
1 | | fsplitfpar.h |
. . . . 5
⊢ 𝐻 = ((◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V))))) |
2 | | fsplitfpar.s |
. . . . 5
⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴) |
3 | 1, 2 | fsplitfpar 7959 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐻 ∘ 𝑆) = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
4 | 3 | coeq2d 5771 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → ( + ∘ (𝐻 ∘ 𝑆)) = ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉))) |
5 | 4 | 3ad2ant1 1132 |
. 2
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝐻 ∘ 𝑆)) = ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉))) |
6 | | dffn3 6613 |
. . . . . . 7
⊢ ( + Fn 𝐶 ↔ + :𝐶⟶ran + ) |
7 | 6 | biimpi 215 |
. . . . . 6
⊢ ( + Fn 𝐶 → + :𝐶⟶ran + ) |
8 | 7 | adantr 481 |
. . . . 5
⊢ (( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶) → + :𝐶⟶ran + ) |
9 | 8 | 3ad2ant3 1134 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → + :𝐶⟶ran + ) |
10 | | simpl3r 1228 |
. . . . 5
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → (ran 𝐹 × ran 𝐺) ⊆ 𝐶) |
11 | | simp1l 1196 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → 𝐹 Fn 𝐴) |
12 | | fnfvelrn 6958 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) |
13 | 11, 12 | sylan 580 |
. . . . . 6
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) |
14 | | simp1r 1197 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → 𝐺 Fn 𝐴) |
15 | | fnfvelrn 6958 |
. . . . . . 7
⊢ ((𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) |
16 | 14, 15 | sylan 580 |
. . . . . 6
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) |
17 | 13, 16 | opelxpd 5627 |
. . . . 5
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ (ran 𝐹 × ran 𝐺)) |
18 | 10, 17 | sseldd 3922 |
. . . 4
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ 𝐶) |
19 | 9, 18 | cofmpt 7004 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) = (𝑎 ∈ 𝐴 ↦ ( + ‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉))) |
20 | | df-ov 7278 |
. . . . 5
⊢ ((𝐹‘𝑎) + (𝐺‘𝑎)) = ( + ‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉) |
21 | 20 | eqcomi 2747 |
. . . 4
⊢ ( +
‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉) = ((𝐹‘𝑎) + (𝐺‘𝑎)) |
22 | 21 | mpteq2i 5179 |
. . 3
⊢ (𝑎 ∈ 𝐴 ↦ ( + ‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) |
23 | 19, 22 | eqtrdi 2794 |
. 2
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
24 | | offval3 7825 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f + 𝐺) = (𝑎 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
25 | | fndm 6536 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
26 | | fndm 6536 |
. . . . . . . 8
⊢ (𝐺 Fn 𝐴 → dom 𝐺 = 𝐴) |
27 | 25, 26 | ineqan12d 4148 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐴)) |
28 | | inidm 4152 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
29 | 27, 28 | eqtrdi 2794 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom 𝐹 ∩ dom 𝐺) = 𝐴) |
30 | 29 | mpteq1d 5169 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝑎 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
31 | 24, 30 | sylan9eqr 2800 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐹 ∘f + 𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) |
32 | 31 | eqcomd 2744 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝐹 ∘f + 𝐺)) |
33 | 32 | 3adant3 1131 |
. 2
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝐹 ∘f + 𝐺)) |
34 | 5, 23, 33 | 3eqtrd 2782 |
1
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝐻 ∘ 𝑆)) = (𝐹 ∘f + 𝐺)) |