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	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐿 )