Metamath Proof Explorer

Theorem lshpnel

Description: A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpnel.v ⊢ V = Base W
lshpnel.n ⊢ N = LSpan ⁡ W
lshpnel.p ⊢ ⊕ ˙ = LSSum ⁡ W
lshpnel.h ⊢ H = LSHyp ⁡ W
lshpnel.w ⊢ φ → W ∈ LMod
lshpnel.u ⊢ φ → U ∈ H
lshpnel.x ⊢ φ → X ∈ V
lshpnel.e ⊢ φ → U ⊕ ˙ N ⁡ X = V
Assertion lshpnel ⊢ φ → ¬ X ∈ U

Proof

Step Hyp Ref Expression
1 lshpnel.v ⊢ V = Base W
2 lshpnel.n ⊢ N = LSpan ⁡ W
3 lshpnel.p ⊢ ⊕ ˙ = LSSum ⁡ W
4 lshpnel.h ⊢ H = LSHyp ⁡ W
5 lshpnel.w ⊢ φ → W ∈ LMod
6 lshpnel.u ⊢ φ → U ∈ H
7 lshpnel.x ⊢ φ → X ∈ V
8 lshpnel.e ⊢ φ → U ⊕ ˙ N ⁡ X = V
9 1 4 5 6 lshpne ⊢ φ → U ≠ V
10 5 adantr ⊢ φ ∧ X ∈ U → W ∈ LMod
11 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
12 11 lsssssubg ⊢ W ∈ LMod → LSubSp ⁡ W ⊆ SubGrp ⁡ W
13 10 12 syl ⊢ φ ∧ X ∈ U → LSubSp ⁡ W ⊆ SubGrp ⁡ W
14 11 4 5 6 lshplss ⊢ φ → U ∈ LSubSp ⁡ W
15 14 adantr ⊢ φ ∧ X ∈ U → U ∈ LSubSp ⁡ W
16 13 15 sseldd ⊢ φ ∧ X ∈ U → U ∈ SubGrp ⁡ W
17 7 adantr ⊢ φ ∧ X ∈ U → X ∈ V
18 1 11 2 lspsncl ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ X ∈ LSubSp ⁡ W
19 10 17 18 syl2anc ⊢ φ ∧ X ∈ U → N ⁡ X ∈ LSubSp ⁡ W
20 13 19 sseldd ⊢ φ ∧ X ∈ U → N ⁡ X ∈ SubGrp ⁡ W
21 simpr ⊢ φ ∧ X ∈ U → X ∈ U
22 11 2 10 15 21 ellspsn5 ⊢ φ ∧ X ∈ U → N ⁡ X ⊆ U
23 3 lsmss2 ⊢ U ∈ SubGrp ⁡ W ∧ N ⁡ X ∈ SubGrp ⁡ W ∧ N ⁡ X ⊆ U → U ⊕ ˙ N ⁡ X = U
24 16 20 22 23 syl3anc ⊢ φ ∧ X ∈ U → U ⊕ ˙ N ⁡ X = U
25 8 adantr ⊢ φ ∧ X ∈ U → U ⊕ ˙ N ⁡ X = V
26 24 25 eqtr3d ⊢ φ ∧ X ∈ U → U = V
27 26 ex ⊢ φ → X ∈ U → U = V
28 27 necon3ad ⊢ φ → U ≠ V → ¬ X ∈ U
29 9 28 mpd ⊢ φ → ¬ X ∈ U