Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(ocvβπ) =
(ocvβπ) |
2 | | csscld.c |
. . . . 5
β’ πΆ = (ClSubSpβπ) |
3 | 1, 2 | cssi 21104 |
. . . 4
β’ (π β πΆ β π = ((ocvβπ)β((ocvβπ)βπ))) |
4 | 3 | adantl 483 |
. . 3
β’ ((π β βPreHil β§
π β πΆ) β π = ((ocvβπ)β((ocvβπ)βπ))) |
5 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
6 | 5, 1 | ocvss 21090 |
. . . . 5
β’
((ocvβπ)βπ) β (Baseβπ) |
7 | | eqid 2733 |
. . . . . 6
β’
(Β·πβπ) =
(Β·πβπ) |
8 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
9 | | eqid 2733 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
10 | 5, 7, 8, 9, 1 | ocvval 21087 |
. . . . 5
β’
(((ocvβπ)βπ) β (Baseβπ) β ((ocvβπ)β((ocvβπ)βπ)) = {π₯ β (Baseβπ) β£ βπ¦ β ((ocvβπ)βπ)(π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
11 | 6, 10 | mp1i 13 |
. . . 4
β’ ((π β βPreHil β§
π β πΆ) β ((ocvβπ)β((ocvβπ)βπ)) = {π₯ β (Baseβπ) β£ βπ¦ β ((ocvβπ)βπ)(π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
12 | | riinrab 5045 |
. . . 4
β’
((Baseβπ)
β© β© π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = {π₯ β (Baseβπ) β£ βπ¦ β ((ocvβπ)βπ)(π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} |
13 | 11, 12 | eqtr4di 2791 |
. . 3
β’ ((π β βPreHil β§
π β πΆ) β ((ocvβπ)β((ocvβπ)βπ)) = ((Baseβπ) β© β©
π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))})) |
14 | | cphnlm 24552 |
. . . . . . . 8
β’ (π β βPreHil β
π β
NrmMod) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β βPreHil β§
π β πΆ) β π β NrmMod) |
16 | | nlmngp 24057 |
. . . . . . 7
β’ (π β NrmMod β π β NrmGrp) |
17 | | ngptps 23974 |
. . . . . . 7
β’ (π β NrmGrp β π β TopSp) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . 6
β’ ((π β βPreHil β§
π β πΆ) β π β TopSp) |
19 | | csscld.j |
. . . . . . 7
β’ π½ = (TopOpenβπ) |
20 | 5, 19 | istps 22299 |
. . . . . 6
β’ (π β TopSp β π½ β
(TopOnβ(Baseβπ))) |
21 | 18, 20 | sylib 217 |
. . . . 5
β’ ((π β βPreHil β§
π β πΆ) β π½ β (TopOnβ(Baseβπ))) |
22 | | toponuni 22279 |
. . . . 5
β’ (π½ β
(TopOnβ(Baseβπ)) β (Baseβπ) = βͺ π½) |
23 | 21, 22 | syl 17 |
. . . 4
β’ ((π β βPreHil β§
π β πΆ) β (Baseβπ) = βͺ π½) |
24 | 23 | ineq1d 4172 |
. . 3
β’ ((π β βPreHil β§
π β πΆ) β ((Baseβπ) β© β©
π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) = (βͺ π½ β©
β© π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))})) |
25 | 4, 13, 24 | 3eqtrd 2777 |
. 2
β’ ((π β βPreHil β§
π β πΆ) β π = (βͺ π½ β© β© π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))})) |
26 | | topontop 22278 |
. . . 4
β’ (π½ β
(TopOnβ(Baseβπ)) β π½ β Top) |
27 | 21, 26 | syl 17 |
. . 3
β’ ((π β βPreHil β§
π β πΆ) β π½ β Top) |
28 | 6 | sseli 3941 |
. . . . 5
β’ (π¦ β ((ocvβπ)βπ) β π¦ β (Baseβπ)) |
29 | | fvex 6856 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) β V |
30 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) = (π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) |
31 | 30 | mptiniseg 6192 |
. . . . . . 7
β’
((0gβ(Scalarβπ)) β V β (β‘(π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) = {π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) |
32 | 29, 31 | ax-mp 5 |
. . . . . 6
β’ (β‘(π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) = {π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} |
33 | | eqid 2733 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
34 | | simpll 766 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β π β βPreHil) |
35 | 21 | adantr 482 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β π½ β (TopOnβ(Baseβπ))) |
36 | 35 | cnmptid 23028 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β (π₯ β (Baseβπ) β¦ π₯) β (π½ Cn π½)) |
37 | | simpr 486 |
. . . . . . . . 9
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β π¦ β (Baseβπ)) |
38 | 35, 35, 37 | cnmptc 23029 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β (π₯ β (Baseβπ) β¦ π¦) β (π½ Cn π½)) |
39 | 19, 33, 7, 34, 35, 36, 38 | cnmpt1ip 24627 |
. . . . . . 7
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β (π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) β (π½ Cn
(TopOpenββfld))) |
40 | 33 | cnfldhaus 24164 |
. . . . . . . 8
β’
(TopOpenββfld) β Haus |
41 | | cphclm 24569 |
. . . . . . . . . . 11
β’ (π β βPreHil β
π β
βMod) |
42 | 8 | clm0 24451 |
. . . . . . . . . . 11
β’ (π β βMod β 0 =
(0gβ(Scalarβπ))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
β’ (π β βPreHil β 0 =
(0gβ(Scalarβπ))) |
44 | 43 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β 0 =
(0gβ(Scalarβπ))) |
45 | | 0cn 11152 |
. . . . . . . . 9
β’ 0 β
β |
46 | 44, 45 | eqeltrrdi 2843 |
. . . . . . . 8
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β
(0gβ(Scalarβπ)) β β) |
47 | | unicntop 24165 |
. . . . . . . . 9
β’ β =
βͺ
(TopOpenββfld) |
48 | 47 | sncld 22738 |
. . . . . . . 8
β’
(((TopOpenββfld) β Haus β§
(0gβ(Scalarβπ)) β β) β
{(0gβ(Scalarβπ))} β
(Clsdβ(TopOpenββfld))) |
49 | 40, 46, 48 | sylancr 588 |
. . . . . . 7
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β
{(0gβ(Scalarβπ))} β
(Clsdβ(TopOpenββfld))) |
50 | | cnclima 22635 |
. . . . . . 7
β’ (((π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) β (π½ Cn (TopOpenββfld))
β§ {(0gβ(Scalarβπ))} β
(Clsdβ(TopOpenββfld))) β (β‘(π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) β (Clsdβπ½)) |
51 | 39, 49, 50 | syl2anc 585 |
. . . . . 6
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β (β‘(π₯ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦)) β
{(0gβ(Scalarβπ))}) β (Clsdβπ½)) |
52 | 32, 51 | eqeltrrid 2839 |
. . . . 5
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β (Baseβπ)) β {π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) |
53 | 28, 52 | sylan2 594 |
. . . 4
β’ (((π β βPreHil β§
π β πΆ) β§ π¦ β ((ocvβπ)βπ)) β {π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) |
54 | 53 | ralrimiva 3140 |
. . 3
β’ ((π β βPreHil β§
π β πΆ) β βπ¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) |
55 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
56 | 55 | riincld 22411 |
. . 3
β’ ((π½ β Top β§ βπ¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))} β (Clsdβπ½)) β (βͺ π½ β©
β© π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) β (Clsdβπ½)) |
57 | 27, 54, 56 | syl2anc 585 |
. 2
β’ ((π β βPreHil β§
π β πΆ) β (βͺ π½ β© β© π¦ β ((ocvβπ)βπ){π₯ β (Baseβπ) β£ (π₯(Β·πβπ)π¦) = (0gβ(Scalarβπ))}) β (Clsdβπ½)) |
58 | 25, 57 | eqeltrd 2834 |
1
β’ ((π β βPreHil β§
π β πΆ) β π β (Clsdβπ½)) |