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 ⊢ H = LHyp ⁡ K
dochsp.u ⊢ U = DVecH ⁡ K ⁡ W
dochsp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsp.v ⊢ V = Base U
dochsp.n ⊢ N = LSpan ⁡ U
dochsp.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsp.x ⊢ φ → X ⊆ V
Assertion dochspss ⊢ φ → N ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 dochsp.h ⊢ H = LHyp ⁡ K
2 dochsp.u ⊢ U = DVecH ⁡ K ⁡ W
3 dochsp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 dochsp.v ⊢ V = Base U
5 dochsp.n ⊢ N = LSpan ⁡ U
6 dochsp.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochsp.x ⊢ φ → X ⊆ V
8 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
9 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
10 1 2 8 9 dihsslss ⊢ K ∈ HL ∧ W ∈ H → ran ⁡ DIsoH ⁡ K ⁡ W ⊆ LSubSp ⁡ U
11 rabss2 ⊢ ran ⁡ DIsoH ⁡ K ⁡ W ⊆ LSubSp ⁡ U → z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ⊆ z ∈ LSubSp ⁡ U | X ⊆ z
12 intss ⊢ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ⊆ z ∈ LSubSp ⁡ U | X ⊆ z → ⋂ z ∈ LSubSp ⁡ U | X ⊆ z ⊆ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
13 6 10 11 12 4syl ⊢ φ → ⋂ z ∈ LSubSp ⁡ U | X ⊆ z ⊆ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
14 1 2 6 dvhlmod ⊢ φ → U ∈ LMod
15 4 9 5 lspval ⊢ U ∈ LMod ∧ X ⊆ V → N ⁡ X = ⋂ z ∈ LSubSp ⁡ U | X ⊆ z
16 14 7 15 syl2anc ⊢ φ → N ⁡ X = ⋂ z ∈ LSubSp ⁡ U | X ⊆ z
17 1 8 2 4 3 6 7 doch2val2 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
18 13 16 17 3sstr4d ⊢ φ → N ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X