Step | Hyp | Ref
| Expression |
1 | | cphngp 24553 |
. . . . . . . 8
β’ (π β βPreHil β
π β
NrmGrp) |
2 | | ngptps 23974 |
. . . . . . . 8
β’ (π β NrmGrp β π β TopSp) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π β βPreHil β
π β
TopSp) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β βPreHil β§
π β π) β π β TopSp) |
5 | | clsocv.v |
. . . . . . 7
β’ π = (Baseβπ) |
6 | | clsocv.j |
. . . . . . 7
β’ π½ = (TopOpenβπ) |
7 | 5, 6 | istps 22299 |
. . . . . 6
β’ (π β TopSp β π½ β (TopOnβπ)) |
8 | 4, 7 | sylib 217 |
. . . . 5
β’ ((π β βPreHil β§
π β π) β π½ β (TopOnβπ)) |
9 | | topontop 22278 |
. . . . 5
β’ (π½ β (TopOnβπ) β π½ β Top) |
10 | 8, 9 | syl 17 |
. . . 4
β’ ((π β βPreHil β§
π β π) β π½ β Top) |
11 | | simpr 486 |
. . . . 5
β’ ((π β βPreHil β§
π β π) β π β π) |
12 | | toponuni 22279 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
13 | 8, 12 | syl 17 |
. . . . 5
β’ ((π β βPreHil β§
π β π) β π = βͺ π½) |
14 | 11, 13 | sseqtrd 3985 |
. . . 4
β’ ((π β βPreHil β§
π β π) β π β βͺ π½) |
15 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
16 | 15 | sscls 22423 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½)
β π β
((clsβπ½)βπ)) |
17 | 10, 14, 16 | syl2anc 585 |
. . 3
β’ ((π β βPreHil β§
π β π) β π β ((clsβπ½)βπ)) |
18 | | clsocv.o |
. . . 4
β’ π = (ocvβπ) |
19 | 18 | ocv2ss 21093 |
. . 3
β’ (π β ((clsβπ½)βπ) β (πβ((clsβπ½)βπ)) β (πβπ)) |
20 | 17, 19 | syl 17 |
. 2
β’ ((π β βPreHil β§
π β π) β (πβ((clsβπ½)βπ)) β (πβπ)) |
21 | 15 | clsss3 22426 |
. . . . . 6
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ) β βͺ π½) |
22 | 10, 14, 21 | syl2anc 585 |
. . . . 5
β’ ((π β βPreHil β§
π β π) β ((clsβπ½)βπ) β βͺ π½) |
23 | 22, 13 | sseqtrrd 3986 |
. . . 4
β’ ((π β βPreHil β§
π β π) β ((clsβπ½)βπ) β π) |
24 | 23 | adantr 482 |
. . 3
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β ((clsβπ½)βπ) β π) |
25 | 5, 18 | ocvss 21090 |
. . . . 5
β’ (πβπ) β π |
26 | 25 | a1i 11 |
. . . 4
β’ ((π β βPreHil β§
π β π) β (πβπ) β π) |
27 | 26 | sselda 3945 |
. . 3
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β π₯ β π) |
28 | | df-ss 3928 |
. . . . . . . . . 10
β’
(((clsβπ½)βπ) β π β (((clsβπ½)βπ) β© π) = ((clsβπ½)βπ)) |
29 | 24, 28 | sylib 217 |
. . . . . . . . 9
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (((clsβπ½)βπ) β© π) = ((clsβπ½)βπ)) |
30 | 29 | ineq1d 4172 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β ((((clsβπ½)βπ) β© π) β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = (((clsβπ½)βπ) β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))})) |
31 | | dfrab3 4270 |
. . . . . . . . . 10
β’ {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} = (π β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
32 | 31 | ineq2i 4170 |
. . . . . . . . 9
β’
(((clsβπ½)βπ) β© {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = (((clsβπ½)βπ) β© (π β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))})) |
33 | | inass 4180 |
. . . . . . . . 9
β’
((((clsβπ½)βπ) β© π) β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = (((clsβπ½)βπ) β© (π β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))})) |
34 | 32, 33 | eqtr4i 2764 |
. . . . . . . 8
β’
(((clsβπ½)βπ) β© {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = ((((clsβπ½)βπ) β© π) β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
35 | | dfrab3 4270 |
. . . . . . . 8
β’ {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} = (((clsβπ½)βπ) β© {π¦ β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
36 | 30, 34, 35 | 3eqtr4g 2798 |
. . . . . . 7
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (((clsβπ½)βπ) β© {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
37 | 15 | clscld 22414 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ) β (Clsdβπ½)) |
38 | 10, 14, 37 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β βPreHil β§
π β π) β ((clsβπ½)βπ) β (Clsdβπ½)) |
39 | 38 | adantr 482 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β ((clsβπ½)βπ) β (Clsdβπ½)) |
40 | | fvex 6856 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) β V |
41 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π¦ β π β¦ (π₯(Β·πβπ)π¦)) = (π¦ β π β¦ (π₯(Β·πβπ)π¦)) |
42 | 41 | mptiniseg 6192 |
. . . . . . . . . 10
β’
((0gβ(Scalarβπ)) β V β (β‘(π¦ β π β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) = {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
43 | 40, 42 | ax-mp 5 |
. . . . . . . . 9
β’ (β‘(π¦ β π β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) = {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} |
44 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
45 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Β·πβπ) =
(Β·πβπ) |
46 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β π β βPreHil) |
47 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β π½ β (TopOnβπ)) |
48 | 47, 47, 27 | cnmptc 23029 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (π¦ β π β¦ π₯) β (π½ Cn π½)) |
49 | 47 | cnmptid 23028 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (π¦ β π β¦ π¦) β (π½ Cn π½)) |
50 | 6, 44, 45, 46, 47, 48, 49 | cnmpt1ip 24627 |
. . . . . . . . . 10
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (π¦ β π β¦ (π₯(Β·πβπ)π¦)) β (π½ Cn
(TopOpenββfld))) |
51 | 44 | cnfldhaus 24164 |
. . . . . . . . . . 11
β’
(TopOpenββfld) β Haus |
52 | | cphclm 24569 |
. . . . . . . . . . . . . 14
β’ (π β βPreHil β
π β
βMod) |
53 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Scalarβπ) =
(Scalarβπ) |
54 | 53 | clm0 24451 |
. . . . . . . . . . . . . 14
β’ (π β βMod β 0 =
(0gβ(Scalarβπ))) |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β βPreHil β 0 =
(0gβ(Scalarβπ))) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β 0 =
(0gβ(Scalarβπ))) |
57 | | 0cn 11152 |
. . . . . . . . . . . 12
β’ 0 β
β |
58 | 56, 57 | eqeltrrdi 2843 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β
(0gβ(Scalarβπ)) β β) |
59 | | unicntop 24165 |
. . . . . . . . . . . 12
β’ β =
βͺ
(TopOpenββfld) |
60 | 59 | sncld 22738 |
. . . . . . . . . . 11
β’
(((TopOpenββfld) β Haus β§
(0gβ(Scalarβπ)) β β) β
{(0gβ(Scalarβπ))} β
(Clsdβ(TopOpenββfld))) |
61 | 51, 58, 60 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β
{(0gβ(Scalarβπ))} β
(Clsdβ(TopOpenββfld))) |
62 | | cnclima 22635 |
. . . . . . . . . 10
β’ (((π¦ β π β¦ (π₯(Β·πβπ)π¦)) β (π½ Cn (TopOpenββfld))
β§ {(0gβ(Scalarβπ))} β
(Clsdβ(TopOpenββfld))) β (β‘(π¦ β π β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) β (Clsdβπ½)) |
63 | 50, 61, 62 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (β‘(π¦ β π β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) β (Clsdβπ½)) |
64 | 43, 63 | eqeltrrid 2839 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) |
65 | | incld 22410 |
. . . . . . . 8
β’
((((clsβπ½)βπ) β (Clsdβπ½) β§ {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) β (((clsβπ½)βπ) β© {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) β (Clsdβπ½)) |
66 | 39, 64, 65 | syl2anc 585 |
. . . . . . 7
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β (((clsβπ½)βπ) β© {π¦ β π β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) β (Clsdβπ½)) |
67 | 36, 66 | eqeltrrd 2835 |
. . . . . 6
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) |
68 | 17 | adantr 482 |
. . . . . . 7
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β π β ((clsβπ½)βπ)) |
69 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
70 | 5, 45, 53, 69, 18 | ocvi 21089 |
. . . . . . . . 9
β’ ((π₯ β (πβπ) β§ π¦ β π) β (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
71 | 70 | ralrimiva 3140 |
. . . . . . . 8
β’ (π₯ β (πβπ) β βπ¦ β π (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
72 | 71 | adantl 483 |
. . . . . . 7
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β βπ¦ β π (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
73 | | ssrab 4031 |
. . . . . . 7
β’ (π β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (π β ((clsβπ½)βπ) β§ βπ¦ β π (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
74 | 68, 72, 73 | sylanbrc 584 |
. . . . . 6
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β π β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
75 | 15 | clsss2 22439 |
. . . . . 6
β’ (({π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½) β§ π β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) β ((clsβπ½)βπ) β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
76 | 67, 74, 75 | syl2anc 585 |
. . . . 5
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β ((clsβπ½)βπ) β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
77 | | ssrab2 4038 |
. . . . . 6
β’ {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β ((clsβπ½)βπ) |
78 | 77 | a1i 11 |
. . . . 5
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β ((clsβπ½)βπ)) |
79 | 76, 78 | eqssd 3962 |
. . . 4
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β ((clsβπ½)βπ) = {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
80 | | rabid2 3435 |
. . . 4
β’
(((clsβπ½)βπ) = {π¦ β ((clsβπ½)βπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β βπ¦ β ((clsβπ½)βπ)(π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
81 | 79, 80 | sylib 217 |
. . 3
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β βπ¦ β ((clsβπ½)βπ)(π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
82 | 5, 45, 53, 69, 18 | elocv 21088 |
. . 3
β’ (π₯ β (πβ((clsβπ½)βπ)) β (((clsβπ½)βπ) β π β§ π₯ β π β§ βπ¦ β ((clsβπ½)βπ)(π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
83 | 24, 27, 81, 82 | syl3anbrc 1344 |
. 2
β’ (((π β βPreHil β§
π β π) β§ π₯ β (πβπ)) β π₯ β (πβ((clsβπ½)βπ))) |
84 | 20, 83 | eqelssd 3966 |
1
β’ ((π β βPreHil β§
π β π) β (πβ((clsβπ½)βπ)) = (πβπ)) |