Metamath Proof Explorer

Theorem dochshpncl

Description: If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 dochshpncl.h ⊢ H = LHyp ⁡ K
2 dochshpncl.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochshpncl.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochshpncl.v ⊢ V = Base U
5 dochshpncl.y ⊢ Y = LSHyp ⁡ U
6 dochshpncl.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochshpncl.x ⊢ φ → X ∈ Y
8 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
9 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
10 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
11 1 3 6 dvhlmod ⊢ φ → U ∈ LMod
12 4 8 9 10 5 11 islshpsm ⊢ φ → X ∈ Y ↔ X ∈ LSubSp ⁡ U ∧ X ≠ V ∧ ∃ v ∈ V X LSSum ⁡ U LSpan ⁡ U ⁡ v = V
13 7 12 mpbid ⊢ φ → X ∈ LSubSp ⁡ U ∧ X ≠ V ∧ ∃ v ∈ V X LSSum ⁡ U LSpan ⁡ U ⁡ v = V
14 13 simp3d ⊢ φ → ∃ v ∈ V X LSSum ⁡ U LSpan ⁡ U ⁡ v = V
15 14 adantr ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X → ∃ v ∈ V X LSSum ⁡ U LSpan ⁡ U ⁡ v = V
16 id ⊢ φ ∧ v ∈ V → φ ∧ v ∈ V
17 16 adantlr ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V → φ ∧ v ∈ V
18 17 3adant3 ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → φ ∧ v ∈ V
19 9 5 11 7 lshplss ⊢ φ → X ∈ LSubSp ⁡ U
20 4 9 lssss ⊢ X ∈ LSubSp ⁡ U → X ⊆ V
21 19 20 syl ⊢ φ → X ⊆ V
22 1 3 4 2 dochocss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
23 6 21 22 syl2anc ⊢ φ → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
24 23 adantr ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
25 24 3ad2ant1 ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
26 simp1r ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X
27 26 necomd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → X ≠ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
28 df-pss ⊢ X ⊂ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ↔ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ X ≠ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
29 25 27 28 sylanbrc ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → X ⊂ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
30 1 3 4 2 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V
31 6 21 30 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ⊆ V
32 1 3 4 2 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V
33 6 31 32 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V
34 33 adantr ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V
35 34 3ad2ant1 ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V
36 simp3 ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → X LSSum ⁡ U LSpan ⁡ U ⁡ v = V
37 35 36 sseqtrrd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ X LSSum ⁡ U LSpan ⁡ U ⁡ v
38 6 adantr ⊢ φ ∧ v ∈ V → K ∈ HL ∧ W ∈ H
39 1 3 38 dvhlvec ⊢ φ ∧ v ∈ V → U ∈ LVec
40 19 adantr ⊢ φ ∧ v ∈ V → X ∈ LSubSp ⁡ U
41 1 3 4 9 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
42 6 31 41 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
43 42 adantr ⊢ φ ∧ v ∈ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
44 simpr ⊢ φ ∧ v ∈ V → v ∈ V
45 4 9 8 10 39 40 43 44 lsmcv ⊢ φ ∧ v ∈ V ∧ X ⊂ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ X LSSum ⁡ U LSpan ⁡ U ⁡ v → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X LSSum ⁡ U LSpan ⁡ U ⁡ v
46 18 29 37 45 syl3anc ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X LSSum ⁡ U LSpan ⁡ U ⁡ v
47 46 36 eqtrd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ∧ v ∈ V ∧ X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V
48 47 rexlimdv3a ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X → ∃ v ∈ V X LSSum ⁡ U LSpan ⁡ U ⁡ v = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V
49 15 48 mpd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V
50 simpr ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V
51 4 5 11 7 lshpne ⊢ φ → X ≠ V
52 51 adantr ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V → X ≠ V
53 52 necomd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V → V ≠ X
54 50 53 eqnetrd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X
55 49 54 impbida ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ≠ X ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = V