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 } )