Step | Hyp | Ref
| Expression |
1 | | isblo3i.u |
. . . 4
β’ π β NrmCVec |
2 | | isblo3i.w |
. . . 4
β’ π β NrmCVec |
3 | | isblo3i.4 |
. . . . 5
β’ πΏ = (π LnOp π) |
4 | | isblo3i.5 |
. . . . 5
β’ π΅ = (π BLnOp π) |
5 | 3, 4 | bloln 29790 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π β πΏ) |
6 | 1, 2, 5 | mp3an12 1452 |
. . 3
β’ (π β π΅ β π β πΏ) |
7 | | isblo3i.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
8 | | eqid 2732 |
. . . . . 6
β’
(BaseSetβπ) =
(BaseSetβπ) |
9 | | eqid 2732 |
. . . . . 6
β’ (π normOpOLD π) = (π normOpOLD π) |
10 | 7, 8, 9, 4 | nmblore 29792 |
. . . . 5
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β ((π normOpOLD π)βπ) β β) |
11 | 1, 2, 10 | mp3an12 1452 |
. . . 4
β’ (π β π΅ β ((π normOpOLD π)βπ) β β) |
12 | | isblo3i.m |
. . . . . 6
β’ π =
(normCVβπ) |
13 | | isblo3i.n |
. . . . . 6
β’ π =
(normCVβπ) |
14 | 7, 12, 13, 9, 4, 1,
2 | nmblolbi 29806 |
. . . . 5
β’ ((π β π΅ β§ π¦ β π) β (πβ(πβπ¦)) β€ (((π normOpOLD π)βπ) Β· (πβπ¦))) |
15 | 14 | ralrimiva 3140 |
. . . 4
β’ (π β π΅ β βπ¦ β π (πβ(πβπ¦)) β€ (((π normOpOLD π)βπ) Β· (πβπ¦))) |
16 | | oveq1 7370 |
. . . . . . 7
β’ (π₯ = ((π normOpOLD π)βπ) β (π₯ Β· (πβπ¦)) = (((π normOpOLD π)βπ) Β· (πβπ¦))) |
17 | 16 | breq2d 5123 |
. . . . . 6
β’ (π₯ = ((π normOpOLD π)βπ) β ((πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦)) β (πβ(πβπ¦)) β€ (((π normOpOLD π)βπ) Β· (πβπ¦)))) |
18 | 17 | ralbidv 3171 |
. . . . 5
β’ (π₯ = ((π normOpOLD π)βπ) β (βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦)) β βπ¦ β π (πβ(πβπ¦)) β€ (((π normOpOLD π)βπ) Β· (πβπ¦)))) |
19 | 18 | rspcev 3583 |
. . . 4
β’ ((((π normOpOLD π)βπ) β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (((π normOpOLD π)βπ) Β· (πβπ¦))) β βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) |
20 | 11, 15, 19 | syl2anc 585 |
. . 3
β’ (π β π΅ β βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) |
21 | 6, 20 | jca 513 |
. 2
β’ (π β π΅ β (π β πΏ β§ βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦)))) |
22 | | simp1 1137 |
. . . . 5
β’ ((π β πΏ β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β π β πΏ) |
23 | 7, 8, 3 | lnof 29761 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π:πβΆ(BaseSetβπ)) |
24 | 1, 2, 23 | mp3an12 1452 |
. . . . . 6
β’ (π β πΏ β π:πβΆ(BaseSetβπ)) |
25 | 7, 8, 9 | nmoxr 29772 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆ(BaseSetβπ)) β ((π normOpOLD π)βπ) β
β*) |
26 | 1, 2, 25 | mp3an12 1452 |
. . . . . . . 8
β’ (π:πβΆ(BaseSetβπ) β ((π normOpOLD π)βπ) β
β*) |
27 | 26 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π:πβΆ(BaseSetβπ) β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β ((π normOpOLD π)βπ) β
β*) |
28 | | recn 11151 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β
β) |
29 | 28 | abscld 15334 |
. . . . . . . . 9
β’ (π₯ β β β
(absβπ₯) β
β) |
30 | 29 | rexrd 11215 |
. . . . . . . 8
β’ (π₯ β β β
(absβπ₯) β
β*) |
31 | 30 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π:πβΆ(BaseSetβπ) β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β (absβπ₯) β
β*) |
32 | | pnfxr 11219 |
. . . . . . . 8
β’ +β
β β* |
33 | 32 | a1i 11 |
. . . . . . 7
β’ ((π:πβΆ(BaseSetβπ) β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β +β β
β*) |
34 | 7, 8, 12, 13, 9, 1, 2 | nmoub3i 29779 |
. . . . . . 7
β’ ((π:πβΆ(BaseSetβπ) β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β ((π normOpOLD π)βπ) β€ (absβπ₯)) |
35 | | ltpnf 13051 |
. . . . . . . . 9
β’
((absβπ₯)
β β β (absβπ₯) < +β) |
36 | 29, 35 | syl 17 |
. . . . . . . 8
β’ (π₯ β β β
(absβπ₯) <
+β) |
37 | 36 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π:πβΆ(BaseSetβπ) β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β (absβπ₯) < +β) |
38 | 27, 31, 33, 34, 37 | xrlelttrd 13090 |
. . . . . 6
β’ ((π:πβΆ(BaseSetβπ) β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β ((π normOpOLD π)βπ) < +β) |
39 | 24, 38 | syl3an1 1164 |
. . . . 5
β’ ((π β πΏ β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β ((π normOpOLD π)βπ) < +β) |
40 | 9, 3, 4 | isblo 29788 |
. . . . . 6
β’ ((π β NrmCVec β§ π β NrmCVec) β (π β π΅ β (π β πΏ β§ ((π normOpOLD π)βπ) < +β))) |
41 | 1, 2, 40 | mp2an 691 |
. . . . 5
β’ (π β π΅ β (π β πΏ β§ ((π normOpOLD π)βπ) < +β)) |
42 | 22, 39, 41 | sylanbrc 584 |
. . . 4
β’ ((π β πΏ β§ π₯ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β π β π΅) |
43 | 42 | rexlimdv3a 3153 |
. . 3
β’ (π β πΏ β (βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦)) β π β π΅)) |
44 | 43 | imp 408 |
. 2
β’ ((π β πΏ β§ βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦))) β π β π΅) |
45 | 21, 44 | impbii 208 |
1
β’ (π β π΅ β (π β πΏ β§ βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦)))) |