Metamath Proof Explorer

Theorem dochn0nv

Description: An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochn0nv.h ⊢ H = LHyp ⁡ K
dochn0nv.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochn0nv.u ⊢ U = DVecH ⁡ K ⁡ W
dochn0nv.v ⊢ V = Base U
dochn0nv.z ⊢ 0 ˙ = 0 U
dochn0nv.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochn0nv.x ⊢ φ → X ⊆ V
Assertion dochn0nv ⊢ φ → ⊥ ˙ ⁡ X ≠ 0 ˙ ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ V

Proof

Step Hyp Ref Expression
1 dochn0nv.h ⊢ H = LHyp ⁡ K
2 dochn0nv.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochn0nv.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochn0nv.v ⊢ V = Base U
5 dochn0nv.z ⊢ 0 ˙ = 0 U
6 dochn0nv.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochn0nv.x ⊢ φ → X ⊆ V
8 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
9 1 8 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
10 6 7 9 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
11 1 8 2 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ X
12 6 10 11 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ X
13 1 3 2 4 5 doch1 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ V = 0 ˙
14 6 13 syl ⊢ φ → ⊥ ˙ ⁡ V = 0 ˙
15 12 14 eqeq12d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ V ↔ ⊥ ˙ ⁡ X = 0 ˙
16 1 3 4 2 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V
17 6 7 16 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ⊆ V
18 1 8 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
19 6 17 18 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
20 1 8 3 4 dih1rn ⊢ K ∈ HL ∧ W ∈ H → V ∈ ran ⁡ DIsoH ⁡ K ⁡ W
21 6 20 syl ⊢ φ → V ∈ ran ⁡ DIsoH ⁡ K ⁡ W
22 1 8 2 6 19 21 doch11 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V
23 15 22 bitr3d ⊢ φ → ⊥ ˙ ⁡ X = 0 ˙ ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V
24 23 necon3bid ⊢ φ → ⊥ ˙ ⁡ X ≠ 0 ˙ ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ V