Metamath Proof Explorer

Theorem hlprlem

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

Ref Expression
Hypotheses hlress.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
hlress.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
Assertion hlprlem ( π‘Š ∈ β„‚Hil β†’ ( 𝐾 ∈ ( SubRing β€˜ β„‚fld ) ∧ ( β„‚fld β†Ύs 𝐾 ) ∈ DivRing ∧ ( β„‚fld β†Ύs 𝐾 ) ∈ CMetSp ) )

Proof

Step Hyp Ref Expression
1 hlress.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
2 hlress.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
3 hlcph ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ β„‚PreHil )
4 1 2 cphsubrg ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐾 ∈ ( SubRing β€˜ β„‚fld ) )
5 3 4 syl ⊒ ( π‘Š ∈ β„‚Hil β†’ 𝐾 ∈ ( SubRing β€˜ β„‚fld ) )
6 1 2 cphsca ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐹 = ( β„‚fld β†Ύs 𝐾 ) )
7 3 6 syl ⊒ ( π‘Š ∈ β„‚Hil β†’ 𝐹 = ( β„‚fld β†Ύs 𝐾 ) )
8 cphlvec ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ LVec )
9 1 lvecdrng ⊒ ( π‘Š ∈ LVec β†’ 𝐹 ∈ DivRing )
10 3 8 9 3syl ⊒ ( π‘Š ∈ β„‚Hil β†’ 𝐹 ∈ DivRing )
11 7 10 eqeltrrd ⊒ ( π‘Š ∈ β„‚Hil β†’ ( β„‚fld β†Ύs 𝐾 ) ∈ DivRing )
12 hlbn ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ Ban )
13 1 bnsca ⊒ ( π‘Š ∈ Ban β†’ 𝐹 ∈ CMetSp )
14 12 13 syl ⊒ ( π‘Š ∈ β„‚Hil β†’ 𝐹 ∈ CMetSp )
15 7 14 eqeltrrd ⊒ ( π‘Š ∈ β„‚Hil β†’ ( β„‚fld β†Ύs 𝐾 ) ∈ CMetSp )
16 5 11 15 3jca ⊒ ( π‘Š ∈ β„‚Hil β†’ ( 𝐾 ∈ ( SubRing β€˜ β„‚fld ) ∧ ( β„‚fld β†Ύs 𝐾 ) ∈ DivRing ∧ ( β„‚fld β†Ύs 𝐾 ) ∈ CMetSp ) )