Step | Hyp | Ref
| Expression |
1 | | ishl 24729 |
. 2
β’ (π β βHil β (π β Ban β§ π β
βPreHil)) |
2 | | df-3an 1090 |
. . 3
β’ ((π β CMetSp β§ πΎ β {β, β} β§
π β βPreHil)
β ((π β CMetSp
β§ πΎ β {β,
β}) β§ π β
βPreHil)) |
3 | | 3ancomb 1100 |
. . 3
β’ ((π β CMetSp β§ π β βPreHil β§
πΎ β {β,
β}) β (π β
CMetSp β§ πΎ β
{β, β} β§ π
β βPreHil)) |
4 | | cphnvc 24543 |
. . . . . 6
β’ (π β βPreHil β
π β
NrmVec) |
5 | | hlress.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
6 | 5 | isbn 24705 |
. . . . . . . 8
β’ (π β Ban β (π β NrmVec β§ π β CMetSp β§ πΉ β
CMetSp)) |
7 | | 3anass 1096 |
. . . . . . . 8
β’ ((π β NrmVec β§ π β CMetSp β§ πΉ β CMetSp) β (π β NrmVec β§ (π β CMetSp β§ πΉ β
CMetSp))) |
8 | 6, 7 | bitri 275 |
. . . . . . 7
β’ (π β Ban β (π β NrmVec β§ (π β CMetSp β§ πΉ β
CMetSp))) |
9 | 8 | baib 537 |
. . . . . 6
β’ (π β NrmVec β (π β Ban β (π β CMetSp β§ πΉ β
CMetSp))) |
10 | 4, 9 | syl 17 |
. . . . 5
β’ (π β βPreHil β
(π β Ban β (π β CMetSp β§ πΉ β
CMetSp))) |
11 | | hlress.k |
. . . . . . . . 9
β’ πΎ = (BaseβπΉ) |
12 | 5, 11 | cphsca 24546 |
. . . . . . . 8
β’ (π β βPreHil β
πΉ = (βfld
βΎs πΎ)) |
13 | 12 | eleq1d 2823 |
. . . . . . 7
β’ (π β βPreHil β
(πΉ β CMetSp β
(βfld βΎs πΎ) β CMetSp)) |
14 | 5, 11 | cphsubrg 24547 |
. . . . . . . . 9
β’ (π β βPreHil β
πΎ β
(SubRingββfld)) |
15 | | cphlvec 24542 |
. . . . . . . . . . 11
β’ (π β βPreHil β
π β
LVec) |
16 | 5 | lvecdrng 20569 |
. . . . . . . . . . 11
β’ (π β LVec β πΉ β
DivRing) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
β’ (π β βPreHil β
πΉ β
DivRing) |
18 | 12, 17 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β βPreHil β
(βfld βΎs πΎ) β DivRing) |
19 | | eqid 2737 |
. . . . . . . . . . 11
β’
(βfld βΎs πΎ) = (βfld
βΎs πΎ) |
20 | 19 | cncdrg 24726 |
. . . . . . . . . 10
β’ ((πΎ β
(SubRingββfld) β§ (βfld
βΎs πΎ)
β DivRing β§ (βfld βΎs πΎ) β CMetSp) β πΎ β {β,
β}) |
21 | 20 | 3expia 1122 |
. . . . . . . . 9
β’ ((πΎ β
(SubRingββfld) β§ (βfld
βΎs πΎ)
β DivRing) β ((βfld βΎs πΎ) β CMetSp β πΎ β {β,
β})) |
22 | 14, 18, 21 | syl2anc 585 |
. . . . . . . 8
β’ (π β βPreHil β
((βfld βΎs πΎ) β CMetSp β πΎ β {β,
β})) |
23 | | elpri 4609 |
. . . . . . . . 9
β’ (πΎ β {β, β}
β (πΎ = β β¨
πΎ =
β)) |
24 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (πΎ = β β
(βfld βΎs πΎ) = (βfld
βΎs β)) |
25 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) =
(TopOpenββfld) |
26 | 25 | recld2 24180 |
. . . . . . . . . . . 12
β’ β
β (Clsdβ(TopOpenββfld)) |
27 | | cncms 24722 |
. . . . . . . . . . . . 13
β’
βfld β CMetSp |
28 | | ax-resscn 11109 |
. . . . . . . . . . . . 13
β’ β
β β |
29 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(βfld βΎs β) =
(βfld βΎs β) |
30 | | cnfldbas 20803 |
. . . . . . . . . . . . . 14
β’ β =
(Baseββfld) |
31 | 29, 30, 25 | cmsss 24718 |
. . . . . . . . . . . . 13
β’
((βfld β CMetSp β§ β β β)
β ((βfld βΎs β) β CMetSp
β β β
(Clsdβ(TopOpenββfld)))) |
32 | 27, 28, 31 | mp2an 691 |
. . . . . . . . . . . 12
β’
((βfld βΎs β) β CMetSp
β β β
(Clsdβ(TopOpenββfld))) |
33 | 26, 32 | mpbir 230 |
. . . . . . . . . . 11
β’
(βfld βΎs β) β
CMetSp |
34 | 24, 33 | eqeltrdi 2846 |
. . . . . . . . . 10
β’ (πΎ = β β
(βfld βΎs πΎ) β CMetSp) |
35 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (πΎ = β β
(βfld βΎs πΎ) = (βfld
βΎs β)) |
36 | 30 | ressid 17126 |
. . . . . . . . . . . . 13
β’
(βfld β CMetSp β (βfld
βΎs β) = βfld) |
37 | 27, 36 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(βfld βΎs β) =
βfld |
38 | 37, 27 | eqeltri 2834 |
. . . . . . . . . . 11
β’
(βfld βΎs β) β
CMetSp |
39 | 35, 38 | eqeltrdi 2846 |
. . . . . . . . . 10
β’ (πΎ = β β
(βfld βΎs πΎ) β CMetSp) |
40 | 34, 39 | jaoi 856 |
. . . . . . . . 9
β’ ((πΎ = β β¨ πΎ = β) β
(βfld βΎs πΎ) β CMetSp) |
41 | 23, 40 | syl 17 |
. . . . . . . 8
β’ (πΎ β {β, β}
β (βfld βΎs πΎ) β CMetSp) |
42 | 22, 41 | impbid1 224 |
. . . . . . 7
β’ (π β βPreHil β
((βfld βΎs πΎ) β CMetSp β πΎ β {β,
β})) |
43 | 13, 42 | bitrd 279 |
. . . . . 6
β’ (π β βPreHil β
(πΉ β CMetSp β
πΎ β {β,
β})) |
44 | 43 | anbi2d 630 |
. . . . 5
β’ (π β βPreHil β
((π β CMetSp β§
πΉ β CMetSp) β
(π β CMetSp β§
πΎ β {β,
β}))) |
45 | 10, 44 | bitrd 279 |
. . . 4
β’ (π β βPreHil β
(π β Ban β (π β CMetSp β§ πΎ β {β,
β}))) |
46 | 45 | pm5.32ri 577 |
. . 3
β’ ((π β Ban β§ π β βPreHil) β
((π β CMetSp β§
πΎ β {β,
β}) β§ π β
βPreHil)) |
47 | 2, 3, 46 | 3bitr4ri 304 |
. 2
β’ ((π β Ban β§ π β βPreHil) β
(π β CMetSp β§
π β βPreHil
β§ πΎ β {β,
β})) |
48 | 1, 47 | bitri 275 |
1
β’ (π β βHil β (π β CMetSp β§ π β βPreHil β§
πΎ β {β,
β})) |