Step | Hyp | Ref
| Expression |
1 | | df-ov 7173 |
. 2
⊢ (𝑋( + ∘ 𝐻)𝑌) = (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) |
2 | | sqrtf 14813 |
. . . . . . . . 9
⊢
√:ℂ⟶ℂ |
3 | | ffn 6504 |
. . . . . . . . 9
⊢
(√:ℂ⟶ℂ → √ Fn
ℂ) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
⊢ √
Fn ℂ |
5 | | rge0ssre 12930 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
6 | | ax-resscn 10672 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
7 | 5, 6 | sstri 3886 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℂ |
8 | | fnssres 6459 |
. . . . . . . . 9
⊢ ((√
Fn ℂ ∧ (0[,)+∞) ⊆ ℂ) → (√ ↾
(0[,)+∞)) Fn (0[,)+∞)) |
9 | | ex-fpar.a |
. . . . . . . . . . 11
⊢ 𝐴 =
(0[,)+∞) |
10 | 9 | reseq2i 5822 |
. . . . . . . . . 10
⊢ (√
↾ 𝐴) = (√
↾ (0[,)+∞)) |
11 | 10 | fneq1i 6435 |
. . . . . . . . 9
⊢ ((√
↾ 𝐴) Fn
(0[,)+∞) ↔ (√ ↾ (0[,)+∞)) Fn
(0[,)+∞)) |
12 | 8, 11 | sylibr 237 |
. . . . . . . 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 6433 |
. . . . . . . 8
⊢ (𝐹 = (√ ↾ 𝐴) → (𝐹 Fn 𝐴 ↔ (√ ↾ 𝐴) Fn (0[,)+∞))) |
18 | 14, 17 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 ↔ (√ ↾ 𝐴) Fn (0[,)+∞)) |
19 | 13, 18 | mpbir 234 |
. . . . . 6
⊢ 𝐹 Fn 𝐴 |
20 | | sinf 15569 |
. . . . . . . . 9
⊢
sin:ℂ⟶ℂ |
21 | | ffn 6504 |
. . . . . . . . 9
⊢
(sin:ℂ⟶ℂ → sin Fn ℂ) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
⊢ sin Fn
ℂ |
23 | | fnssres 6459 |
. . . . . . . . 9
⊢ ((sin Fn
ℂ ∧ ℝ ⊆ ℂ) → (sin ↾ ℝ) Fn
ℝ) |
24 | | ex-fpar.b |
. . . . . . . . . . 11
⊢ 𝐵 = ℝ |
25 | 24 | reseq2i 5822 |
. . . . . . . . . 10
⊢ (sin
↾ 𝐵) = (sin ↾
ℝ) |
26 | 25 | fneq1i 6435 |
. . . . . . . . 9
⊢ ((sin
↾ 𝐵) Fn ℝ
↔ (sin ↾ ℝ) Fn ℝ) |
27 | 23, 26 | sylibr 237 |
. . . . . . . 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 6433 |
. . . . . . . 8
⊢ (𝐺 = (sin ↾ 𝐵) → (𝐺 Fn 𝐵 ↔ (sin ↾ 𝐵) Fn ℝ)) |
33 | 29, 32 | ax-mp 5 |
. . . . . . 7
⊢ (𝐺 Fn 𝐵 ↔ (sin ↾ 𝐵) Fn ℝ) |
34 | 28, 33 | mpbir 234 |
. . . . . 6
⊢ 𝐺 Fn 𝐵 |
35 | | ex-fpar.h |
. . . . . . 7
⊢ 𝐻 = ((◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V))))) |
36 | 35 | fpar 7837 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉)) |
37 | 19, 34, 36 | mp2an 692 |
. . . . 5
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) |
38 | | opex 5322 |
. . . . 5
⊢
〈(𝐹‘𝑥), (𝐺‘𝑦)〉 ∈ V |
39 | 37, 38 | fnmpoi 7793 |
. . . 4
⊢ 𝐻 Fn (𝐴 × 𝐵) |
40 | | opelxpi 5562 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
41 | | fvco2 6765 |
. . . 4
⊢ ((𝐻 Fn (𝐴 × 𝐵) ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) → (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) = ( + ‘(𝐻‘〈𝑋, 𝑌〉))) |
42 | 39, 40, 41 | sylancr 590 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) = ( + ‘(𝐻‘〈𝑋, 𝑌〉))) |
43 | | simpl 486 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐴) |
44 | | simpr 488 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
45 | 37, 43, 44 | fvproj 7854 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐻‘〈𝑋, 𝑌〉) = 〈(𝐹‘𝑋), (𝐺‘𝑌)〉) |
46 | 45 | fveq2d 6678 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ( + ‘(𝐻‘〈𝑋, 𝑌〉)) = ( + ‘〈(𝐹‘𝑋), (𝐺‘𝑌)〉)) |
47 | | df-ov 7173 |
. . . 4
⊢ ((𝐹‘𝑋) + (𝐺‘𝑌)) = ( + ‘〈(𝐹‘𝑋), (𝐺‘𝑌)〉) |
48 | 14 | fveq1i 6675 |
. . . . . 6
⊢ (𝐹‘𝑋) = ((√ ↾ 𝐴)‘𝑋) |
49 | | fvres 6693 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → ((√ ↾ 𝐴)‘𝑋) = (√‘𝑋)) |
50 | 48, 49 | syl5eq 2785 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝐹‘𝑋) = (√‘𝑋)) |
51 | 29 | fveq1i 6675 |
. . . . . 6
⊢ (𝐺‘𝑌) = ((sin ↾ 𝐵)‘𝑌) |
52 | | fvres 6693 |
. . . . . 6
⊢ (𝑌 ∈ 𝐵 → ((sin ↾ 𝐵)‘𝑌) = (sin‘𝑌)) |
53 | 51, 52 | syl5eq 2785 |
. . . . 5
⊢ (𝑌 ∈ 𝐵 → (𝐺‘𝑌) = (sin‘𝑌)) |
54 | 50, 53 | oveqan12d 7189 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝐹‘𝑋) + (𝐺‘𝑌)) = ((√‘𝑋) + (sin‘𝑌))) |
55 | 47, 54 | eqtr3id 2787 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ( + ‘〈(𝐹‘𝑋), (𝐺‘𝑌)〉) = ((√‘𝑋) + (sin‘𝑌))) |
56 | 42, 46, 55 | 3eqtrd 2777 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (( + ∘ 𝐻)‘〈𝑋, 𝑌〉) = ((√‘𝑋) + (sin‘𝑌))) |
57 | 1, 56 | syl5eq 2785 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋( + ∘ 𝐻)𝑌) = ((√‘𝑋) + (sin‘𝑌))) |