Theorem lcdvscl

Description: The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	lcdvscl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvscl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvscl.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcdvscl.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcdvscl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvscl.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdvscl.t	⊢ · = ( ·𝑠 ‘ 𝐶 )
	lcdvscl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
	lcdvscl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion	lcdvscl	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lcdvscl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvscl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvscl.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4		lcdvscl.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
5		lcdvscl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		lcdvscl.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
7		lcdvscl.t	⊢ · = ( ·𝑠 ‘ 𝐶 )
8		lcdvscl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		lcdvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
10		lcdvscl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
11	1 5 8	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
12		eqid	⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
13		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
14	1 2 3 4 5 12 13 8	lcdsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝑅 )
15	9 14	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
16	6 12 7 13	lmodvscl	⊢ ( ( 𝐶 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝐺 ∈ 𝑉 ) → ( 𝑋 · 𝐺 ) ∈ 𝑉 )
17	11 15 10 16	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝑉 )