Step | Hyp | Ref
| Expression |
1 | | minveco.r |
. . 3
β’ π
= ran (π¦ β π β¦ (πβ(π΄ππ¦))) |
2 | | minveco.u |
. . . . . . . 8
β’ (π β π β
CPreHilOLD) |
3 | | phnv 29798 |
. . . . . . . 8
β’ (π β CPreHilOLD
β π β
NrmCVec) |
4 | 2, 3 | syl 17 |
. . . . . . 7
β’ (π β π β NrmCVec) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β π) β π β NrmCVec) |
6 | | minveco.a |
. . . . . . . 8
β’ (π β π΄ β π) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π΄ β π) |
8 | | minveco.w |
. . . . . . . . . . 11
β’ (π β π β ((SubSpβπ) β© CBan)) |
9 | | elin 3927 |
. . . . . . . . . . 11
β’ (π β ((SubSpβπ) β© CBan) β (π β (SubSpβπ) β§ π β CBan)) |
10 | 8, 9 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π β (SubSpβπ) β§ π β CBan)) |
11 | 10 | simpld 496 |
. . . . . . . . 9
β’ (π β π β (SubSpβπ)) |
12 | | minveco.x |
. . . . . . . . . 10
β’ π = (BaseSetβπ) |
13 | | minveco.y |
. . . . . . . . . 10
β’ π = (BaseSetβπ) |
14 | | eqid 2733 |
. . . . . . . . . 10
β’
(SubSpβπ) =
(SubSpβπ) |
15 | 12, 13, 14 | sspba 29711 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β π) |
16 | 4, 11, 15 | syl2anc 585 |
. . . . . . . 8
β’ (π β π β π) |
17 | 16 | sselda 3945 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π¦ β π) |
18 | | minveco.m |
. . . . . . . 8
β’ π = ( βπ£
βπ) |
19 | 12, 18 | nvmcl 29630 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π¦ β π) β (π΄ππ¦) β π) |
20 | 5, 7, 17, 19 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π΄ππ¦) β π) |
21 | | minveco.n |
. . . . . . 7
β’ π =
(normCVβπ) |
22 | 12, 21 | nvcl 29645 |
. . . . . 6
β’ ((π β NrmCVec β§ (π΄ππ¦) β π) β (πβ(π΄ππ¦)) β β) |
23 | 5, 20, 22 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β π) β (πβ(π΄ππ¦)) β β) |
24 | 23 | fmpttd 7064 |
. . . 4
β’ (π β (π¦ β π β¦ (πβ(π΄ππ¦))):πβΆβ) |
25 | 24 | frnd 6677 |
. . 3
β’ (π β ran (π¦ β π β¦ (πβ(π΄ππ¦))) β β) |
26 | 1, 25 | eqsstrid 3993 |
. 2
β’ (π β π
β β) |
27 | 10 | simprd 497 |
. . . . . 6
β’ (π β π β CBan) |
28 | | bnnv 29850 |
. . . . . 6
β’ (π β CBan β π β
NrmCVec) |
29 | | eqid 2733 |
. . . . . . 7
β’
(0vecβπ) = (0vecβπ) |
30 | 13, 29 | nvzcl 29618 |
. . . . . 6
β’ (π β NrmCVec β
(0vecβπ)
β π) |
31 | 27, 28, 30 | 3syl 18 |
. . . . 5
β’ (π β
(0vecβπ)
β π) |
32 | | fvex 6856 |
. . . . . 6
β’ (πβ(π΄ππ¦)) β V |
33 | | eqid 2733 |
. . . . . 6
β’ (π¦ β π β¦ (πβ(π΄ππ¦))) = (π¦ β π β¦ (πβ(π΄ππ¦))) |
34 | 32, 33 | dmmpti 6646 |
. . . . 5
β’ dom
(π¦ β π β¦ (πβ(π΄ππ¦))) = π |
35 | 31, 34 | eleqtrrdi 2845 |
. . . 4
β’ (π β
(0vecβπ)
β dom (π¦ β π β¦ (πβ(π΄ππ¦)))) |
36 | 35 | ne0d 4296 |
. . 3
β’ (π β dom (π¦ β π β¦ (πβ(π΄ππ¦))) β β
) |
37 | | dm0rn0 5881 |
. . . . 5
β’ (dom
(π¦ β π β¦ (πβ(π΄ππ¦))) = β
β ran (π¦ β π β¦ (πβ(π΄ππ¦))) = β
) |
38 | 1 | eqeq1i 2738 |
. . . . 5
β’ (π
= β
β ran (π¦ β π β¦ (πβ(π΄ππ¦))) = β
) |
39 | 37, 38 | bitr4i 278 |
. . . 4
β’ (dom
(π¦ β π β¦ (πβ(π΄ππ¦))) = β
β π
= β
) |
40 | 39 | necon3bii 2993 |
. . 3
β’ (dom
(π¦ β π β¦ (πβ(π΄ππ¦))) β β
β π
β β
) |
41 | 36, 40 | sylib 217 |
. 2
β’ (π β π
β β
) |
42 | 12, 21 | nvge0 29657 |
. . . . . 6
β’ ((π β NrmCVec β§ (π΄ππ¦) β π) β 0 β€ (πβ(π΄ππ¦))) |
43 | 5, 20, 42 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β π) β 0 β€ (πβ(π΄ππ¦))) |
44 | 43 | ralrimiva 3140 |
. . . 4
β’ (π β βπ¦ β π 0 β€ (πβ(π΄ππ¦))) |
45 | 32 | rgenw 3065 |
. . . . 5
β’
βπ¦ β
π (πβ(π΄ππ¦)) β V |
46 | | breq2 5110 |
. . . . . 6
β’ (π€ = (πβ(π΄ππ¦)) β (0 β€ π€ β 0 β€ (πβ(π΄ππ¦)))) |
47 | 33, 46 | ralrnmptw 7045 |
. . . . 5
β’
(βπ¦ β
π (πβ(π΄ππ¦)) β V β (βπ€ β ran (π¦ β π β¦ (πβ(π΄ππ¦)))0 β€ π€ β βπ¦ β π 0 β€ (πβ(π΄ππ¦)))) |
48 | 45, 47 | ax-mp 5 |
. . . 4
β’
(βπ€ β
ran (π¦ β π β¦ (πβ(π΄ππ¦)))0 β€ π€ β βπ¦ β π 0 β€ (πβ(π΄ππ¦))) |
49 | 44, 48 | sylibr 233 |
. . 3
β’ (π β βπ€ β ran (π¦ β π β¦ (πβ(π΄ππ¦)))0 β€ π€) |
50 | 1 | raleqi 3310 |
. . 3
β’
(βπ€ β
π
0 β€ π€ β βπ€ β ran (π¦ β π β¦ (πβ(π΄ππ¦)))0 β€ π€) |
51 | 49, 50 | sylibr 233 |
. 2
β’ (π β βπ€ β π
0 β€ π€) |
52 | 26, 41, 51 | 3jca 1129 |
1
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |