Step | Hyp | Ref
| Expression |
1 | | df-ov 7365 |
. 2
β’ (π( + β π»)π) = (( + β π»)ββ¨π, πβ©) |
2 | | sqrtf 15255 |
. . . . . . . . 9
β’
β:ββΆβ |
3 | | ffn 6673 |
. . . . . . . . 9
β’
(β:ββΆβ β β Fn
β) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
β’ β
Fn β |
5 | | rge0ssre 13380 |
. . . . . . . . 9
β’
(0[,)+β) β β |
6 | | ax-resscn 11115 |
. . . . . . . . 9
β’ β
β β |
7 | 5, 6 | sstri 3958 |
. . . . . . . 8
β’
(0[,)+β) β β |
8 | | fnssres 6629 |
. . . . . . . . 9
β’ ((β
Fn β β§ (0[,)+β) β β) β (β βΎ
(0[,)+β)) Fn (0[,)+β)) |
9 | | ex-fpar.a |
. . . . . . . . . . 11
β’ π΄ =
(0[,)+β) |
10 | 9 | reseq2i 5939 |
. . . . . . . . . 10
β’ (β
βΎ π΄) = (β
βΎ (0[,)+β)) |
11 | 10 | fneq1i 6604 |
. . . . . . . . 9
β’ ((β
βΎ π΄) Fn
(0[,)+β) β (β βΎ (0[,)+β)) Fn
(0[,)+β)) |
12 | 8, 11 | sylibr 233 |
. . . . . . . 8
β’ ((β
Fn β β§ (0[,)+β) β β) β (β βΎ π΄) Fn
(0[,)+β)) |
13 | 4, 7, 12 | mp2an 691 |
. . . . . . 7
β’ (β
βΎ π΄) Fn
(0[,)+β) |
14 | | ex-fpar.f |
. . . . . . . 8
β’ πΉ = (β βΎ π΄) |
15 | | id 22 |
. . . . . . . . 9
β’ (πΉ = (β βΎ π΄) β πΉ = (β βΎ π΄)) |
16 | 9 | a1i 11 |
. . . . . . . . 9
β’ (πΉ = (β βΎ π΄) β π΄ = (0[,)+β)) |
17 | 15, 16 | fneq12d 6602 |
. . . . . . . 8
β’ (πΉ = (β βΎ π΄) β (πΉ Fn π΄ β (β βΎ π΄) Fn (0[,)+β))) |
18 | 14, 17 | ax-mp 5 |
. . . . . . 7
β’ (πΉ Fn π΄ β (β βΎ π΄) Fn (0[,)+β)) |
19 | 13, 18 | mpbir 230 |
. . . . . 6
β’ πΉ Fn π΄ |
20 | | sinf 16013 |
. . . . . . . . 9
β’
sin:ββΆβ |
21 | | ffn 6673 |
. . . . . . . . 9
β’
(sin:ββΆβ β sin Fn β) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
β’ sin Fn
β |
23 | | fnssres 6629 |
. . . . . . . . 9
β’ ((sin Fn
β β§ β β β) β (sin βΎ β) Fn
β) |
24 | | ex-fpar.b |
. . . . . . . . . . 11
β’ π΅ = β |
25 | 24 | reseq2i 5939 |
. . . . . . . . . 10
β’ (sin
βΎ π΅) = (sin βΎ
β) |
26 | 25 | fneq1i 6604 |
. . . . . . . . 9
β’ ((sin
βΎ π΅) Fn β
β (sin βΎ β) Fn β) |
27 | 23, 26 | sylibr 233 |
. . . . . . . 8
β’ ((sin Fn
β β§ β β β) β (sin βΎ π΅) Fn β) |
28 | 22, 6, 27 | mp2an 691 |
. . . . . . 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 6602 |
. . . . . . . 8
β’ (πΊ = (sin βΎ π΅) β (πΊ Fn π΅ β (sin βΎ π΅) Fn β)) |
33 | 29, 32 | ax-mp 5 |
. . . . . . 7
β’ (πΊ Fn π΅ β (sin βΎ π΅) Fn β) |
34 | 28, 33 | mpbir 230 |
. . . . . 6
β’ πΊ Fn π΅ |
35 | | ex-fpar.h |
. . . . . . 7
β’ π» = ((β‘(1st βΎ (V Γ V))
β (πΉ β
(1st βΎ (V Γ V)))) β© (β‘(2nd βΎ (V Γ V))
β (πΊ β
(2nd βΎ (V Γ V))))) |
36 | 35 | fpar 8053 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ πΊ Fn π΅) β π» = (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©)) |
37 | 19, 34, 36 | mp2an 691 |
. . . . 5
β’ π» = (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) |
38 | | opex 5426 |
. . . . 5
β’
β¨(πΉβπ₯), (πΊβπ¦)β© β V |
39 | 37, 38 | fnmpoi 8007 |
. . . 4
β’ π» Fn (π΄ Γ π΅) |
40 | | opelxpi 5675 |
. . . 4
β’ ((π β π΄ β§ π β π΅) β β¨π, πβ© β (π΄ Γ π΅)) |
41 | | fvco2 6943 |
. . . 4
β’ ((π» Fn (π΄ Γ π΅) β§ β¨π, πβ© β (π΄ Γ π΅)) β (( + β π»)ββ¨π, πβ©) = ( + β(π»ββ¨π, πβ©))) |
42 | 39, 40, 41 | sylancr 588 |
. . 3
β’ ((π β π΄ β§ π β π΅) β (( + β π»)ββ¨π, πβ©) = ( + β(π»ββ¨π, πβ©))) |
43 | | simpl 484 |
. . . . 5
β’ ((π β π΄ β§ π β π΅) β π β π΄) |
44 | | simpr 486 |
. . . . 5
β’ ((π β π΄ β§ π β π΅) β π β π΅) |
45 | 37, 43, 44 | fvproj 8071 |
. . . 4
β’ ((π β π΄ β§ π β π΅) β (π»ββ¨π, πβ©) = β¨(πΉβπ), (πΊβπ)β©) |
46 | 45 | fveq2d 6851 |
. . 3
β’ ((π β π΄ β§ π β π΅) β ( + β(π»ββ¨π, πβ©)) = ( + ββ¨(πΉβπ), (πΊβπ)β©)) |
47 | | df-ov 7365 |
. . . 4
β’ ((πΉβπ) + (πΊβπ)) = ( + ββ¨(πΉβπ), (πΊβπ)β©) |
48 | 14 | fveq1i 6848 |
. . . . . 6
β’ (πΉβπ) = ((β βΎ π΄)βπ) |
49 | | fvres 6866 |
. . . . . 6
β’ (π β π΄ β ((β βΎ π΄)βπ) = (ββπ)) |
50 | 48, 49 | eqtrid 2789 |
. . . . 5
β’ (π β π΄ β (πΉβπ) = (ββπ)) |
51 | 29 | fveq1i 6848 |
. . . . . 6
β’ (πΊβπ) = ((sin βΎ π΅)βπ) |
52 | | fvres 6866 |
. . . . . 6
β’ (π β π΅ β ((sin βΎ π΅)βπ) = (sinβπ)) |
53 | 51, 52 | eqtrid 2789 |
. . . . 5
β’ (π β π΅ β (πΊβπ) = (sinβπ)) |
54 | 50, 53 | oveqan12d 7381 |
. . . 4
β’ ((π β π΄ β§ π β π΅) β ((πΉβπ) + (πΊβπ)) = ((ββπ) + (sinβπ))) |
55 | 47, 54 | eqtr3id 2791 |
. . 3
β’ ((π β π΄ β§ π β π΅) β ( + ββ¨(πΉβπ), (πΊβπ)β©) = ((ββπ) + (sinβπ))) |
56 | 42, 46, 55 | 3eqtrd 2781 |
. 2
β’ ((π β π΄ β§ π β π΅) β (( + β π»)ββ¨π, πβ©) = ((ββπ) + (sinβπ))) |
57 | 1, 56 | eqtrid 2789 |
1
β’ ((π β π΄ β§ π β π΅) β (π( + β π»)π) = ((ββπ) + (sinβπ))) |