Step | Hyp | Ref
| Expression |
1 | | minvec.f |
. . 3
β’ πΉ = ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
2 | | ssrab2 4042 |
. . . . . 6
β’ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β π |
3 | | minvec.y |
. . . . . . . 8
β’ (π β π β (LSubSpβπ)) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β+) β π β (LSubSpβπ)) |
5 | | elpw2g 5306 |
. . . . . . 7
β’ (π β (LSubSpβπ) β ({π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β π« π β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β π)) |
6 | 4, 5 | syl 17 |
. . . . . 6
β’ ((π β§ π β β+) β ({π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β π« π β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β π)) |
7 | 2, 6 | mpbiri 258 |
. . . . 5
β’ ((π β§ π β β+) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β π« π) |
8 | 7 | fmpttd 7068 |
. . . 4
β’ (π β (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}):β+βΆπ«
π) |
9 | 8 | frnd 6681 |
. . 3
β’ (π β ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) β π« π) |
10 | 1, 9 | eqsstrid 3997 |
. 2
β’ (π β πΉ β π« π) |
11 | | 1rp 12926 |
. . . . . 6
β’ 1 β
β+ |
12 | | eqid 2737 |
. . . . . . 7
β’ (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
13 | 12, 7 | dmmptd 6651 |
. . . . . 6
β’ (π β dom (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = β+) |
14 | 11, 13 | eleqtrrid 2845 |
. . . . 5
β’ (π β 1 β dom (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
15 | 14 | ne0d 4300 |
. . . 4
β’ (π β dom (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) β β
) |
16 | | dm0rn0 5885 |
. . . . . 6
β’ (dom
(π β
β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = β
β ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = β
) |
17 | 1 | eqeq1i 2742 |
. . . . . 6
β’ (πΉ = β
β ran (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = β
) |
18 | 16, 17 | bitr4i 278 |
. . . . 5
β’ (dom
(π β
β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = β
β πΉ = β
) |
19 | 18 | necon3bii 2997 |
. . . 4
β’ (dom
(π β
β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) β β
β πΉ β β
) |
20 | 15, 19 | sylib 217 |
. . 3
β’ (π β πΉ β β
) |
21 | | minvec.x |
. . . . . . . . . . . . . . . . . 18
β’ π = (Baseβπ) |
22 | | minvec.m |
. . . . . . . . . . . . . . . . . 18
β’ β =
(-gβπ) |
23 | | minvec.n |
. . . . . . . . . . . . . . . . . 18
β’ π = (normβπ) |
24 | | minvec.u |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β βPreHil) |
25 | | minvec.w |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π βΎs π) β CMetSp) |
26 | | minvec.a |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β π) |
27 | | minvec.j |
. . . . . . . . . . . . . . . . . 18
β’ π½ = (TopOpenβπ) |
28 | | minvec.r |
. . . . . . . . . . . . . . . . . 18
β’ π
= ran (π¦ β π β¦ (πβ(π΄ β π¦))) |
29 | | minvec.s |
. . . . . . . . . . . . . . . . . 18
β’ π = inf(π
, β, < ) |
30 | 21, 22, 23, 24, 3, 25, 26, 27, 28, 29 | minveclem4c 24805 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
31 | 30 | resqcld 14037 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ2) β β) |
32 | | ltaddrp 12959 |
. . . . . . . . . . . . . . . 16
β’ (((πβ2) β β β§
π β
β+) β (πβ2) < ((πβ2) + π)) |
33 | 31, 32 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β+) β (πβ2) < ((πβ2) + π)) |
34 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β+) β (πβ2) β
β) |
35 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β π β
β) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β+) β π β
β) |
37 | 34, 36 | readdcld 11191 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β ((πβ2) + π) β β) |
38 | 37 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β+) β ((πβ2) + π) β β) |
39 | 38 | sqsqrtd 15331 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β+) β
((ββ((πβ2)
+ π))β2) = ((πβ2) + π)) |
40 | 33, 39 | breqtrrd 5138 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β (πβ2) <
((ββ((πβ2)
+ π))β2)) |
41 | 21, 22, 23, 24, 3, 25, 26, 27, 28 | minveclem1 24804 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
42 | 41 | simp1d 1143 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π
β β) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β π
β
β) |
44 | 41 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π
β β
) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β π
β β
) |
46 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
47 | 41 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ€ β π
0 β€ π€) |
48 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = 0 β (π¦ β€ π€ β 0 β€ π€)) |
49 | 48 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = 0 β (βπ€ β π
π¦ β€ π€ β βπ€ β π
0 β€ π€)) |
50 | 49 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ¦ β β βπ€ β π
π¦ β€ π€) |
51 | 46, 47, 50 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ¦ β β βπ€ β π
π¦ β€ π€) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β
βπ¦ β β
βπ€ β π
π¦ β€ π€) |
53 | | infrecl 12144 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β β β§ π
β β
β§ βπ¦ β β βπ€ β π
π¦ β€ π€) β inf(π
, β, < ) β
β) |
54 | 43, 45, 52, 53 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β+) β inf(π
, β, < ) β
β) |
55 | 29, 54 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β+) β π β
β) |
56 | | 0red 11165 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β 0 β
β) |
57 | 55 | sqge0d 14049 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β+) β 0 β€
(πβ2)) |
58 | 56, 34, 37, 57, 33 | lelttrd 11320 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β 0 <
((πβ2) + π)) |
59 | 56, 37, 58 | ltled 11310 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β+) β 0 β€
((πβ2) + π)) |
60 | 37, 59 | resqrtcld 15309 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β+) β
(ββ((πβ2)
+ π)) β
β) |
61 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β
βπ€ β π
0 β€ π€) |
62 | | infregelb 12146 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β β β§ π
β β
β§ βπ¦ β β βπ€ β π
π¦ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
63 | 43, 45, 52, 56, 62 | syl31anc 1374 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
64 | 61, 63 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β+) β 0 β€
inf(π
, β, <
)) |
65 | 64, 29 | breqtrrdi 5152 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β+) β 0 β€
π) |
66 | 37, 59 | sqrtge0d 15312 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β+) β 0 β€
(ββ((πβ2)
+ π))) |
67 | 55, 60, 65, 66 | lt2sqd 14166 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β (π < (ββ((πβ2) + π)) β (πβ2) < ((ββ((πβ2) + π))β2))) |
68 | 40, 67 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β π < (ββ((πβ2) + π))) |
69 | 55, 60 | ltnled 11309 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β (π < (ββ((πβ2) + π)) β Β¬ (ββ((πβ2) + π)) β€ π)) |
70 | 68, 69 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β β+) β Β¬
(ββ((πβ2)
+ π)) β€ π) |
71 | 29 | breq2i 5118 |
. . . . . . . . . . . . 13
β’
((ββ((πβ2) + π)) β€ π β (ββ((πβ2) + π)) β€ inf(π
, β, < )) |
72 | | infregelb 12146 |
. . . . . . . . . . . . . . 15
β’ (((π
β β β§ π
β β
β§ βπ¦ β β βπ€ β π
π¦ β€ π€) β§ (ββ((πβ2) + π)) β β) β
((ββ((πβ2)
+ π)) β€ inf(π
, β, < ) β
βπ€ β π
(ββ((πβ2) + π)) β€ π€)) |
73 | 43, 45, 52, 60, 72 | syl31anc 1374 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β
((ββ((πβ2)
+ π)) β€ inf(π
, β, < ) β
βπ€ β π
(ββ((πβ2) + π)) β€ π€)) |
74 | 28 | raleqi 3314 |
. . . . . . . . . . . . . . 15
β’
(βπ€ β
π
(ββ((πβ2) + π)) β€ π€ β βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))(ββ((πβ2) + π)) β€ π€) |
75 | | fvex 6860 |
. . . . . . . . . . . . . . . . 17
β’ (πβ(π΄ β π¦)) β V |
76 | 75 | rgenw 3069 |
. . . . . . . . . . . . . . . 16
β’
βπ¦ β
π (πβ(π΄ β π¦)) β V |
77 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β π β¦ (πβ(π΄ β π¦))) = (π¦ β π β¦ (πβ(π΄ β π¦))) |
78 | | breq2 5114 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = (πβ(π΄ β π¦)) β ((ββ((πβ2) + π)) β€ π€ β (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)))) |
79 | 77, 78 | ralrnmptw 7049 |
. . . . . . . . . . . . . . . 16
β’
(βπ¦ β
π (πβ(π΄ β π¦)) β V β (βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))(ββ((πβ2) + π)) β€ π€ β βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)))) |
80 | 76, 79 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
(βπ€ β
ran (π¦ β π β¦ (πβ(π΄ β π¦)))(ββ((πβ2) + π)) β€ π€ β βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦))) |
81 | 74, 80 | bitri 275 |
. . . . . . . . . . . . . 14
β’
(βπ€ β
π
(ββ((πβ2) + π)) β€ π€ β βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦))) |
82 | 73, 81 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β
((ββ((πβ2)
+ π)) β€ inf(π
, β, < ) β
βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)))) |
83 | 71, 82 | bitrid 283 |
. . . . . . . . . . . 12
β’ ((π β§ π β β+) β
((ββ((πβ2)
+ π)) β€ π β βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)))) |
84 | 70, 83 | mtbid 324 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β Β¬
βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦))) |
85 | | rexnal 3104 |
. . . . . . . . . . 11
β’
(βπ¦ β
π Β¬
(ββ((πβ2)
+ π)) β€ (πβ(π΄ β π¦)) β Β¬ βπ¦ β π (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦))) |
86 | 84, 85 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β
βπ¦ β π Β¬ (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦))) |
87 | 60 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π¦ β π) β (ββ((πβ2) + π)) β β) |
88 | | cphngp 24553 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βPreHil β
π β
NrmGrp) |
89 | 24, 88 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β NrmGrp) |
90 | | ngpms 23972 |
. . . . . . . . . . . . . . . . . 18
β’ (π β NrmGrp β π β MetSp) |
91 | | minvec.d |
. . . . . . . . . . . . . . . . . . 19
β’ π· = ((distβπ) βΎ (π Γ π)) |
92 | 21, 91 | msmet 23826 |
. . . . . . . . . . . . . . . . . 18
β’ (π β MetSp β π· β (Metβπ)) |
93 | 89, 90, 92 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π β π· β (Metβπ)) |
94 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π¦ β π) β π· β (Metβπ)) |
95 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π¦ β π) β π΄ β π) |
96 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(LSubSpβπ) =
(LSubSpβπ) |
97 | 21, 96 | lssss 20413 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (LSubSpβπ) β π β π) |
98 | 4, 97 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β+) β π β π) |
99 | 98 | sselda 3949 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π¦ β π) β π¦ β π) |
100 | | metcl 23701 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Metβπ) β§ π΄ β π β§ π¦ β π) β (π΄π·π¦) β β) |
101 | 94, 95, 99, 100 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π¦ β π) β (π΄π·π¦) β β) |
102 | 66 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π¦ β π) β 0 β€ (ββ((πβ2) + π))) |
103 | | metge0 23714 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Metβπ) β§ π΄ β π β§ π¦ β π) β 0 β€ (π΄π·π¦)) |
104 | 94, 95, 99, 103 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π¦ β π) β 0 β€ (π΄π·π¦)) |
105 | 87, 101, 102, 104 | le2sqd 14167 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π¦ β π) β ((ββ((πβ2) + π)) β€ (π΄π·π¦) β ((ββ((πβ2) + π))β2) β€ ((π΄π·π¦)β2))) |
106 | 91 | oveqi 7375 |
. . . . . . . . . . . . . . . . 17
β’ (π΄π·π¦) = (π΄((distβπ) βΎ (π Γ π))π¦) |
107 | 95, 99 | ovresd 7526 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π¦ β π) β (π΄((distβπ) βΎ (π Γ π))π¦) = (π΄(distβπ)π¦)) |
108 | 106, 107 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π¦ β π) β (π΄π·π¦) = (π΄(distβπ)π¦)) |
109 | 89 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π¦ β π) β π β NrmGrp) |
110 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(distβπ) =
(distβπ) |
111 | 23, 21, 22, 110 | ngpds 23976 |
. . . . . . . . . . . . . . . . 17
β’ ((π β NrmGrp β§ π΄ β π β§ π¦ β π) β (π΄(distβπ)π¦) = (πβ(π΄ β π¦))) |
112 | 109, 95, 99, 111 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π¦ β π) β (π΄(distβπ)π¦) = (πβ(π΄ β π¦))) |
113 | 108, 112 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π¦ β π) β (π΄π·π¦) = (πβ(π΄ β π¦))) |
114 | 113 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π¦ β π) β ((ββ((πβ2) + π)) β€ (π΄π·π¦) β (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)))) |
115 | 39 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π¦ β π) β ((ββ((πβ2) + π))β2) = ((πβ2) + π)) |
116 | 115 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π¦ β π) β (((ββ((πβ2) + π))β2) β€ ((π΄π·π¦)β2) β ((πβ2) + π) β€ ((π΄π·π¦)β2))) |
117 | 105, 114,
116 | 3bitr3d 309 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π¦ β π) β ((ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)) β ((πβ2) + π) β€ ((π΄π·π¦)β2))) |
118 | 117 | notbid 318 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π¦ β π) β (Β¬ (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)) β Β¬ ((πβ2) + π) β€ ((π΄π·π¦)β2))) |
119 | 37 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π¦ β π) β ((πβ2) + π) β β) |
120 | 101 | resqcld 14037 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π¦ β π) β ((π΄π·π¦)β2) β β) |
121 | 119, 120 | letrid 11314 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π¦ β π) β (((πβ2) + π) β€ ((π΄π·π¦)β2) β¨ ((π΄π·π¦)β2) β€ ((πβ2) + π))) |
122 | 121 | ord 863 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π¦ β π) β (Β¬ ((πβ2) + π) β€ ((π΄π·π¦)β2) β ((π΄π·π¦)β2) β€ ((πβ2) + π))) |
123 | 118, 122 | sylbid 239 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π¦ β π) β (Β¬ (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)) β ((π΄π·π¦)β2) β€ ((πβ2) + π))) |
124 | 123 | reximdva 3166 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β
(βπ¦ β π Β¬ (ββ((πβ2) + π)) β€ (πβ(π΄ β π¦)) β βπ¦ β π ((π΄π·π¦)β2) β€ ((πβ2) + π))) |
125 | 86, 124 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β β+) β
βπ¦ β π ((π΄π·π¦)β2) β€ ((πβ2) + π)) |
126 | | rabn0 4350 |
. . . . . . . . 9
β’ ({π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β β
β βπ¦ β π ((π΄π·π¦)β2) β€ ((πβ2) + π)) |
127 | 125, 126 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ π β β+) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β β
) |
128 | 127 | necomd 3000 |
. . . . . . 7
β’ ((π β§ π β β+) β β
β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
129 | 128 | neneqd 2949 |
. . . . . 6
β’ ((π β§ π β β+) β Β¬
β
= {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
130 | 129 | nrexdv 3147 |
. . . . 5
β’ (π β Β¬ βπ β β+
β
= {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
131 | 1 | eleq2i 2830 |
. . . . . 6
β’ (β
β πΉ β β
β ran (π β
β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
132 | | 0ex 5269 |
. . . . . . 7
β’ β
β V |
133 | 12 | elrnmpt 5916 |
. . . . . . 7
β’ (β
β V β (β
β ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) β βπ β β+ β
= {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
134 | 132, 133 | ax-mp 5 |
. . . . . 6
β’ (β
β ran (π β
β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) β βπ β β+ β
= {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
135 | 131, 134 | bitri 275 |
. . . . 5
β’ (β
β πΉ β
βπ β
β+ β
= {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
136 | 130, 135 | sylnibr 329 |
. . . 4
β’ (π β Β¬ β
β πΉ) |
137 | | df-nel 3051 |
. . . 4
β’ (β
β πΉ β Β¬
β
β πΉ) |
138 | 136, 137 | sylibr 233 |
. . 3
β’ (π β β
β πΉ) |
139 | 55 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π¦ β π) β π β β) |
140 | 139 | resqcld 14037 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π¦ β π) β (πβ2) β β) |
141 | 36 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π¦ β π) β π β β) |
142 | 120, 140,
141 | lesubadd2d 11761 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π¦ β π) β ((((π΄π·π¦)β2) β (πβ2)) β€ π β ((π΄π·π¦)β2) β€ ((πβ2) + π))) |
143 | 142 | rabbidva 3417 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π} = {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
144 | 143 | mpteq2dva 5210 |
. . . . . . . . . 10
β’ (π β (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) = (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
145 | 144 | rneqd 5898 |
. . . . . . . . 9
β’ (π β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) = ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
146 | 1, 145 | eqtr4id 2796 |
. . . . . . . 8
β’ (π β πΉ = ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π})) |
147 | 146 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π’ β πΉ β π’ β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}))) |
148 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π = π β ((((π΄π·π¦)β2) β (πβ2)) β€ π β (((π΄π·π¦)β2) β (πβ2)) β€ π )) |
149 | 148 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π = π β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π} = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π }) |
150 | 149 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π β β+
β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) = (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π }) |
151 | 150 | elrnmpt 5916 |
. . . . . . . 8
β’ (π’ β V β (π’ β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) β βπ β β+ π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π })) |
152 | 151 | elv 3454 |
. . . . . . 7
β’ (π’ β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) β βπ β β+ π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π }) |
153 | 147, 152 | bitrdi 287 |
. . . . . 6
β’ (π β (π’ β πΉ β βπ β β+ π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π })) |
154 | 146 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π£ β πΉ β π£ β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}))) |
155 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π = π‘ β ((((π΄π·π¦)β2) β (πβ2)) β€ π β (((π΄π·π¦)β2) β (πβ2)) β€ π‘)) |
156 | 155 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π = π‘ β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π} = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) |
157 | 156 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π β β+
β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) = (π‘ β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) |
158 | 157 | elrnmpt 5916 |
. . . . . . . 8
β’ (π£ β V β (π£ β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) β βπ‘ β β+ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘})) |
159 | 158 | elv 3454 |
. . . . . . 7
β’ (π£ β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) β βπ‘ β β+ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) |
160 | 154, 159 | bitrdi 287 |
. . . . . 6
β’ (π β (π£ β πΉ β βπ‘ β β+ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘})) |
161 | 153, 160 | anbi12d 632 |
. . . . 5
β’ (π β ((π’ β πΉ β§ π£ β πΉ) β (βπ β β+ π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ βπ‘ β β+ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}))) |
162 | | reeanv 3220 |
. . . . . 6
β’
(βπ β
β+ βπ‘ β β+ (π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (βπ β β+ π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ βπ‘ β β+ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘})) |
163 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π· β (Metβπ)) |
164 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π΄ β π) |
165 | 3, 97 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π) |
166 | 165 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β+ β§ π‘ β β+))
β π β π) |
167 | 166 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π¦ β π) |
168 | 163, 164,
167, 100 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β (π΄π·π¦) β β) |
169 | 168 | resqcld 14037 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β ((π΄π·π¦)β2) β β) |
170 | 31 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β (πβ2) β β) |
171 | 169, 170 | resubcld 11590 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β (((π΄π·π¦)β2) β (πβ2)) β β) |
172 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π β β+) |
173 | 172 | rpred 12964 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π β β) |
174 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π‘ β β+) |
175 | 174 | rpred 12964 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β π‘ β β) |
176 | | lemin 13118 |
. . . . . . . . . . . 12
β’
(((((π΄π·π¦)β2) β (πβ2)) β β β§ π β β β§ π‘ β β) β
((((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘) β ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘))) |
177 | 171, 173,
175, 176 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π β β+ β§ π‘ β β+))
β§ π¦ β π) β ((((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘) β ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘))) |
178 | 177 | rabbidva 3417 |
. . . . . . . . . 10
β’ ((π β§ (π β β+ β§ π‘ β β+))
β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} = {π¦ β π β£ ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘)}) |
179 | | ifcl 4536 |
. . . . . . . . . . . 12
β’ ((π β β+
β§ π‘ β
β+) β if(π β€ π‘, π , π‘) β
β+) |
180 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β+ β§ π‘ β β+))
β π β
(LSubSpβπ)) |
181 | | rabexg 5293 |
. . . . . . . . . . . . 13
β’ (π β (LSubSpβπ) β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} β V) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β+ β§ π‘ β β+))
β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} β V) |
183 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β+
β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) = (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π}) |
184 | | breq2 5114 |
. . . . . . . . . . . . . 14
β’ (π = if(π β€ π‘, π , π‘) β ((((π΄π·π¦)β2) β (πβ2)) β€ π β (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘))) |
185 | 184 | rabbidv 3418 |
. . . . . . . . . . . . 13
β’ (π = if(π β€ π‘, π , π‘) β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π} = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)}) |
186 | 183, 185 | elrnmpt1s 5917 |
. . . . . . . . . . . 12
β’
((if(π β€ π‘, π , π‘) β β+ β§ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} β V) β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π})) |
187 | 179, 182,
186 | syl2an2 685 |
. . . . . . . . . . 11
β’ ((π β§ (π β β+ β§ π‘ β β+))
β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} β ran (π β β+ β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π})) |
188 | 146 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β β+ β§ π‘ β β+))
β πΉ = ran (π β β+
β¦ {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π})) |
189 | 187, 188 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ ((π β§ (π β β+ β§ π‘ β β+))
β {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ if(π β€ π‘, π , π‘)} β πΉ) |
190 | 178, 189 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((π β§ (π β β+ β§ π‘ β β+))
β {π¦ β π β£ ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘)} β πΉ) |
191 | | ineq12 4172 |
. . . . . . . . . . 11
β’ ((π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (π’ β© π£) = ({π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β© {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘})) |
192 | | inrab 4271 |
. . . . . . . . . . 11
β’ ({π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β© {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) = {π¦ β π β£ ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘)} |
193 | 191, 192 | eqtrdi 2793 |
. . . . . . . . . 10
β’ ((π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (π’ β© π£) = {π¦ β π β£ ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘)}) |
194 | 193 | eleq1d 2823 |
. . . . . . . . 9
β’ ((π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β ((π’ β© π£) β πΉ β {π¦ β π β£ ((((π΄π·π¦)β2) β (πβ2)) β€ π β§ (((π΄π·π¦)β2) β (πβ2)) β€ π‘)} β πΉ)) |
195 | 190, 194 | syl5ibrcom 247 |
. . . . . . . 8
β’ ((π β§ (π β β+ β§ π‘ β β+))
β ((π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (π’ β© π£) β πΉ)) |
196 | | vex 3452 |
. . . . . . . . . . 11
β’ π’ β V |
197 | 196 | inex1 5279 |
. . . . . . . . . 10
β’ (π’ β© π£) β V |
198 | 197 | pwid 4587 |
. . . . . . . . 9
β’ (π’ β© π£) β π« (π’ β© π£) |
199 | | inelcm 4429 |
. . . . . . . . 9
β’ (((π’ β© π£) β πΉ β§ (π’ β© π£) β π« (π’ β© π£)) β (πΉ β© π« (π’ β© π£)) β β
) |
200 | 198, 199 | mpan2 690 |
. . . . . . . 8
β’ ((π’ β© π£) β πΉ β (πΉ β© π« (π’ β© π£)) β β
) |
201 | 195, 200 | syl6 35 |
. . . . . . 7
β’ ((π β§ (π β β+ β§ π‘ β β+))
β ((π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (πΉ β© π« (π’ β© π£)) β β
)) |
202 | 201 | rexlimdvva 3206 |
. . . . . 6
β’ (π β (βπ β β+ βπ‘ β β+
(π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (πΉ β© π« (π’ β© π£)) β β
)) |
203 | 162, 202 | biimtrrid 242 |
. . . . 5
β’ (π β ((βπ β β+
π’ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π } β§ βπ‘ β β+ π£ = {π¦ β π β£ (((π΄π·π¦)β2) β (πβ2)) β€ π‘}) β (πΉ β© π« (π’ β© π£)) β β
)) |
204 | 161, 203 | sylbid 239 |
. . . 4
β’ (π β ((π’ β πΉ β§ π£ β πΉ) β (πΉ β© π« (π’ β© π£)) β β
)) |
205 | 204 | ralrimivv 3196 |
. . 3
β’ (π β βπ’ β πΉ βπ£ β πΉ (πΉ β© π« (π’ β© π£)) β β
) |
206 | 20, 138, 205 | 3jca 1129 |
. 2
β’ (π β (πΉ β β
β§ β
β πΉ β§ βπ’ β πΉ βπ£ β πΉ (πΉ β© π« (π’ β© π£)) β β
)) |
207 | | isfbas 23196 |
. . 3
β’ (π β (LSubSpβπ) β (πΉ β (fBasβπ) β (πΉ β π« π β§ (πΉ β β
β§ β
β πΉ β§ βπ’ β πΉ βπ£ β πΉ (πΉ β© π« (π’ β© π£)) β β
)))) |
208 | 3, 207 | syl 17 |
. 2
β’ (π β (πΉ β (fBasβπ) β (πΉ β π« π β§ (πΉ β β
β§ β
β πΉ β§ βπ’ β πΉ βπ£ β πΉ (πΉ β© π« (π’ β© π£)) β β
)))) |
209 | 10, 206, 208 | mpbir2and 712 |
1
β’ (π β πΉ β (fBasβπ)) |