Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lshpnel Structured version   Unicode version

Theorem lshpnel 29718
 Description: A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
Hypotheses
Ref Expression
lshpnel.v
lshpnel.n
lshpnel.p
lshpnel.h LSHyp
lshpnel.w
lshpnel.u
lshpnel.x
lshpnel.e
Assertion
Ref Expression
lshpnel

Proof of Theorem lshpnel
StepHypRef Expression
1 lshpnel.v . . 3
2 lshpnel.h . . 3 LSHyp
3 lshpnel.w . . 3
4 lshpnel.u . . 3
51, 2, 3, 4lshpne 29717 . 2
63adantr 452 . . . . . . . 8
7 eqid 2435 . . . . . . . . 9
87lsssssubg 16026 . . . . . . . 8 SubGrp
96, 8syl 16 . . . . . . 7 SubGrp
107, 2, 3, 4lshplss 29716 . . . . . . . 8
1110adantr 452 . . . . . . 7
129, 11sseldd 3341 . . . . . 6 SubGrp
13 lshpnel.x . . . . . . . . 9
1413adantr 452 . . . . . . . 8
15 lshpnel.n . . . . . . . . 9
161, 7, 15lspsncl 16045 . . . . . . . 8
176, 14, 16syl2anc 643 . . . . . . 7
189, 17sseldd 3341 . . . . . 6 SubGrp
19 simpr 448 . . . . . . 7
207, 15, 6, 11, 19lspsnel5a 16064 . . . . . 6
21 lshpnel.p . . . . . . 7
2221lsmss2 15292 . . . . . 6 SubGrp SubGrp
2312, 18, 20, 22syl3anc 1184 . . . . 5
24 lshpnel.e . . . . . 6
2524adantr 452 . . . . 5
2623, 25eqtr3d 2469 . . . 4
2726ex 424 . . 3