| Step | Hyp | Ref
| Expression |
| 1 | | df-ov 7434 |
. 2
⊢ (𝑋( + ∘ 𝐻)𝑌) = (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) |
| 2 | | sqrtf 15402 |
. . . . . . . . 9
⊢
√:ℂ⟶ℂ |
| 3 | | ffn 6736 |
. . . . . . . . 9
⊢
(√:ℂ⟶ℂ → √ Fn
ℂ) |
| 4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
⊢ √
Fn ℂ |
| 5 | | rge0ssre 13496 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
| 6 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 7 | 5, 6 | sstri 3993 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℂ |
| 8 | | fnssres 6691 |
. . . . . . . . 9
⊢ ((√
Fn ℂ ∧ (0[,)+∞) ⊆ ℂ) → (√ ↾
(0[,)+∞)) Fn (0[,)+∞)) |
| 9 | | ex-fpar.a |
. . . . . . . . . . 11
⊢ 𝐴 =
(0[,)+∞) |
| 10 | 9 | reseq2i 5994 |
. . . . . . . . . 10
⊢ (√
↾ 𝐴) = (√
↾ (0[,)+∞)) |
| 11 | 10 | fneq1i 6665 |
. . . . . . . . 9
⊢ ((√
↾ 𝐴) Fn
(0[,)+∞) ↔ (√ ↾ (0[,)+∞)) Fn
(0[,)+∞)) |
| 12 | 8, 11 | sylibr 234 |
. . . . . . . 8
⊢ ((√
Fn ℂ ∧ (0[,)+∞) ⊆ ℂ) → (√ ↾ 𝐴) Fn
(0[,)+∞)) |
| 13 | 4, 7, 12 | mp2an 692 |
. . . . . . 7
⊢ (√
↾ 𝐴) Fn
(0[,)+∞) |
| 14 | | ex-fpar.f |
. . . . . . . 8
⊢ 𝐹 = (√ ↾ 𝐴) |
| 15 | | id 22 |
. . . . . . . . 9
⊢ (𝐹 = (√ ↾ 𝐴) → 𝐹 = (√ ↾ 𝐴)) |
| 16 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 = (√ ↾ 𝐴) → 𝐴 = (0[,)+∞)) |
| 17 | 15, 16 | fneq12d 6663 |
. . . . . . . 8
⊢ (𝐹 = (√ ↾ 𝐴) → (𝐹 Fn 𝐴 ↔ (√ ↾ 𝐴) Fn (0[,)+∞))) |
| 18 | 14, 17 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 ↔ (√ ↾ 𝐴) Fn (0[,)+∞)) |
| 19 | 13, 18 | mpbir 231 |
. . . . . 6
⊢ 𝐹 Fn 𝐴 |
| 20 | | sinf 16160 |
. . . . . . . . 9
⊢
sin:ℂ⟶ℂ |
| 21 | | ffn 6736 |
. . . . . . . . 9
⊢
(sin:ℂ⟶ℂ → sin Fn ℂ) |
| 22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
⊢ sin Fn
ℂ |
| 23 | | fnssres 6691 |
. . . . . . . . 9
⊢ ((sin Fn
ℂ ∧ ℝ ⊆ ℂ) → (sin ↾ ℝ) Fn
ℝ) |
| 24 | | ex-fpar.b |
. . . . . . . . . . 11
⊢ 𝐵 = ℝ |
| 25 | 24 | reseq2i 5994 |
. . . . . . . . . 10
⊢ (sin
↾ 𝐵) = (sin ↾
ℝ) |
| 26 | 25 | fneq1i 6665 |
. . . . . . . . 9
⊢ ((sin
↾ 𝐵) Fn ℝ
↔ (sin ↾ ℝ) Fn ℝ) |
| 27 | 23, 26 | sylibr 234 |
. . . . . . . 8
⊢ ((sin Fn
ℂ ∧ ℝ ⊆ ℂ) → (sin ↾ 𝐵) Fn ℝ) |
| 28 | 22, 6, 27 | mp2an 692 |
. . . . . . 7
⊢ (sin
↾ 𝐵) Fn
ℝ |
| 29 | | ex-fpar.g |
. . . . . . . 8
⊢ 𝐺 = (sin ↾ 𝐵) |
| 30 | | id 22 |
. . . . . . . . 9
⊢ (𝐺 = (sin ↾ 𝐵) → 𝐺 = (sin ↾ 𝐵)) |
| 31 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 = (sin ↾ 𝐵) → 𝐵 = ℝ) |
| 32 | 30, 31 | fneq12d 6663 |
. . . . . . . 8
⊢ (𝐺 = (sin ↾ 𝐵) → (𝐺 Fn 𝐵 ↔ (sin ↾ 𝐵) Fn ℝ)) |
| 33 | 29, 32 | ax-mp 5 |
. . . . . . 7
⊢ (𝐺 Fn 𝐵 ↔ (sin ↾ 𝐵) Fn ℝ) |
| 34 | 28, 33 | mpbir 231 |
. . . . . 6
⊢ 𝐺 Fn 𝐵 |
| 35 | | ex-fpar.h |
. . . . . . 7
⊢ 𝐻 = ((◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V))))) |
| 36 | 35 | fpar 8141 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉)) |
| 37 | 19, 34, 36 | mp2an 692 |
. . . . 5
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) |
| 38 | | opex 5469 |
. . . . 5
⊢
〈(𝐹‘𝑥), (𝐺‘𝑦)〉 ∈ V |
| 39 | 37, 38 | fnmpoi 8095 |
. . . 4
⊢ 𝐻 Fn (𝐴 × 𝐵) |
| 40 | | opelxpi 5722 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
| 41 | | fvco2 7006 |
. . . 4
⊢ ((𝐻 Fn (𝐴 × 𝐵) ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) → (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) = ( + ‘(𝐻‘〈𝑋, 𝑌〉))) |
| 42 | 39, 40, 41 | sylancr 587 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) = ( + ‘(𝐻‘〈𝑋, 𝑌〉))) |
| 43 | | simpl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐴) |
| 44 | | simpr 484 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
| 45 | 37, 43, 44 | fvproj 8159 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐻‘〈𝑋, 𝑌〉) = 〈(𝐹‘𝑋), (𝐺‘𝑌)〉) |
| 46 | 45 | fveq2d 6910 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ( + ‘(𝐻‘〈𝑋, 𝑌〉)) = ( + ‘〈(𝐹‘𝑋), (𝐺‘𝑌)〉)) |
| 47 | | df-ov 7434 |
. . . 4
⊢ ((𝐹‘𝑋) + (𝐺‘𝑌)) = ( + ‘〈(𝐹‘𝑋), (𝐺‘𝑌)〉) |
| 48 | 14 | fveq1i 6907 |
. . . . . 6
⊢ (𝐹‘𝑋) = ((√ ↾ 𝐴)‘𝑋) |
| 49 | | fvres 6925 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → ((√ ↾ 𝐴)‘𝑋) = (√‘𝑋)) |
| 50 | 48, 49 | eqtrid 2789 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝐹‘𝑋) = (√‘𝑋)) |
| 51 | 29 | fveq1i 6907 |
. . . . . 6
⊢ (𝐺‘𝑌) = ((sin ↾ 𝐵)‘𝑌) |
| 52 | | fvres 6925 |
. . . . . 6
⊢ (𝑌 ∈ 𝐵 → ((sin ↾ 𝐵)‘𝑌) = (sin‘𝑌)) |
| 53 | 51, 52 | eqtrid 2789 |
. . . . 5
⊢ (𝑌 ∈ 𝐵 → (𝐺‘𝑌) = (sin‘𝑌)) |
| 54 | 50, 53 | oveqan12d 7450 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝐹‘𝑋) + (𝐺‘𝑌)) = ((√‘𝑋) + (sin‘𝑌))) |
| 55 | 47, 54 | eqtr3id 2791 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ( + ‘〈(𝐹‘𝑋), (𝐺‘𝑌)〉) = ((√‘𝑋) + (sin‘𝑌))) |
| 56 | 42, 46, 55 | 3eqtrd 2781 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) = ((√‘𝑋) + (sin‘𝑌))) |
| 57 | 1, 56 | eqtrid 2789 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋( + ∘ 𝐻)𝑌) = ((√‘𝑋) + (sin‘𝑌))) |