| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ishl 25234 |
. 2
β’ (π β βHil β (π β Ban β§ π β
βPreHil)) |
| 2 | | df-3an 1086 |
. . 3
β’ ((π β CMetSp β§ πΎ β {β, β} β§
π β βPreHil)
β ((π β CMetSp
β§ πΎ β {β,
β}) β§ π β
βPreHil)) |
| 3 | | 3ancomb 1096 |
. . 3
β’ ((π β CMetSp β§ π β βPreHil β§
πΎ β {β,
β}) β (π β
CMetSp β§ πΎ β
{β, β} β§ π
β βPreHil)) |
| 4 | | cphnvc 25048 |
. . . . . 6
β’ (π β βPreHil β
π β
NrmVec) |
| 5 | | hlress.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
| 6 | 5 | isbn 25210 |
. . . . . . . 8
β’ (π β Ban β (π β NrmVec β§ π β CMetSp β§ πΉ β
CMetSp)) |
| 7 | | 3anass 1092 |
. . . . . . . 8
β’ ((π β NrmVec β§ π β CMetSp β§ πΉ β CMetSp) β (π β NrmVec β§ (π β CMetSp β§ πΉ β
CMetSp))) |
| 8 | 6, 7 | bitri 275 |
. . . . . . 7
β’ (π β Ban β (π β NrmVec β§ (π β CMetSp β§ πΉ β
CMetSp))) |
| 9 | 8 | baib 535 |
. . . . . 6
β’ (π β NrmVec β (π β Ban β (π β CMetSp β§ πΉ β
CMetSp))) |
| 10 | 4, 9 | syl 17 |
. . . . 5
β’ (π β βPreHil β
(π β Ban β (π β CMetSp β§ πΉ β
CMetSp))) |
| 11 | | hlress.k |
. . . . . . . . 9
β’ πΎ = (BaseβπΉ) |
| 12 | 5, 11 | cphsca 25051 |
. . . . . . . 8
β’ (π β βPreHil β
πΉ = (βfld
βΎs πΎ)) |
| 13 | 12 | eleq1d 2810 |
. . . . . . 7
β’ (π β βPreHil β
(πΉ β CMetSp β
(βfld βΎs πΎ) β CMetSp)) |
| 14 | 5, 11 | cphsubrg 25052 |
. . . . . . . . 9
β’ (π β βPreHil β
πΎ β
(SubRingββfld)) |
| 15 | | cphlvec 25047 |
. . . . . . . . . . 11
β’ (π β βPreHil β
π β
LVec) |
| 16 | 5 | lvecdrng 20949 |
. . . . . . . . . . 11
β’ (π β LVec β πΉ β
DivRing) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . 10
β’ (π β βPreHil β
πΉ β
DivRing) |
| 18 | 12, 17 | eqeltrrd 2826 |
. . . . . . . . 9
β’ (π β βPreHil β
(βfld βΎs πΎ) β DivRing) |
| 19 | | eqid 2724 |
. . . . . . . . . . 11
β’
(βfld βΎs πΎ) = (βfld
βΎs πΎ) |
| 20 | 19 | cncdrg 25231 |
. . . . . . . . . 10
β’ ((πΎ β
(SubRingββfld) β§ (βfld
βΎs πΎ)
β DivRing β§ (βfld βΎs πΎ) β CMetSp) β πΎ β {β,
β}) |
| 21 | 20 | 3expia 1118 |
. . . . . . . . 9
β’ ((πΎ β
(SubRingββfld) β§ (βfld
βΎs πΎ)
β DivRing) β ((βfld βΎs πΎ) β CMetSp β πΎ β {β,
β})) |
| 22 | 14, 18, 21 | syl2anc 583 |
. . . . . . . 8
β’ (π β βPreHil β
((βfld βΎs πΎ) β CMetSp β πΎ β {β,
β})) |
| 23 | | elpri 4643 |
. . . . . . . . 9
β’ (πΎ β {β, β}
β (πΎ = β β¨
πΎ =
β)) |
| 24 | | oveq2 7410 |
. . . . . . . . . . 11
β’ (πΎ = β β
(βfld βΎs πΎ) = (βfld
βΎs β)) |
| 25 | | eqid 2724 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) =
(TopOpenββfld) |
| 26 | 25 | recld2 24674 |
. . . . . . . . . . . 12
β’ β
β (Clsdβ(TopOpenββfld)) |
| 27 | | cncms 25227 |
. . . . . . . . . . . . 13
β’
βfld β CMetSp |
| 28 | | ax-resscn 11164 |
. . . . . . . . . . . . 13
β’ β
β β |
| 29 | | eqid 2724 |
. . . . . . . . . . . . . 14
β’
(βfld βΎs β) =
(βfld βΎs β) |
| 30 | | cnfldbas 21238 |
. . . . . . . . . . . . . 14
β’ β =
(Baseββfld) |
| 31 | 29, 30, 25 | cmsss 25223 |
. . . . . . . . . . . . 13
β’
((βfld β CMetSp β§ β β β)
β ((βfld βΎs β) β CMetSp
β β β
(Clsdβ(TopOpenββfld)))) |
| 32 | 27, 28, 31 | mp2an 689 |
. . . . . . . . . . . 12
β’
((βfld βΎs β) β CMetSp
β β β
(Clsdβ(TopOpenββfld))) |
| 33 | 26, 32 | mpbir 230 |
. . . . . . . . . . 11
β’
(βfld βΎs β) β
CMetSp |
| 34 | 24, 33 | eqeltrdi 2833 |
. . . . . . . . . 10
β’ (πΎ = β β
(βfld βΎs πΎ) β CMetSp) |
| 35 | | oveq2 7410 |
. . . . . . . . . . 11
β’ (πΎ = β β
(βfld βΎs πΎ) = (βfld
βΎs β)) |
| 36 | 30 | ressid 17194 |
. . . . . . . . . . . . 13
β’
(βfld β CMetSp β (βfld
βΎs β) = βfld) |
| 37 | 27, 36 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(βfld βΎs β) =
βfld |
| 38 | 37, 27 | eqeltri 2821 |
. . . . . . . . . . 11
β’
(βfld βΎs β) β
CMetSp |
| 39 | 35, 38 | eqeltrdi 2833 |
. . . . . . . . . 10
β’ (πΎ = β β
(βfld βΎs πΎ) β CMetSp) |
| 40 | 34, 39 | jaoi 854 |
. . . . . . . . 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 628 |
. . . . 5
β’ (π β βPreHil β
((π β CMetSp β§
πΉ β CMetSp) β
(π β CMetSp β§
πΎ β {β,
β}))) |
| 45 | 10, 44 | bitrd 279 |
. . . 4
β’ (π β βPreHil β
(π β Ban β (π β CMetSp β§ πΎ β {β,
β}))) |
| 46 | 45 | pm5.32ri 575 |
. . 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 β§
πΎ β {β,
β})) |
