Metamath Proof Explorer


Theorem doch1

Description: Orthocomplement of the unit subspace (all vectors). (Contributed by NM, 19-Jun-2014)

Ref Expression
Hypotheses doch1.h 𝐻 = ( LHyp ‘ 𝐾 )
doch1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
doch1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
doch1.v 𝑉 = ( Base ‘ 𝑈 )
doch1.z 0 = ( 0g𝑈 )
Assertion doch1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑉 ) = { 0 } )

Proof

Step Hyp Ref Expression
1 doch1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 doch1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 doch1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 doch1.v 𝑉 = ( Base ‘ 𝑈 )
5 doch1.z 0 = ( 0g𝑈 )
6 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 1 6 2 4 dih1rn ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
8 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 8 1 6 3 dochvalr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑉 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ) ) )
10 7 9 mpdan ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑉 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ) ) )
11 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
12 1 11 6 2 4 dih1cnv ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) = ( 1. ‘ 𝐾 ) )
13 12 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) )
14 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
15 14 adantr ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐾 ∈ OP )
16 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
17 16 11 8 opoc1 ( 𝐾 ∈ OP → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
18 15 17 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
19 13 18 eqtrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ) = ( 0. ‘ 𝐾 ) )
20 19 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0. ‘ 𝐾 ) ) )
21 16 1 6 2 5 dih0 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
22 10 20 21 3eqtrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑉 ) = { 0 } )