Theorem dvhlvec

Description: The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W ) is a left module. (Contributed by NM, 23-May-2015)

	Ref	Expression
Hypotheses	dvhlvec.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhlvec.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvhlvec.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		dvhlvec.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvhlvec.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dvhlvec.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
4		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
7		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
8		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
9		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
10		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
11		eqid	⊢ ( invg ‘ ( Scalar ‘ 𝑈 ) ) = ( invg ‘ ( Scalar ‘ 𝑈 ) )
12		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑈 ) ) = ( .r ‘ ( Scalar ‘ 𝑈 ) )
13		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
14	4 1 5 6 2 7 8 9 10 11 12 13	dvhlveclem	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )
15	3 14	syl	⊢ ( 𝜑 → 𝑈 ∈ LVec )