Metamath Proof Explorer

Theorem doch0

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

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

Proof

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