Metamath Proof Explorer

Theorem hlprlem

Description: Lemma for hlpr . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses hlress.f 
|- F = ( Scalar ` W )
hlress.k 
|- K = ( Base ` F )
Assertion hlprlem 
|- ( W e. CHil -> ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing /\ ( CCfld |`s K ) e. CMetSp ) )

Proof

Step Hyp Ref Expression
1 hlress.f 
 |-  F = ( Scalar ` W )
2 hlress.k 
 |-  K = ( Base ` F )
3 hlcph 
 |-  ( W e. CHil -> W e. CPreHil )
4 1 2 cphsubrg 
 |-  ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
5 3 4 syl 
 |-  ( W e. CHil -> K e. ( SubRing ` CCfld ) )
6 1 2 cphsca 
 |-  ( W e. CPreHil -> F = ( CCfld |`s K ) )
7 3 6 syl 
 |-  ( W e. CHil -> F = ( CCfld |`s K ) )
8 cphlvec 
 |-  ( W e. CPreHil -> W e. LVec )
9 1 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
10 3 8 9 3syl 
 |-  ( W e. CHil -> F e. DivRing )
11 7 10 eqeltrrd 
 |-  ( W e. CHil -> ( CCfld |`s K ) e. DivRing )
12 hlbn 
 |-  ( W e. CHil -> W e. Ban )
13 1 bnsca 
 |-  ( W e. Ban -> F e. CMetSp )
14 12 13 syl 
 |-  ( W e. CHil -> F e. CMetSp )
15 7 14 eqeltrrd 
 |-  ( W e. CHil -> ( CCfld |`s K ) e. CMetSp )
16 5 11 15 3jca 
 |-  ( W e. CHil -> ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing /\ ( CCfld |`s K ) e. CMetSp ) )