This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )