Step | Hyp | Ref
| Expression |
1 | | impexp 452 |
. . . . . 6
β’ (((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π) β (π:ββΆπ β (βπ β β (πΏβ(πβπ)) β€ 1 β βπ β β (πβ(πβ(πβπ))) β€ π))) |
2 | | r19.35 3108 |
. . . . . . 7
β’
(βπ β
β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π) β (βπ β β (πΏβ(πβπ)) β€ 1 β βπ β β (πβ(πβ(πβπ))) β€ π)) |
3 | 2 | imbi2i 336 |
. . . . . 6
β’ ((π:ββΆπ β βπ β β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π)) β (π:ββΆπ β (βπ β β (πΏβ(πβπ)) β€ 1 β βπ β β (πβ(πβ(πβπ))) β€ π))) |
4 | 1, 3 | bitr4i 278 |
. . . . 5
β’ (((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π) β (π:ββΆπ β βπ β β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π))) |
5 | 4 | albii 1822 |
. . . 4
β’
(βπ((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π) β βπ(π:ββΆπ β βπ β β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π))) |
6 | | nnex 12167 |
. . . . . 6
β’ β
β V |
7 | | fveq2 6846 |
. . . . . . . 8
β’ (π¦ = (πβπ) β (πΏβπ¦) = (πΏβ(πβπ))) |
8 | 7 | breq1d 5119 |
. . . . . . 7
β’ (π¦ = (πβπ) β ((πΏβπ¦) β€ 1 β (πΏβ(πβπ)) β€ 1)) |
9 | | fveq2 6846 |
. . . . . . . . 9
β’ (π¦ = (πβπ) β (πβπ¦) = (πβ(πβπ))) |
10 | 9 | fveq2d 6850 |
. . . . . . . 8
β’ (π¦ = (πβπ) β (πβ(πβπ¦)) = (πβ(πβ(πβπ)))) |
11 | 10 | breq1d 5119 |
. . . . . . 7
β’ (π¦ = (πβπ) β ((πβ(πβπ¦)) β€ π β (πβ(πβ(πβπ))) β€ π)) |
12 | 8, 11 | imbi12d 345 |
. . . . . 6
β’ (π¦ = (πβπ) β (((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π) β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π))) |
13 | 6, 12 | ac6n 10429 |
. . . . 5
β’
(βπ(π:ββΆπ β βπ β β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π)) β βπ β β βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π)) |
14 | | nnre 12168 |
. . . . . . 7
β’ (π β β β π β
β) |
15 | 14 | anim1i 616 |
. . . . . 6
β’ ((π β β β§
βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π)) β (π β β β§ βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π))) |
16 | 15 | reximi2 3079 |
. . . . 5
β’
(βπ β
β βπ¦ β
π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π) β βπ β β βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π)) |
17 | 13, 16 | syl 17 |
. . . 4
β’
(βπ(π:ββΆπ β βπ β β ((πΏβ(πβπ)) β€ 1 β (πβ(πβ(πβπ))) β€ π)) β βπ β β βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π)) |
18 | 5, 17 | sylbi 216 |
. . 3
β’
(βπ((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π) β βπ β β βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π)) |
19 | | nmoubi.1 |
. . . 4
β’ π = (BaseSetβπ) |
20 | | nmoubi.y |
. . . 4
β’ π = (BaseSetβπ) |
21 | | nmoubi.l |
. . . 4
β’ πΏ =
(normCVβπ) |
22 | | nmoubi.m |
. . . 4
β’ π =
(normCVβπ) |
23 | | nmoubi.3 |
. . . 4
β’ π = (π normOpOLD π) |
24 | | nmoubi.u |
. . . 4
β’ π β NrmCVec |
25 | | nmoubi.w |
. . . 4
β’ π β NrmCVec |
26 | 19, 20, 21, 22, 23, 24, 25 | nmobndi 29766 |
. . 3
β’ (π:πβΆπ β ((πβπ) β β β βπ β β βπ¦ β π ((πΏβπ¦) β€ 1 β (πβ(πβπ¦)) β€ π))) |
27 | 18, 26 | syl5ibr 246 |
. 2
β’ (π:πβΆπ β (βπ((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π) β (πβπ) β β)) |
28 | 27 | imp 408 |
1
β’ ((π:πβΆπ β§ βπ((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π)) β (πβπ) β β) |