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