Metamath Proof Explorer


Theorem lcdlssvscl

Description: Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses lcdlssvscl.h 𝐻 = ( LHyp ‘ 𝐾 )
lcdlssvscl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdlssvscl.f 𝐹 = ( Scalar ‘ 𝑈 )
lcdlssvscl.r 𝑅 = ( Base ‘ 𝐹 )
lcdlssvscl.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdlssvscl.v 𝑉 = ( Base ‘ 𝐶 )
lcdlssvscl.t · = ( ·𝑠𝐶 )
lcdlssvscl.s 𝑆 = ( LSubSp ‘ 𝐶 )
lcdlssvscl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcdlssvscl.l ( 𝜑𝐿𝑆 )
lcdlssvscl.x ( 𝜑𝑋𝑅 )
lcdlssvscl.y ( 𝜑𝑌𝐿 )
Assertion lcdlssvscl ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐿 )

Proof

Step Hyp Ref Expression
1 lcdlssvscl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdlssvscl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdlssvscl.f 𝐹 = ( Scalar ‘ 𝑈 )
4 lcdlssvscl.r 𝑅 = ( Base ‘ 𝐹 )
5 lcdlssvscl.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 lcdlssvscl.v 𝑉 = ( Base ‘ 𝐶 )
7 lcdlssvscl.t · = ( ·𝑠𝐶 )
8 lcdlssvscl.s 𝑆 = ( LSubSp ‘ 𝐶 )
9 lcdlssvscl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 lcdlssvscl.l ( 𝜑𝐿𝑆 )
11 lcdlssvscl.x ( 𝜑𝑋𝑅 )
12 lcdlssvscl.y ( 𝜑𝑌𝐿 )
13 1 5 9 lcdlmod ( 𝜑𝐶 ∈ LMod )
14 eqid ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
15 eqid ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
16 1 2 3 4 5 14 15 9 lcdsbase ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝑅 )
17 11 16 eleqtrrd ( 𝜑𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
18 14 7 15 8 lssvscl ( ( ( 𝐶 ∈ LMod ∧ 𝐿𝑆 ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑌𝐿 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐿 )
19 13 10 17 12 18 syl22anc ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐿 )