Metamath Proof Explorer

Theorem dochocsp

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

Ref Expression
Hypotheses dochsp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsp.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsp.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochsp.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dochsp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsp.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion dochocsp ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) = ( ⊥ ‘ 𝑋 ) )

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 4 5 lspssv ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) ⊆ 𝑉 )
10 8 7 9 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ 𝑉 )
11 4 5 lspssid ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ⊆ 𝑉 ) → 𝑋 ⊆ ( 𝑁 ‘ 𝑋 ) )
12 8 7 11 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑁 ‘ 𝑋 ) )
13 1 2 4 3 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ 𝑋 ) ⊆ 𝑉 ∧ 𝑋 ⊆ ( 𝑁 ‘ 𝑋 ) ) → ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ 𝑋 ) )
14 6 10 12 13 syl3anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ 𝑋 ) )
15 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
16 1 15 2 4 3 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
17 6 7 16 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
18 1 15 3 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
19 6 17 18 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
20 1 2 4 3 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
21 6 7 20 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
22 1 2 4 3 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
23 6 21 22 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
24 1 2 3 4 5 6 7 dochspss ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
25 1 2 4 3 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) )
26 6 23 24 25 syl3anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) )
27 19 26 eqsstrrd ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) )
28 14 27 eqssd ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ 𝑋 ) ) = ( ⊥ ‘ 𝑋 ) )