Metamath Proof Explorer

Theorem lshpdisj

Description: A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpdisj.v 
|- V = ( Base ` W )
lshpdisj.o 
|- .0. = ( 0g ` W )
lshpdisj.n 
|- N = ( LSpan ` W )
lshpdisj.p 
|- .(+) = ( LSSum ` W )
lshpdisj.h 
|- H = ( LSHyp ` W )
lshpdisj.w 
|- ( ph -> W e. LVec )
lshpdisj.u 
|- ( ph -> U e. H )
lshpdisj.x 
|- ( ph -> X e. V )
lshpdisj.e 
|- ( ph -> ( U .(+) ( N ` { X } ) ) = V )
Assertion lshpdisj 
|- ( ph -> ( U i^i ( N ` { X } ) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lshpdisj.v 
 |-  V = ( Base ` W )
2 lshpdisj.o 
 |-  .0. = ( 0g ` W )
3 lshpdisj.n 
 |-  N = ( LSpan ` W )
4 lshpdisj.p 
 |-  .(+) = ( LSSum ` W )
5 lshpdisj.h 
 |-  H = ( LSHyp ` W )
6 lshpdisj.w 
 |-  ( ph -> W e. LVec )
7 lshpdisj.u 
 |-  ( ph -> U e. H )
8 lshpdisj.x 
 |-  ( ph -> X e. V )
9 lshpdisj.e 
 |-  ( ph -> ( U .(+) ( N ` { X } ) ) = V )
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 6 10 syl 
 |-  ( ph -> W e. LMod )
12 11 adantr 
 |-  ( ( ph /\ v e. U ) -> W e. LMod )
13 8 adantr 
 |-  ( ( ph /\ v e. U ) -> X e. V )
14 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
15 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
16 eqid 
 |-  ( .s ` W ) = ( .s ` W )
17 14 15 1 16 3 lspsnel 
 |-  ( ( W e. LMod /\ X e. V ) -> ( v e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) )
18 12 13 17 syl2anc 
 |-  ( ( ph /\ v e. U ) -> ( v e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) )
19 1 3 4 5 11 7 8 9 lshpnel 
 |-  ( ph -> -. X e. U )
20 19 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> -. X e. U )
21 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
22 6 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> W e. LVec )
23 21 5 11 7 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> U e. ( LSubSp ` W ) )
25 8 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> X e. V )
26 11 adantr 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> W e. LMod )
27 simpr 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
28 8 adantr 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> X e. V )
29 1 16 14 15 3 26 27 28 lspsneli 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( N ` { X } ) )
30 29 adantr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> ( k ( .s ` W ) X ) e. ( N ` { X } ) )
31 simpr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> ( k ( .s ` W ) X ) =/= .0. )
32 1 2 21 3 22 24 25 30 31 lspsnel4 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> ( X e. U <-> ( k ( .s ` W ) X ) e. U ) )
33 20 32 mtbid 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( k ( .s ` W ) X ) =/= .0. ) -> -. ( k ( .s ` W ) X ) e. U )
34 33 ex 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( ( k ( .s ` W ) X ) =/= .0. -> -. ( k ( .s ` W ) X ) e. U ) )
35 34 necon4ad 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( ( k ( .s ` W ) X ) e. U -> ( k ( .s ` W ) X ) = .0. ) )
36 eleq1 
 |-  ( v = ( k ( .s ` W ) X ) -> ( v e. U <-> ( k ( .s ` W ) X ) e. U ) )
37 eqeq1 
 |-  ( v = ( k ( .s ` W ) X ) -> ( v = .0. <-> ( k ( .s ` W ) X ) = .0. ) )
38 36 37 imbi12d 
 |-  ( v = ( k ( .s ` W ) X ) -> ( ( v e. U -> v = .0. ) <-> ( ( k ( .s ` W ) X ) e. U -> ( k ( .s ` W ) X ) = .0. ) ) )
39 35 38 syl5ibrcom 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( v = ( k ( .s ` W ) X ) -> ( v e. U -> v = .0. ) ) )
40 39 ex 
 |-  ( ph -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v = ( k ( .s ` W ) X ) -> ( v e. U -> v = .0. ) ) ) )
41 40 com23 
 |-  ( ph -> ( v = ( k ( .s ` W ) X ) -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v e. U -> v = .0. ) ) ) )
42 41 com24 
 |-  ( ph -> ( v e. U -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v = ( k ( .s ` W ) X ) -> v = .0. ) ) ) )
43 42 imp31 
 |-  ( ( ( ph /\ v e. U ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( v = ( k ( .s ` W ) X ) -> v = .0. ) )
44 43 rexlimdva 
 |-  ( ( ph /\ v e. U ) -> ( E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) -> v = .0. ) )
45 18 44 sylbid 
 |-  ( ( ph /\ v e. U ) -> ( v e. ( N ` { X } ) -> v = .0. ) )
46 45 expimpd 
 |-  ( ph -> ( ( v e. U /\ v e. ( N ` { X } ) ) -> v = .0. ) )
47 elin 
 |-  ( v e. ( U i^i ( N ` { X } ) ) <-> ( v e. U /\ v e. ( N ` { X } ) ) )
48 velsn 
 |-  ( v e. { .0. } <-> v = .0. )
49 46 47 48 3imtr4g 
 |-  ( ph -> ( v e. ( U i^i ( N ` { X } ) ) -> v e. { .0. } ) )
50 49 ssrdv 
 |-  ( ph -> ( U i^i ( N ` { X } ) ) C_ { .0. } )
51 1 21 3 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
52 11 8 51 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
53 21 lssincl 
 |-  ( ( W e. LMod /\ U e. ( LSubSp ` W ) /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> ( U i^i ( N ` { X } ) ) e. ( LSubSp ` W ) )
54 11 23 52 53 syl3anc 
 |-  ( ph -> ( U i^i ( N ` { X } ) ) e. ( LSubSp ` W ) )
55 2 21 lss0ss 
 |-  ( ( W e. LMod /\ ( U i^i ( N ` { X } ) ) e. ( LSubSp ` W ) ) -> { .0. } C_ ( U i^i ( N ` { X } ) ) )
56 11 54 55 syl2anc 
 |-  ( ph -> { .0. } C_ ( U i^i ( N ` { X } ) ) )
57 50 56 eqssd 
 |-  ( ph -> ( U i^i ( N ` { X } ) ) = { .0. } )