Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’ βͺ π½ =
βͺ π½ |
2 | 1 | restin 22540 |
. 2
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) = (π½ βΎt (π΄ β© βͺ π½))) |
3 | | simpll 766 |
. . . . . 6
β’ (((π½ β CNrm β§ π΄ β π) β§ π₯ β π« (π΄ β© βͺ π½)) β π½ β CNrm) |
4 | | elpwi 4571 |
. . . . . . 7
β’ (π₯ β π« (π΄ β© βͺ π½)
β π₯ β (π΄ β© βͺ π½)) |
5 | 4 | adantl 483 |
. . . . . 6
β’ (((π½ β CNrm β§ π΄ β π) β§ π₯ β π« (π΄ β© βͺ π½)) β π₯ β (π΄ β© βͺ π½)) |
6 | | inex1g 5280 |
. . . . . . 7
β’ (π΄ β π β (π΄ β© βͺ π½) β V) |
7 | 6 | ad2antlr 726 |
. . . . . 6
β’ (((π½ β CNrm β§ π΄ β π) β§ π₯ β π« (π΄ β© βͺ π½)) β (π΄ β© βͺ π½) β V) |
8 | | restabs 22539 |
. . . . . 6
β’ ((π½ β CNrm β§ π₯ β (π΄ β© βͺ π½) β§ (π΄ β© βͺ π½) β V) β ((π½ βΎt (π΄ β© βͺ π½))
βΎt π₯) =
(π½ βΎt
π₯)) |
9 | 3, 5, 7, 8 | syl3anc 1372 |
. . . . 5
β’ (((π½ β CNrm β§ π΄ β π) β§ π₯ β π« (π΄ β© βͺ π½)) β ((π½ βΎt (π΄ β© βͺ π½)) βΎt π₯) = (π½ βΎt π₯)) |
10 | | cnrmi 22734 |
. . . . . 6
β’ ((π½ β CNrm β§ π₯ β π« (π΄ β© βͺ π½))
β (π½
βΎt π₯)
β Nrm) |
11 | 10 | adantlr 714 |
. . . . 5
β’ (((π½ β CNrm β§ π΄ β π) β§ π₯ β π« (π΄ β© βͺ π½)) β (π½ βΎt π₯) β Nrm) |
12 | 9, 11 | eqeltrd 2834 |
. . . 4
β’ (((π½ β CNrm β§ π΄ β π) β§ π₯ β π« (π΄ β© βͺ π½)) β ((π½ βΎt (π΄ β© βͺ π½)) βΎt π₯) β Nrm) |
13 | 12 | ralrimiva 3140 |
. . 3
β’ ((π½ β CNrm β§ π΄ β π) β βπ₯ β π« (π΄ β© βͺ π½)((π½ βΎt (π΄ β© βͺ π½)) βΎt π₯) β Nrm) |
14 | | cnrmtop 22711 |
. . . . . . 7
β’ (π½ β CNrm β π½ β Top) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π½ β CNrm β§ π΄ β π) β π½ β Top) |
16 | | toptopon2 22290 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
17 | 15, 16 | sylib 217 |
. . . . 5
β’ ((π½ β CNrm β§ π΄ β π) β π½ β (TopOnββͺ π½)) |
18 | | inss2 4193 |
. . . . 5
β’ (π΄ β© βͺ π½)
β βͺ π½ |
19 | | resttopon 22535 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ (π΄ β© βͺ π½)
β βͺ π½) β (π½ βΎt (π΄ β© βͺ π½)) β (TopOnβ(π΄ β© βͺ π½))) |
20 | 17, 18, 19 | sylancl 587 |
. . . 4
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt (π΄ β© βͺ π½)) β (TopOnβ(π΄ β© βͺ π½))) |
21 | | iscnrm2 22712 |
. . . 4
β’ ((π½ βΎt (π΄ β© βͺ π½))
β (TopOnβ(π΄
β© βͺ π½)) β ((π½ βΎt (π΄ β© βͺ π½)) β CNrm β
βπ₯ β π«
(π΄ β© βͺ π½)((π½ βΎt (π΄ β© βͺ π½)) βΎt π₯) β Nrm)) |
22 | 20, 21 | syl 17 |
. . 3
β’ ((π½ β CNrm β§ π΄ β π) β ((π½ βΎt (π΄ β© βͺ π½)) β CNrm β
βπ₯ β π«
(π΄ β© βͺ π½)((π½ βΎt (π΄ β© βͺ π½)) βΎt π₯) β Nrm)) |
23 | 13, 22 | mpbird 257 |
. 2
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt (π΄ β© βͺ π½)) β CNrm) |
24 | 2, 23 | eqeltrd 2834 |
1
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β CNrm) |