Step | Hyp | Ref
| Expression |
1 | | i1ff 25043 |
. . . . . . . 8
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
2 | 1 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ π₯ β β)
β (πΉβπ₯) β
β) |
3 | | i1ff 25043 |
. . . . . . . 8
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
4 | 3 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((πΊ β dom β«1
β§ π₯ β β)
β (πΊβπ₯) β
β) |
5 | | absreim 15179 |
. . . . . . 7
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β) β (absβ((πΉβπ₯) + (i Β· (πΊβπ₯)))) = (ββ(((πΉβπ₯)β2) + ((πΊβπ₯)β2)))) |
6 | 2, 4, 5 | syl2an 597 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ π₯ β β)
β§ (πΊ β dom
β«1 β§ π₯
β β)) β (absβ((πΉβπ₯) + (i Β· (πΊβπ₯)))) = (ββ(((πΉβπ₯)β2) + ((πΊβπ₯)β2)))) |
7 | 6 | anandirs 678 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (absβ((πΉβπ₯) + (i Β· (πΊβπ₯)))) = (ββ(((πΉβπ₯)β2) + ((πΊβπ₯)β2)))) |
8 | 2 | recnd 11184 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ π₯ β β)
β (πΉβπ₯) β
β) |
9 | 8 | sqvald 14049 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ π₯ β β)
β ((πΉβπ₯)β2) = ((πΉβπ₯) Β· (πΉβπ₯))) |
10 | 4 | recnd 11184 |
. . . . . . . . 9
β’ ((πΊ β dom β«1
β§ π₯ β β)
β (πΊβπ₯) β
β) |
11 | 10 | sqvald 14049 |
. . . . . . . 8
β’ ((πΊ β dom β«1
β§ π₯ β β)
β ((πΊβπ₯)β2) = ((πΊβπ₯) Β· (πΊβπ₯))) |
12 | 9, 11 | oveqan12d 7377 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ π₯ β β)
β§ (πΊ β dom
β«1 β§ π₯
β β)) β (((πΉβπ₯)β2) + ((πΊβπ₯)β2)) = (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯)))) |
13 | 12 | anandirs 678 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (((πΉβπ₯)β2) + ((πΊβπ₯)β2)) = (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯)))) |
14 | 13 | fveq2d 6847 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (ββ(((πΉβπ₯)β2) + ((πΊβπ₯)β2))) = (ββ(((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))))) |
15 | 7, 14 | eqtrd 2777 |
. . . 4
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (absβ((πΉβπ₯) + (i Β· (πΊβπ₯)))) = (ββ(((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))))) |
16 | 15 | mpteq2dva 5206 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (π₯ β β β¦ (absβ((πΉβπ₯) + (i Β· (πΊβπ₯))))) = (π₯ β β β¦
(ββ(((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯)))))) |
17 | | ax-icn 11111 |
. . . . . . 7
β’ i β
β |
18 | | mulcl 11136 |
. . . . . . 7
β’ ((i
β β β§ (πΊβπ₯) β β) β (i Β· (πΊβπ₯)) β β) |
19 | 17, 10, 18 | sylancr 588 |
. . . . . 6
β’ ((πΊ β dom β«1
β§ π₯ β β)
β (i Β· (πΊβπ₯)) β β) |
20 | | addcl 11134 |
. . . . . 6
β’ (((πΉβπ₯) β β β§ (i Β· (πΊβπ₯)) β β) β ((πΉβπ₯) + (i Β· (πΊβπ₯))) β β) |
21 | 8, 19, 20 | syl2an 597 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π₯ β β)
β§ (πΊ β dom
β«1 β§ π₯
β β)) β ((πΉβπ₯) + (i Β· (πΊβπ₯))) β β) |
22 | 21 | anandirs 678 |
. . . 4
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β ((πΉβπ₯) + (i Β· (πΊβπ₯))) β β) |
23 | | reex 11143 |
. . . . . 6
β’ β
β V |
24 | 23 | a1i 11 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β β β V) |
25 | 2 | adantlr 714 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (πΉβπ₯) β β) |
26 | | ovexd 7393 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (i Β· (πΊβπ₯)) β V) |
27 | 1 | feqmptd 6911 |
. . . . . 6
β’ (πΉ β dom β«1
β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
28 | 27 | adantr 482 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β πΉ
= (π₯ β β β¦
(πΉβπ₯))) |
29 | 23 | a1i 11 |
. . . . . . 7
β’ (πΊ β dom β«1
β β β V) |
30 | 17 | a1i 11 |
. . . . . . 7
β’ ((πΊ β dom β«1
β§ π₯ β β)
β i β β) |
31 | | fconstmpt 5695 |
. . . . . . . 8
β’ (β
Γ {i}) = (π₯ β
β β¦ i) |
32 | 31 | a1i 11 |
. . . . . . 7
β’ (πΊ β dom β«1
β (β Γ {i}) = (π₯ β β β¦ i)) |
33 | 3 | feqmptd 6911 |
. . . . . . 7
β’ (πΊ β dom β«1
β πΊ = (π₯ β β β¦ (πΊβπ₯))) |
34 | 29, 30, 4, 32, 33 | offval2 7638 |
. . . . . 6
β’ (πΊ β dom β«1
β ((β Γ {i}) βf Β· πΊ) = (π₯ β β β¦ (i Β· (πΊβπ₯)))) |
35 | 34 | adantl 483 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ((β Γ {i}) βf Β·
πΊ) = (π₯ β β β¦ (i Β· (πΊβπ₯)))) |
36 | 24, 25, 26, 28, 35 | offval2 7638 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΉ βf + ((β Γ
{i}) βf Β· πΊ)) = (π₯ β β β¦ ((πΉβπ₯) + (i Β· (πΊβπ₯))))) |
37 | | absf 15223 |
. . . . . 6
β’
abs:ββΆβ |
38 | 37 | a1i 11 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β abs:ββΆβ) |
39 | 38 | feqmptd 6911 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β abs = (π¦ β β β¦ (absβπ¦))) |
40 | | fveq2 6843 |
. . . 4
β’ (π¦ = ((πΉβπ₯) + (i Β· (πΊβπ₯))) β (absβπ¦) = (absβ((πΉβπ₯) + (i Β· (πΊβπ₯))))) |
41 | 22, 36, 39, 40 | fmptco 7076 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (abs β (πΉ βf + ((β Γ
{i}) βf Β· πΊ))) = (π₯ β β β¦ (absβ((πΉβπ₯) + (i Β· (πΊβπ₯)))))) |
42 | 8, 8 | mulcld 11176 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π₯ β β)
β ((πΉβπ₯) Β· (πΉβπ₯)) β β) |
43 | 10, 10 | mulcld 11176 |
. . . . . 6
β’ ((πΊ β dom β«1
β§ π₯ β β)
β ((πΊβπ₯) Β· (πΊβπ₯)) β β) |
44 | | addcl 11134 |
. . . . . 6
β’ ((((πΉβπ₯) Β· (πΉβπ₯)) β β β§ ((πΊβπ₯) Β· (πΊβπ₯)) β β) β (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))) β β) |
45 | 42, 43, 44 | syl2an 597 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π₯ β β)
β§ (πΊ β dom
β«1 β§ π₯
β β)) β (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))) β β) |
46 | 45 | anandirs 678 |
. . . 4
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))) β β) |
47 | 42 | adantlr 714 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β ((πΉβπ₯) Β· (πΉβπ₯)) β β) |
48 | 43 | adantll 713 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β β) β ((πΊβπ₯) Β· (πΊβπ₯)) β β) |
49 | 23 | a1i 11 |
. . . . . . 7
β’ (πΉ β dom β«1
β β β V) |
50 | 49, 2, 2, 27, 27 | offval2 7638 |
. . . . . 6
β’ (πΉ β dom β«1
β (πΉ
βf Β· πΉ) = (π₯ β β β¦ ((πΉβπ₯) Β· (πΉβπ₯)))) |
51 | 50 | adantr 482 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΉ βf Β· πΉ) = (π₯ β β β¦ ((πΉβπ₯) Β· (πΉβπ₯)))) |
52 | 29, 4, 4, 33, 33 | offval2 7638 |
. . . . . 6
β’ (πΊ β dom β«1
β (πΊ
βf Β· πΊ) = (π₯ β β β¦ ((πΊβπ₯) Β· (πΊβπ₯)))) |
53 | 52 | adantl 483 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΊ βf Β· πΊ) = (π₯ β β β¦ ((πΊβπ₯) Β· (πΊβπ₯)))) |
54 | 24, 47, 48, 51, 53 | offval2 7638 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) = (π₯ β β β¦ (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))))) |
55 | | sqrtf 15249 |
. . . . . 6
β’
β:ββΆβ |
56 | 55 | a1i 11 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β β:ββΆβ) |
57 | 56 | feqmptd 6911 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β β = (π¦ β β β¦ (ββπ¦))) |
58 | | fveq2 6843 |
. . . 4
β’ (π¦ = (((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))) β (ββπ¦) = (ββ(((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯))))) |
59 | 46, 54, 57, 58 | fmptco 7076 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) = (π₯ β β β¦
(ββ(((πΉβπ₯) Β· (πΉβπ₯)) + ((πΊβπ₯) Β· (πΊβπ₯)))))) |
60 | 16, 41, 59 | 3eqtr4d 2787 |
. 2
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (abs β (πΉ βf + ((β Γ
{i}) βf Β· πΊ))) = (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)))) |
61 | | elrege0 13372 |
. . . . . . 7
β’ (π₯ β (0[,)+β) β
(π₯ β β β§ 0
β€ π₯)) |
62 | | resqrtcl 15139 |
. . . . . . 7
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β) |
63 | 61, 62 | sylbi 216 |
. . . . . 6
β’ (π₯ β (0[,)+β) β
(ββπ₯) β
β) |
64 | 63 | adantl 483 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β (0[,)+β)) β (ββπ₯) β β) |
65 | | id 22 |
. . . . . . . . 9
β’
(β:ββΆβ β
β:ββΆβ) |
66 | 65 | feqmptd 6911 |
. . . . . . . 8
β’
(β:ββΆβ β β = (π₯ β β β¦ (ββπ₯))) |
67 | 55, 66 | ax-mp 5 |
. . . . . . 7
β’ β =
(π₯ β β β¦
(ββπ₯)) |
68 | 67 | reseq1i 5934 |
. . . . . 6
β’ (β
βΎ (0[,)+β)) = ((π₯ β β β¦ (ββπ₯)) βΎ
(0[,)+β)) |
69 | | rge0ssre 13374 |
. . . . . . . 8
β’
(0[,)+β) β β |
70 | | ax-resscn 11109 |
. . . . . . . 8
β’ β
β β |
71 | 69, 70 | sstri 3954 |
. . . . . . 7
β’
(0[,)+β) β β |
72 | | resmpt 5992 |
. . . . . . 7
β’
((0[,)+β) β β β ((π₯ β β β¦ (ββπ₯)) βΎ (0[,)+β)) =
(π₯ β (0[,)+β)
β¦ (ββπ₯))) |
73 | 71, 72 | ax-mp 5 |
. . . . . 6
β’ ((π₯ β β β¦
(ββπ₯)) βΎ
(0[,)+β)) = (π₯ β
(0[,)+β) β¦ (ββπ₯)) |
74 | 68, 73 | eqtri 2765 |
. . . . 5
β’ (β
βΎ (0[,)+β)) = (π₯ β (0[,)+β) β¦
(ββπ₯)) |
75 | 64, 74 | fmptd 7063 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β βΎ
(0[,)+β)):(0[,)+β)βΆβ) |
76 | | ge0addcl 13378 |
. . . . . 6
β’ ((π₯ β (0[,)+β) β§
π¦ β (0[,)+β))
β (π₯ + π¦) β
(0[,)+β)) |
77 | 76 | adantl 483 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ (π₯
β (0[,)+β) β§ π¦ β (0[,)+β))) β (π₯ + π¦) β (0[,)+β)) |
78 | | oveq12 7367 |
. . . . . . . . 9
β’ ((π§ = πΉ β§ π§ = πΉ) β (π§ βf Β· π§) = (πΉ βf Β· πΉ)) |
79 | 78 | anidms 568 |
. . . . . . . 8
β’ (π§ = πΉ β (π§ βf Β· π§) = (πΉ βf Β· πΉ)) |
80 | 79 | feq1d 6654 |
. . . . . . 7
β’ (π§ = πΉ β ((π§ βf Β· π§):ββΆ(0[,)+β)
β (πΉ
βf Β· πΉ):ββΆ(0[,)+β))) |
81 | | i1ff 25043 |
. . . . . . . . . . . 12
β’ (π§ β dom β«1
β π§:ββΆβ) |
82 | 81 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π§ β dom β«1
β§ π₯ β β)
β (π§βπ₯) β
β) |
83 | 82, 82 | remulcld 11186 |
. . . . . . . . . 10
β’ ((π§ β dom β«1
β§ π₯ β β)
β ((π§βπ₯) Β· (π§βπ₯)) β β) |
84 | 82 | msqge0d 11724 |
. . . . . . . . . 10
β’ ((π§ β dom β«1
β§ π₯ β β)
β 0 β€ ((π§βπ₯) Β· (π§βπ₯))) |
85 | | elrege0 13372 |
. . . . . . . . . 10
β’ (((π§βπ₯) Β· (π§βπ₯)) β (0[,)+β) β (((π§βπ₯) Β· (π§βπ₯)) β β β§ 0 β€ ((π§βπ₯) Β· (π§βπ₯)))) |
86 | 83, 84, 85 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π§ β dom β«1
β§ π₯ β β)
β ((π§βπ₯) Β· (π§βπ₯)) β (0[,)+β)) |
87 | 86 | fmpttd 7064 |
. . . . . . . 8
β’ (π§ β dom β«1
β (π₯ β β
β¦ ((π§βπ₯) Β· (π§βπ₯))):ββΆ(0[,)+β)) |
88 | 23 | a1i 11 |
. . . . . . . . . 10
β’ (π§ β dom β«1
β β β V) |
89 | 81 | feqmptd 6911 |
. . . . . . . . . 10
β’ (π§ β dom β«1
β π§ = (π₯ β β β¦ (π§βπ₯))) |
90 | 88, 82, 82, 89, 89 | offval2 7638 |
. . . . . . . . 9
β’ (π§ β dom β«1
β (π§
βf Β· π§) = (π₯ β β β¦ ((π§βπ₯) Β· (π§βπ₯)))) |
91 | 90 | feq1d 6654 |
. . . . . . . 8
β’ (π§ β dom β«1
β ((π§
βf Β· π§):ββΆ(0[,)+β) β (π₯ β β β¦ ((π§βπ₯) Β· (π§βπ₯))):ββΆ(0[,)+β))) |
92 | 87, 91 | mpbird 257 |
. . . . . . 7
β’ (π§ β dom β«1
β (π§
βf Β· π§):ββΆ(0[,)+β)) |
93 | 80, 92 | vtoclga 3535 |
. . . . . 6
β’ (πΉ β dom β«1
β (πΉ
βf Β· πΉ):ββΆ(0[,)+β)) |
94 | 93 | adantr 482 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΉ βf Β· πΉ):ββΆ(0[,)+β)) |
95 | | oveq12 7367 |
. . . . . . . . 9
β’ ((π§ = πΊ β§ π§ = πΊ) β (π§ βf Β· π§) = (πΊ βf Β· πΊ)) |
96 | 95 | anidms 568 |
. . . . . . . 8
β’ (π§ = πΊ β (π§ βf Β· π§) = (πΊ βf Β· πΊ)) |
97 | 96 | feq1d 6654 |
. . . . . . 7
β’ (π§ = πΊ β ((π§ βf Β· π§):ββΆ(0[,)+β)
β (πΊ
βf Β· πΊ):ββΆ(0[,)+β))) |
98 | 97, 92 | vtoclga 3535 |
. . . . . 6
β’ (πΊ β dom β«1
β (πΊ
βf Β· πΊ):ββΆ(0[,)+β)) |
99 | 98 | adantl 483 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΊ βf Β· πΊ):ββΆ(0[,)+β)) |
100 | | inidm 4179 |
. . . . 5
β’ (β
β© β) = β |
101 | 77, 94, 99, 24, 24, 100 | off 7636 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)):ββΆ(0[,)+β)) |
102 | | fco2 6696 |
. . . 4
β’
(((β βΎ (0[,)+β)):(0[,)+β)βΆβ β§
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ)):ββΆ(0[,)+β)) β
(β β ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ))):ββΆβ) |
103 | 75, 101, 102 | syl2anc 585 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))):ββΆβ) |
104 | | rnco 6205 |
. . . 4
β’ ran
(β β ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ))) = ran (β βΎ ran
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) |
105 | | ffn 6669 |
. . . . . . . 8
β’
(β:ββΆβ β β Fn
β) |
106 | 55, 105 | ax-mp 5 |
. . . . . . 7
β’ β
Fn β |
107 | | readdcl 11135 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
108 | 107 | adantl 483 |
. . . . . . . . . 10
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ (π₯
β β β§ π¦
β β)) β (π₯
+ π¦) β
β) |
109 | | remulcl 11137 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
110 | 109 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΉ β dom β«1
β§ (π₯ β β
β§ π¦ β β))
β (π₯ Β· π¦) β
β) |
111 | 110, 1, 1, 49, 49, 100 | off 7636 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (πΉ
βf Β· πΉ):ββΆβ) |
112 | 111 | adantr 482 |
. . . . . . . . . 10
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΉ βf Β· πΉ):ββΆβ) |
113 | 109 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΊ β dom β«1
β§ (π₯ β β
β§ π¦ β β))
β (π₯ Β· π¦) β
β) |
114 | 113, 3, 3, 29, 29, 100 | off 7636 |
. . . . . . . . . . 11
β’ (πΊ β dom β«1
β (πΊ
βf Β· πΊ):ββΆβ) |
115 | 114 | adantl 483 |
. . . . . . . . . 10
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΊ βf Β· πΊ):ββΆβ) |
116 | 108, 112,
115, 24, 24, 100 | off 7636 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)):ββΆβ) |
117 | 116 | frnd 6677 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β
β) |
118 | 117, 70 | sstrdi 3957 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β
β) |
119 | | fnssres 6625 |
. . . . . . 7
β’ ((β
Fn β β§ ran ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ)) β β) β
(β βΎ ran ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ))) Fn ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) |
120 | 106, 118,
119 | sylancr 588 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β βΎ ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) Fn ran ((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ))) |
121 | | id 22 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β πΉ β dom
β«1) |
122 | 121, 121 | i1fmul 25063 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (πΉ
βf Β· πΉ) β dom
β«1) |
123 | 122 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΉ βf Β· πΉ) β dom
β«1) |
124 | | id 22 |
. . . . . . . . . 10
β’ (πΊ β dom β«1
β πΊ β dom
β«1) |
125 | 124, 124 | i1fmul 25063 |
. . . . . . . . 9
β’ (πΊ β dom β«1
β (πΊ
βf Β· πΊ) β dom
β«1) |
126 | 125 | adantl 483 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (πΊ βf Β· πΊ) β dom
β«1) |
127 | 123, 126 | i1fadd 25062 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β dom
β«1) |
128 | | i1frn 25044 |
. . . . . . 7
β’ (((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ)) β dom
β«1 β ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β
Fin) |
129 | 127, 128 | syl 17 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β
Fin) |
130 | | fnfi 9126 |
. . . . . 6
β’
(((β βΎ ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) Fn ran ((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ)) β§ ran
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ)) β Fin) β (β βΎ ran
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) β Fin) |
131 | 120, 129,
130 | syl2anc 585 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β βΎ ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β
Fin) |
132 | | rnfi 9280 |
. . . . 5
β’ ((β
βΎ ran ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ))) β Fin β ran
(β βΎ ran ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ))) β Fin) |
133 | 131, 132 | syl 17 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ran (β βΎ ran ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β
Fin) |
134 | 104, 133 | eqeltrid 2842 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β ran (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β
Fin) |
135 | | cnvco 5842 |
. . . . . . 7
β’ β‘(β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) = (β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β β‘β) |
136 | 135 | imaeq1i 6011 |
. . . . . 6
β’ (β‘(β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β {π₯}) = ((β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β β‘β) β {π₯}) |
137 | | imaco 6204 |
. . . . . 6
β’ ((β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β β‘β) β {π₯}) = (β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β (β‘β β {π₯})) |
138 | 136, 137 | eqtri 2765 |
. . . . 5
β’ (β‘(β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β {π₯}) = (β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β (β‘β β {π₯})) |
139 | | i1fima 25045 |
. . . . . 6
β’ (((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ)) β dom
β«1 β (β‘((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ)) β (β‘β β {π₯})) β dom vol) |
140 | 127, 139 | syl 17 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β‘((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ)) β (β‘β β {π₯})) β dom vol) |
141 | 138, 140 | eqeltrid 2842 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β‘(β
β ((πΉ
βf Β· πΉ) βf + (πΊ βf Β· πΊ))) β {π₯}) β dom vol) |
142 | 141 | adantr 482 |
. . 3
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β (ran (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β {0})) β
(β‘(β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β {π₯}) β dom
vol) |
143 | 138 | fveq2i 6846 |
. . . 4
β’
(volβ(β‘(β β
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) β {π₯})) = (volβ(β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β (β‘β β {π₯}))) |
144 | | eldifsni 4751 |
. . . . . . . 8
β’ (π₯ β (ran (β β
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) β {0}) β π₯ β 0) |
145 | | c0ex 11150 |
. . . . . . . . . . . 12
β’ 0 β
V |
146 | 145 | elsn 4602 |
. . . . . . . . . . 11
β’ (0 β
{π₯} β 0 = π₯) |
147 | | eqcom 2744 |
. . . . . . . . . . 11
β’ (0 =
π₯ β π₯ = 0) |
148 | 146, 147 | bitri 275 |
. . . . . . . . . 10
β’ (0 β
{π₯} β π₯ = 0) |
149 | 148 | necon3bbii 2992 |
. . . . . . . . 9
β’ (Β¬ 0
β {π₯} β π₯ β 0) |
150 | | sqrt0 15127 |
. . . . . . . . . 10
β’
(ββ0) = 0 |
151 | 150 | eleq1i 2829 |
. . . . . . . . 9
β’
((ββ0) β {π₯} β 0 β {π₯}) |
152 | 149, 151 | xchnxbir 333 |
. . . . . . . 8
β’ (Β¬
(ββ0) β {π₯} β π₯ β 0) |
153 | 144, 152 | sylibr 233 |
. . . . . . 7
β’ (π₯ β (ran (β β
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) β {0}) β Β¬
(ββ0) β {π₯}) |
154 | 153 | olcd 873 |
. . . . . 6
β’ (π₯ β (ran (β β
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) β {0}) β (Β¬ 0 β
β β¨ Β¬ (ββ0) β {π₯})) |
155 | | ianor 981 |
. . . . . . 7
β’ (Β¬ (0
β β β§ (ββ0) β {π₯}) β (Β¬ 0 β β β¨ Β¬
(ββ0) β {π₯})) |
156 | | elpreima 7009 |
. . . . . . . 8
β’ (β
Fn β β (0 β (β‘β
β {π₯}) β (0
β β β§ (ββ0) β {π₯}))) |
157 | 55, 105, 156 | mp2b 10 |
. . . . . . 7
β’ (0 β
(β‘β β {π₯}) β (0 β β β§
(ββ0) β {π₯})) |
158 | 155, 157 | xchnxbir 333 |
. . . . . 6
β’ (Β¬ 0
β (β‘β β {π₯}) β (Β¬ 0 β
β β¨ Β¬ (ββ0) β {π₯})) |
159 | 154, 158 | sylibr 233 |
. . . . 5
β’ (π₯ β (ran (β β
((πΉ βf
Β· πΉ)
βf + (πΊ
βf Β· πΊ))) β {0}) β Β¬ 0 β
(β‘β β {π₯})) |
160 | | i1fima2 25046 |
. . . . 5
β’ ((((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ)) β dom
β«1 β§ Β¬ 0 β (β‘β β {π₯})) β (volβ(β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β (β‘β β {π₯}))) β β) |
161 | 127, 159,
160 | syl2an 597 |
. . . 4
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β (ran (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β {0})) β
(volβ(β‘((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ)) β (β‘β β {π₯}))) β β) |
162 | 143, 161 | eqeltrid 2842 |
. . 3
β’ (((πΉ β dom β«1
β§ πΊ β dom
β«1) β§ π₯
β (ran (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β {0})) β
(volβ(β‘(β β ((πΉ βf Β·
πΉ) βf +
(πΊ βf
Β· πΊ))) β
{π₯})) β
β) |
163 | 103, 134,
142, 162 | i1fd 25048 |
. 2
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (β β ((πΉ βf Β· πΉ) βf + (πΊ βf Β·
πΊ))) β dom
β«1) |
164 | 60, 163 | eqeltrd 2838 |
1
β’ ((πΉ β dom β«1
β§ πΊ β dom
β«1) β (abs β (πΉ βf + ((β Γ
{i}) βf Β· πΊ))) β dom
β«1) |