Metamath Proof Explorer

Theorem doch1

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

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

Proof

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