Step | Hyp | Ref
| Expression |
1 | | minvec.r |
. . 3
β’ π
= ran (π¦ β π β¦ (πβ(π΄ β π¦))) |
2 | | minvec.u |
. . . . . . 7
β’ (π β π β βPreHil) |
3 | | cphngp 24553 |
. . . . . . 7
β’ (π β βPreHil β
π β
NrmGrp) |
4 | 2, 3 | syl 17 |
. . . . . 6
β’ (π β π β NrmGrp) |
5 | | cphlmod 24554 |
. . . . . . . . 9
β’ (π β βPreHil β
π β
LMod) |
6 | 2, 5 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π β LMod) |
8 | | minvec.a |
. . . . . . . 8
β’ (π β π΄ β π) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π΄ β π) |
10 | | minvec.y |
. . . . . . . . 9
β’ (π β π β (LSubSpβπ)) |
11 | | minvec.x |
. . . . . . . . . 10
β’ π = (Baseβπ) |
12 | | eqid 2737 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
13 | 11, 12 | lssss 20413 |
. . . . . . . . 9
β’ (π β (LSubSpβπ) β π β π) |
14 | 10, 13 | syl 17 |
. . . . . . . 8
β’ (π β π β π) |
15 | 14 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π¦ β π) |
16 | | minvec.m |
. . . . . . . 8
β’ β =
(-gβπ) |
17 | 11, 16 | lmodvsubcl 20383 |
. . . . . . 7
β’ ((π β LMod β§ π΄ β π β§ π¦ β π) β (π΄ β π¦) β π) |
18 | 7, 9, 15, 17 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π΄ β π¦) β π) |
19 | | minvec.n |
. . . . . . 7
β’ π = (normβπ) |
20 | 11, 19 | nmcl 23988 |
. . . . . 6
β’ ((π β NrmGrp β§ (π΄ β π¦) β π) β (πβ(π΄ β π¦)) β β) |
21 | 4, 18, 20 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π¦ β π) β (πβ(π΄ β π¦)) β β) |
22 | 21 | fmpttd 7068 |
. . . 4
β’ (π β (π¦ β π β¦ (πβ(π΄ β π¦))):πβΆβ) |
23 | 22 | frnd 6681 |
. . 3
β’ (π β ran (π¦ β π β¦ (πβ(π΄ β π¦))) β β) |
24 | 1, 23 | eqsstrid 3997 |
. 2
β’ (π β π
β β) |
25 | 12 | lssn0 20417 |
. . . 4
β’ (π β (LSubSpβπ) β π β β
) |
26 | 10, 25 | syl 17 |
. . 3
β’ (π β π β β
) |
27 | 1 | eqeq1i 2742 |
. . . . 5
β’ (π
= β
β ran (π¦ β π β¦ (πβ(π΄ β π¦))) = β
) |
28 | | dm0rn0 5885 |
. . . . 5
β’ (dom
(π¦ β π β¦ (πβ(π΄ β π¦))) = β
β ran (π¦ β π β¦ (πβ(π΄ β π¦))) = β
) |
29 | | fvex 6860 |
. . . . . . 7
β’ (πβ(π΄ β π¦)) β V |
30 | | eqid 2737 |
. . . . . . 7
β’ (π¦ β π β¦ (πβ(π΄ β π¦))) = (π¦ β π β¦ (πβ(π΄ β π¦))) |
31 | 29, 30 | dmmpti 6650 |
. . . . . 6
β’ dom
(π¦ β π β¦ (πβ(π΄ β π¦))) = π |
32 | 31 | eqeq1i 2742 |
. . . . 5
β’ (dom
(π¦ β π β¦ (πβ(π΄ β π¦))) = β
β π = β
) |
33 | 27, 28, 32 | 3bitr2i 299 |
. . . 4
β’ (π
= β
β π = β
) |
34 | 33 | necon3bii 2997 |
. . 3
β’ (π
β β
β π β β
) |
35 | 26, 34 | sylibr 233 |
. 2
β’ (π β π
β β
) |
36 | 11, 19 | nmge0 23989 |
. . . . . 6
β’ ((π β NrmGrp β§ (π΄ β π¦) β π) β 0 β€ (πβ(π΄ β π¦))) |
37 | 4, 18, 36 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π¦ β π) β 0 β€ (πβ(π΄ β π¦))) |
38 | 37 | ralrimiva 3144 |
. . . 4
β’ (π β βπ¦ β π 0 β€ (πβ(π΄ β π¦))) |
39 | 29 | rgenw 3069 |
. . . . 5
β’
βπ¦ β
π (πβ(π΄ β π¦)) β V |
40 | | breq2 5114 |
. . . . . 6
β’ (π€ = (πβ(π΄ β π¦)) β (0 β€ π€ β 0 β€ (πβ(π΄ β π¦)))) |
41 | 30, 40 | ralrnmptw 7049 |
. . . . 5
β’
(βπ¦ β
π (πβ(π΄ β π¦)) β V β (βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))0 β€ π€ β βπ¦ β π 0 β€ (πβ(π΄ β π¦)))) |
42 | 39, 41 | ax-mp 5 |
. . . 4
β’
(βπ€ β
ran (π¦ β π β¦ (πβ(π΄ β π¦)))0 β€ π€ β βπ¦ β π 0 β€ (πβ(π΄ β π¦))) |
43 | 38, 42 | sylibr 233 |
. . 3
β’ (π β βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))0 β€ π€) |
44 | 1 | raleqi 3314 |
. . 3
β’
(βπ€ β
π
0 β€ π€ β βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))0 β€ π€) |
45 | 43, 44 | sylibr 233 |
. 2
β’ (π β βπ€ β π
0 β€ π€) |
46 | 24, 35, 45 | 3jca 1129 |
1
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |