| 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 8143 | . . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐻 ∘ 𝑆) = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) | 
| 4 | 3 | coeq2d 5873 | . . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → ( + ∘ (𝐻 ∘ 𝑆)) = ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉))) | 
| 5 | 4 | 3ad2ant1 1134 | . 2
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝐻 ∘ 𝑆)) = ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉))) | 
| 6 |  | dffn3 6748 | . . . . . . 7
⊢ ( + Fn 𝐶 ↔ + :𝐶⟶ran + ) | 
| 7 | 6 | biimpi 216 | . . . . . 6
⊢ ( + Fn 𝐶 → + :𝐶⟶ran + ) | 
| 8 | 7 | adantr 480 | . . . . 5
⊢ (( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶) → + :𝐶⟶ran + ) | 
| 9 | 8 | 3ad2ant3 1136 | . . . 4
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → + :𝐶⟶ran + ) | 
| 10 |  | simpl3r 1230 | . . . . 5
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → (ran 𝐹 × ran 𝐺) ⊆ 𝐶) | 
| 11 |  | simp1l 1198 | . . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → 𝐹 Fn 𝐴) | 
| 12 |  | fnfvelrn 7100 | . . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) | 
| 13 | 11, 12 | sylan 580 | . . . . . 6
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ran 𝐹) | 
| 14 |  | simp1r 1199 | . . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → 𝐺 Fn 𝐴) | 
| 15 |  | fnfvelrn 7100 | . . . . . . 7
⊢ ((𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) | 
| 16 | 14, 15 | sylan 580 | . . . . . 6
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ ran 𝐺) | 
| 17 | 13, 16 | opelxpd 5724 | . . . . 5
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ (ran 𝐹 × ran 𝐺)) | 
| 18 | 10, 17 | sseldd 3984 | . . . 4
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) ∧ 𝑎 ∈ 𝐴) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ 𝐶) | 
| 19 | 9, 18 | cofmpt 7152 | . . 3
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) = (𝑎 ∈ 𝐴 ↦ ( + ‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉))) | 
| 20 |  | df-ov 7434 | . . . . 5
⊢ ((𝐹‘𝑎) + (𝐺‘𝑎)) = ( + ‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉) | 
| 21 | 20 | eqcomi 2746 | . . . 4
⊢ ( +
‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉) = ((𝐹‘𝑎) + (𝐺‘𝑎)) | 
| 22 | 21 | mpteq2i 5247 | . . 3
⊢ (𝑎 ∈ 𝐴 ↦ ( + ‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) | 
| 23 | 19, 22 | eqtrdi 2793 | . 2
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) | 
| 24 |  | offval3 8007 | . . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f + 𝐺) = (𝑎 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) | 
| 25 |  | fndm 6671 | . . . . . . . 8
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | 
| 26 |  | fndm 6671 | . . . . . . . 8
⊢ (𝐺 Fn 𝐴 → dom 𝐺 = 𝐴) | 
| 27 | 25, 26 | ineqan12d 4222 | . . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐴)) | 
| 28 |  | inidm 4227 | . . . . . . 7
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 29 | 27, 28 | eqtrdi 2793 | . . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom 𝐹 ∩ dom 𝐺) = 𝐴) | 
| 30 | 29 | mpteq1d 5237 | . . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝑎 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) | 
| 31 | 24, 30 | sylan9eqr 2799 | . . . 4
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐹 ∘f + 𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎)))) | 
| 32 | 31 | eqcomd 2743 | . . 3
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝐹 ∘f + 𝐺)) | 
| 33 | 32 | 3adant3 1133 | . 2
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎) + (𝐺‘𝑎))) = (𝐹 ∘f + 𝐺)) | 
| 34 | 5, 23, 33 | 3eqtrd 2781 | 1
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝐻 ∘ 𝑆)) = (𝐹 ∘f + 𝐺)) |