Theorem dochflcl

Description: Closure of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkrcl . (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochflcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochflcl.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochflcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochflcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochflcl.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochflcl.a	⊢ + = ( +g ‘ 𝑈 )
	dochflcl.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	dochflcl.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	dochflcl.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
	dochflcl.r	⊢ 𝑅 = ( Base ‘ 𝐷 )
	dochflcl.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
	dochflcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochflcl.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion	dochflcl	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		dochflcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochflcl.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochflcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochflcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochflcl.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		dochflcl.a	⊢ + = ( +g ‘ 𝑈 )
7		dochflcl.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
8		dochflcl.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9		dochflcl.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
10		dochflcl.r	⊢ 𝑅 = ( Base ‘ 𝐷 )
11		dochflcl.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
12		dochflcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		dochflcl.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
15		eqid	⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
16		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
17	1 3 12	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
18	1 2 3 4 5 16 12 13	dochsnshp	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
19	13	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
20	1 2 3 4 5 14 15 12 13	dochexmidat	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = 𝑉 )
21	4 6 14 15 16 17 18 19 20 9 10 7 11 8	lshpkrcl	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )