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=BaseU
doch0.z ⊢0˙=0U
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=BaseU
5 doch0.z ⊢0˙=0U
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