Metamath Proof Explorer

Theorem dochspocN

Description: The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014) (New usage is discouraged.)

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 dochspocN ⊢ φ → N ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ N ⁡ 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 1 2 6 dvhlmod ⊢ φ → U ∈ LMod
9 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
10 1 2 4 9 3 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
11 6 7 10 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
12 9 5 lspid ⊢ U ∈ LMod ∧ ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U → N ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ X
13 8 11 12 syl2anc ⊢ φ → N ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ X
14 1 2 3 4 5 6 7 dochocsp ⊢ φ → ⊥ ˙ ⁡ N ⁡ X = ⊥ ˙ ⁡ X
15 13 14 eqtr4d ⊢ φ → N ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ N ⁡ X