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

Theorem dvh3dim 32245
 Description: There is a vector that is outside the span of 2 others. (Contributed by NM, 24-Apr-2015.)
Hypotheses
Ref Expression
dvh3dim.h
dvh3dim.u
dvh3dim.v
dvh3dim.n
dvh3dim.k
dvh3dim.x
dvh3dim.y
Assertion
Ref Expression
dvh3dim
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem dvh3dim
StepHypRef Expression
1 dvh3dim.h . . . . 5
2 dvh3dim.u . . . . 5
3 dvh3dim.v . . . . 5
4 dvh3dim.n . . . . 5
5 dvh3dim.k . . . . 5
6 dvh3dim.y . . . . 5
71, 2, 3, 4, 5, 6dvh2dim 32244 . . . 4
9 prcom 3883 . . . . . . . . 9
10 preq2 3885 . . . . . . . . 9
119, 10syl5eq 2481 . . . . . . . 8
1211fveq2d 5733 . . . . . . 7
13 eqid 2437 . . . . . . . 8
141, 2, 5dvhlmod 31909 . . . . . . . 8
153, 13, 4, 14, 6lsppr0 16165 . . . . . . 7
1612, 15sylan9eqr 2491 . . . . . 6
1716eleq2d 2504 . . . . 5
1817notbid 287 . . . 4
1918rexbidv 2727 . . 3
208, 19mpbird 225 . 2
21 dvh3dim.x . . . . 5
221, 2, 3, 4, 5, 21dvh2dim 32244 . . . 4
24 preq2 3885 . . . . . . . 8
2524fveq2d 5733 . . . . . . 7
263, 13, 4, 14, 21lsppr0 16165 . . . . . . 7
2725, 26sylan9eqr 2491 . . . . . 6
2827eleq2d 2504 . . . . 5
2928notbid 287 . . . 4
3029rexbidv 2727 . . 3
3123, 30mpbird 225 . 2