Metamath Proof Explorer

Theorem doch0

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

Ref Expression
Hypotheses doch0.h ⊢ H = LHyp ⁡ K
doch0.u ⊢ U = DVecH ⁡ K ⁡ W
doch0.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
doch0.v ⊢ V = Base U
doch0.z ⊢ 0 ˙ = 0 U
Assertion doch0 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ 0 ˙ = V

Proof

Step Hyp Ref Expression
1 doch0.h ⊢ H = LHyp ⁡ K
2 doch0.u ⊢ U = DVecH ⁡ K ⁡ W
3 doch0.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 doch0.v ⊢ V = Base U
5 doch0.z ⊢ 0 ˙ = 0 U
6 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
7 1 6 2 5 dih0rn ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ ran ⁡ DIsoH ⁡ K ⁡ W
8 eqid ⊢ oc ⁡ K = oc ⁡ K
9 8 1 6 3 dochvalr ⊢ K ∈ HL ∧ W ∈ H ∧ 0 ˙ ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ 0 ˙ = DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙
10 7 9 mpdan ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ 0 ˙ = DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙
11 eqid ⊢ 0. ⁡ K = 0. ⁡ K
12 1 11 6 2 5 dih0cnv ⊢ K ∈ HL ∧ W ∈ H → DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙ = 0. ⁡ K
13 12 fveq2d ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙ = oc ⁡ K ⁡ 0. ⁡ K
14 hlop ⊢ K ∈ HL → K ∈ OP
15 14 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ OP
16 eqid ⊢ 1. ⁡ K = 1. ⁡ K
17 11 16 8 opoc0 ⊢ K ∈ OP → oc ⁡ K ⁡ 0. ⁡ K = 1. ⁡ K
18 15 17 syl ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ 0. ⁡ K = 1. ⁡ K
19 13 18 eqtrd ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙ = 1. ⁡ K
20 19 fveq2d ⊢ K ∈ HL ∧ W ∈ H → DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙ = DIsoH ⁡ K ⁡ W ⁡ 1. ⁡ K
21 16 1 6 2 4 dih1 ⊢ K ∈ HL ∧ W ∈ H → DIsoH ⁡ K ⁡ W ⁡ 1. ⁡ K = V
22 20 21 eqtrd ⊢ K ∈ HL ∧ W ∈ H → DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ 0 ˙ = V
23 10 22 eqtrd ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ 0 ˙ = V