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

Theorem dvh4dimN 32245
 Description: There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015.) (New usage is discouraged.)
Hypotheses
Ref Expression
dvh3dim.h
dvh3dim.u
dvh3dim.v
dvh3dim.n
dvh3dim.k
dvh3dim.x
dvh3dim.y
dvh3dim2.z
Assertion
Ref Expression
dvh4dimN
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem dvh4dimN
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
7 dvh3dim2.z . . . . 5
81, 2, 3, 4, 5, 6, 7dvh3dim 32244 . . . 4
10 eqid 2436 . . . . . . . 8
111, 2, 5dvhlmod 31908 . . . . . . . 8
12 prssi 3954 . . . . . . . . 9
136, 7, 12syl2anc 643 . . . . . . . 8
143, 10, 4, 11, 13lspun0 16087 . . . . . . 7
15 tpeq1 3892 . . . . . . . . 9
16 tprot 3899 . . . . . . . . . 10
17 df-tp 3822 . . . . . . . . . 10
1816, 17eqtr2i 2457 . . . . . . . . 9
1915, 18syl6reqr 2487 . . . . . . . 8
2019fveq2d 5732 . . . . . . 7
2114, 20sylan9req 2489 . . . . . 6
2221eleq2d 2503 . . . . 5
2322notbid 286 . . . 4
2423rexbidv 2726 . . 3
259, 24mpbid 202 . 2
26 dvh3dim.x . . . . 5
271, 2, 3, 4, 5, 26, 7dvh3dim 32244 . . . 4
29 prssi 3954 . . . . . . . . 9
3026, 7, 29syl2anc 643 . . . . . . . 8
313, 10, 4, 11, 30lspun0 16087 . . . . . . 7
32 tpeq2 3893 . . . . . . . . 9
33 df-tp 3822 . . . . . . . . . 10
34 tpcomb 3901 . . . . . . . . . 10
3533, 34eqtr3i 2458 . . . . . . . . 9
3632, 35syl6reqr 2487 . . . . . . . 8
3736fveq2d 5732 . . . . . . 7
3831, 37sylan9req 2489 . . . . . 6
3938eleq2d 2503 . . . . 5
4039notbid 286 . . . 4
4140rexbidv 2726 . . 3
4228, 41mpbid 202 . 2
431, 2, 3, 4, 5, 26, 6dvh3dim 32244 . . . 4
45 prssi 3954 . . . . . . . . 9
4626, 6, 45syl2anc 643 . . . . . . . 8
473, 10, 4, 11, 46lspun0 16087 . . . . . . 7
48 tpeq3 3894 . . . . . . . . 9
49 df-tp 3822 . . . . . . . . 9
5048, 49syl6req 2485 . . . . . . . 8
5150fveq2d 5732 . . . . . . 7
5247, 51sylan9req 2489 . . . . . 6
5352eleq2d 2503 . . . . 5
5453notbid 286 . . . 4
5554rexbidv 2726 . . 3
5644, 55mpbid 202 . 2