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 𝐻 = ( LHyp ‘ 𝐾 )
dochsp.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsp.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsp.v 𝑉 = ( Base ‘ 𝑈 )
dochsp.n 𝑁 = ( LSpan ‘ 𝑈 )
dochsp.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochsp.x ( 𝜑𝑋𝑉 )
Assertion dochspocN ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ) ) = ( ‘ ( 𝑁𝑋 ) ) )

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 1 2 6 dvhlmod ( 𝜑𝑈 ∈ LMod )
9 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10 1 2 4 9 3 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
11 6 7 10 syl2anc ( 𝜑 → ( 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
12 9 5 lspid ( ( 𝑈 ∈ LMod ∧ ( 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 𝑁 ‘ ( 𝑋 ) ) = ( 𝑋 ) )
13 8 11 12 syl2anc ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ) ) = ( 𝑋 ) )
14 1 2 3 4 5 6 7 dochocsp ( 𝜑 → ( ‘ ( 𝑁𝑋 ) ) = ( 𝑋 ) )
15 13 14 eqtr4d ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ) ) = ( ‘ ( 𝑁𝑋 ) ) )