Step | Hyp | Ref
| Expression |
1 | | nmoubi.u |
. . . . . . . . . . . . 13
β’ π β NrmCVec |
2 | | nmoubi.1 |
. . . . . . . . . . . . . 14
β’ π = (BaseSetβπ) |
3 | | nmoubi.l |
. . . . . . . . . . . . . 14
β’ πΏ =
(normCVβπ) |
4 | 2, 3 | nvcl 29777 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ π₯ β π) β (πΏβπ₯) β β) |
5 | 1, 4 | mpan 688 |
. . . . . . . . . . . 12
β’ (π₯ β π β (πΏβπ₯) β β) |
6 | | remulcl 11177 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ (πΏβπ₯) β β) β (π΄ Β· (πΏβπ₯)) β β) |
7 | 5, 6 | sylan2 593 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π₯ β π) β (π΄ Β· (πΏβπ₯)) β β) |
8 | 7 | adantr 481 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β (π΄ Β· (πΏβπ₯)) β β) |
9 | | recn 11182 |
. . . . . . . . . . . . 13
β’ (π΄ β β β π΄ β
β) |
10 | 9 | abscld 15365 |
. . . . . . . . . . . 12
β’ (π΄ β β β
(absβπ΄) β
β) |
11 | | remulcl 11177 |
. . . . . . . . . . . 12
β’
(((absβπ΄)
β β β§ (πΏβπ₯) β β) β ((absβπ΄) Β· (πΏβπ₯)) β β) |
12 | 10, 5, 11 | syl2an 596 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π₯ β π) β ((absβπ΄) Β· (πΏβπ₯)) β β) |
13 | 12 | adantr 481 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β ((absβπ΄) Β· (πΏβπ₯)) β β) |
14 | 10 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β (absβπ΄) β β) |
15 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π₯ β π) β π΄ β β) |
16 | 10 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π₯ β π) β (absβπ΄) β β) |
17 | 2, 3 | nvge0 29789 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ π₯ β π) β 0 β€ (πΏβπ₯)) |
18 | 1, 17 | mpan 688 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β 0 β€ (πΏβπ₯)) |
19 | 5, 18 | jca 512 |
. . . . . . . . . . . . 13
β’ (π₯ β π β ((πΏβπ₯) β β β§ 0 β€ (πΏβπ₯))) |
20 | 19 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π₯ β π) β ((πΏβπ₯) β β β§ 0 β€ (πΏβπ₯))) |
21 | | leabs 15228 |
. . . . . . . . . . . . 13
β’ (π΄ β β β π΄ β€ (absβπ΄)) |
22 | 21 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π₯ β π) β π΄ β€ (absβπ΄)) |
23 | | lemul1a 12050 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(absβπ΄) β
β β§ ((πΏβπ₯) β β β§ 0 β€ (πΏβπ₯))) β§ π΄ β€ (absβπ΄)) β (π΄ Β· (πΏβπ₯)) β€ ((absβπ΄) Β· (πΏβπ₯))) |
24 | 15, 16, 20, 22, 23 | syl31anc 1373 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π₯ β π) β (π΄ Β· (πΏβπ₯)) β€ ((absβπ΄) Β· (πΏβπ₯))) |
25 | 24 | adantr 481 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β (π΄ Β· (πΏβπ₯)) β€ ((absβπ΄) Β· (πΏβπ₯))) |
26 | 5 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π₯ β π) β (πΏβπ₯) β β) |
27 | | 1red 11197 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π₯ β π) β 1 β β) |
28 | 9 | absge0d 15373 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β 0 β€
(absβπ΄)) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π₯ β π) β 0 β€ (absβπ΄)) |
30 | 16, 29 | jca 512 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π₯ β π) β ((absβπ΄) β β β§ 0 β€
(absβπ΄))) |
31 | 26, 27, 30 | 3jca 1128 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π₯ β π) β ((πΏβπ₯) β β β§ 1 β β β§
((absβπ΄) β
β β§ 0 β€ (absβπ΄)))) |
32 | | lemul2a 12051 |
. . . . . . . . . . . 12
β’ ((((πΏβπ₯) β β β§ 1 β β β§
((absβπ΄) β
β β§ 0 β€ (absβπ΄))) β§ (πΏβπ₯) β€ 1) β ((absβπ΄) Β· (πΏβπ₯)) β€ ((absβπ΄) Β· 1)) |
33 | 31, 32 | sylan 580 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β ((absβπ΄) Β· (πΏβπ₯)) β€ ((absβπ΄) Β· 1)) |
34 | 10 | recnd 11224 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
(absβπ΄) β
β) |
35 | 34 | mulridd 11213 |
. . . . . . . . . . . 12
β’ (π΄ β β β
((absβπ΄) Β· 1)
= (absβπ΄)) |
36 | 35 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β ((absβπ΄) Β· 1) = (absβπ΄)) |
37 | 33, 36 | breqtrd 5167 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β ((absβπ΄) Β· (πΏβπ₯)) β€ (absβπ΄)) |
38 | 8, 13, 14, 25, 37 | letrd 11353 |
. . . . . . . . 9
β’ (((π΄ β β β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β (π΄ Β· (πΏβπ₯)) β€ (absβπ΄)) |
39 | 38 | adantlll 716 |
. . . . . . . 8
β’ ((((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β (π΄ Β· (πΏβπ₯)) β€ (absβπ΄)) |
40 | | nmoubi.w |
. . . . . . . . . . . 12
β’ π β NrmCVec |
41 | | ffvelcdm 7068 |
. . . . . . . . . . . 12
β’ ((π:πβΆπ β§ π₯ β π) β (πβπ₯) β π) |
42 | | nmoubi.y |
. . . . . . . . . . . . 13
β’ π = (BaseSetβπ) |
43 | | nmoubi.m |
. . . . . . . . . . . . 13
β’ π =
(normCVβπ) |
44 | 42, 43 | nvcl 29777 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ (πβπ₯) β π) β (πβ(πβπ₯)) β β) |
45 | 40, 41, 44 | sylancr 587 |
. . . . . . . . . . 11
β’ ((π:πβΆπ β§ π₯ β π) β (πβ(πβπ₯)) β β) |
46 | 45 | adantlr 713 |
. . . . . . . . . 10
β’ (((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β (πβ(πβπ₯)) β β) |
47 | 7 | adantll 712 |
. . . . . . . . . 10
β’ (((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β (π΄ Β· (πΏβπ₯)) β β) |
48 | 10 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β (absβπ΄) β β) |
49 | | letr 11290 |
. . . . . . . . . 10
β’ (((πβ(πβπ₯)) β β β§ (π΄ Β· (πΏβπ₯)) β β β§ (absβπ΄) β β) β
(((πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β§ (π΄ Β· (πΏβπ₯)) β€ (absβπ΄)) β (πβ(πβπ₯)) β€ (absβπ΄))) |
50 | 46, 47, 48, 49 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β (((πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β§ (π΄ Β· (πΏβπ₯)) β€ (absβπ΄)) β (πβ(πβπ₯)) β€ (absβπ΄))) |
51 | 50 | adantr 481 |
. . . . . . . 8
β’ ((((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β (((πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β§ (π΄ Β· (πΏβπ₯)) β€ (absβπ΄)) β (πβ(πβπ₯)) β€ (absβπ΄))) |
52 | 39, 51 | mpan2d 692 |
. . . . . . 7
β’ ((((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β§ (πΏβπ₯) β€ 1) β ((πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβ(πβπ₯)) β€ (absβπ΄))) |
53 | 52 | ex 413 |
. . . . . 6
β’ (((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β ((πΏβπ₯) β€ 1 β ((πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβ(πβπ₯)) β€ (absβπ΄)))) |
54 | 53 | com23 86 |
. . . . 5
β’ (((π:πβΆπ β§ π΄ β β) β§ π₯ β π) β ((πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β ((πΏβπ₯) β€ 1 β (πβ(πβπ₯)) β€ (absβπ΄)))) |
55 | 54 | ralimdva 3166 |
. . . 4
β’ ((π:πβΆπ β§ π΄ β β) β (βπ₯ β π (πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β βπ₯ β π ((πΏβπ₯) β€ 1 β (πβ(πβπ₯)) β€ (absβπ΄)))) |
56 | 55 | imp 407 |
. . 3
β’ (((π:πβΆπ β§ π΄ β β) β§ βπ₯ β π (πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯))) β βπ₯ β π ((πΏβπ₯) β€ 1 β (πβ(πβπ₯)) β€ (absβπ΄))) |
57 | 10 | rexrd 11246 |
. . . . 5
β’ (π΄ β β β
(absβπ΄) β
β*) |
58 | | nmoubi.3 |
. . . . . 6
β’ π = (π normOpOLD π) |
59 | 2, 42, 3, 43, 58, 1, 40 | nmoubi 29888 |
. . . . 5
β’ ((π:πβΆπ β§ (absβπ΄) β β*) β ((πβπ) β€ (absβπ΄) β βπ₯ β π ((πΏβπ₯) β€ 1 β (πβ(πβπ₯)) β€ (absβπ΄)))) |
60 | 57, 59 | sylan2 593 |
. . . 4
β’ ((π:πβΆπ β§ π΄ β β) β ((πβπ) β€ (absβπ΄) β βπ₯ β π ((πΏβπ₯) β€ 1 β (πβ(πβπ₯)) β€ (absβπ΄)))) |
61 | 60 | biimpar 478 |
. . 3
β’ (((π:πβΆπ β§ π΄ β β) β§ βπ₯ β π ((πΏβπ₯) β€ 1 β (πβ(πβπ₯)) β€ (absβπ΄))) β (πβπ) β€ (absβπ΄)) |
62 | 56, 61 | syldan 591 |
. 2
β’ (((π:πβΆπ β§ π΄ β β) β§ βπ₯ β π (πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯))) β (πβπ) β€ (absβπ΄)) |
63 | 62 | 3impa 1110 |
1
β’ ((π:πβΆπ β§ π΄ β β β§ βπ₯ β π (πβ(πβπ₯)) β€ (π΄ Β· (πΏβπ₯))) β (πβπ) β€ (absβπ΄)) |