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