Theorem dochspss

Description: The span of a set of vectors is included in their double orthocomplement. (Contributed by NM, 26-Jul-2014)

	Ref	Expression
Hypotheses	dochsp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochsp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochsp.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochsp.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dochsp.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochsp.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion	dochspss	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochsp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochsp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dochsp.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		dochsp.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		dochsp.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		dochsp.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
8		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10	1 2 8 9	dihsslss	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ⊆ ( LSubSp ‘ 𝑈 ) )
11		rabss2	⊢ ( ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ⊆ ( LSubSp ‘ 𝑈 ) → { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋 ⊆ 𝑧 } ⊆ { 𝑧 ∈ ( LSubSp ‘ 𝑈 ) ∣ 𝑋 ⊆ 𝑧 } )
12		intss	⊢ ( { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋 ⊆ 𝑧 } ⊆ { 𝑧 ∈ ( LSubSp ‘ 𝑈 ) ∣ 𝑋 ⊆ 𝑧 } → ∩ { 𝑧 ∈ ( LSubSp ‘ 𝑈 ) ∣ 𝑋 ⊆ 𝑧 } ⊆ ∩ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋 ⊆ 𝑧 } )
13	6 10 11 12	4syl	⊢ ( 𝜑 → ∩ { 𝑧 ∈ ( LSubSp ‘ 𝑈 ) ∣ 𝑋 ⊆ 𝑧 } ⊆ ∩ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋 ⊆ 𝑧 } )
14	1 2 6	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
15	4 9 5	lspval	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ∩ { 𝑧 ∈ ( LSubSp ‘ 𝑈 ) ∣ 𝑋 ⊆ 𝑧 } )
16	14 7 15	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ∩ { 𝑧 ∈ ( LSubSp ‘ 𝑈 ) ∣ 𝑋 ⊆ 𝑧 } )
17	1 8 2 4 3 6 7	doch2val2	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ∩ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋 ⊆ 𝑧 } )
18	13 16 17	3sstr4d	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )