Metamath Proof Explorer

Theorem lss1d

Description: One-dimensional subspace (or zero-dimensional if X is the zero vector). (Contributed by NM, 14-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lss1d.v 
|- V = ( Base ` W )
lss1d.f 
|- F = ( Scalar ` W )
lss1d.t 
|- .x. = ( .s ` W )
lss1d.k 
|- K = ( Base ` F )
lss1d.s 
|- S = ( LSubSp ` W )
Assertion lss1d 
|- ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } e. S )

Proof

Step Hyp Ref Expression
1 lss1d.v 
 |-  V = ( Base ` W )
2 lss1d.f 
 |-  F = ( Scalar ` W )
3 lss1d.t 
 |-  .x. = ( .s ` W )
4 lss1d.k 
 |-  K = ( Base ` F )
5 lss1d.s 
 |-  S = ( LSubSp ` W )
6 2 a1i 
 |-  ( ( W e. LMod /\ X e. V ) -> F = ( Scalar ` W ) )
7 4 a1i 
 |-  ( ( W e. LMod /\ X e. V ) -> K = ( Base ` F ) )
8 1 a1i 
 |-  ( ( W e. LMod /\ X e. V ) -> V = ( Base ` W ) )
9 eqidd 
 |-  ( ( W e. LMod /\ X e. V ) -> ( +g ` W ) = ( +g ` W ) )
10 3 a1i 
 |-  ( ( W e. LMod /\ X e. V ) -> .x. = ( .s ` W ) )
11 5 a1i 
 |-  ( ( W e. LMod /\ X e. V ) -> S = ( LSubSp ` W ) )
12 1 2 3 4 lmodvscl 
 |-  ( ( W e. LMod /\ k e. K /\ X e. V ) -> ( k .x. X ) e. V )
13 12 3expa 
 |-  ( ( ( W e. LMod /\ k e. K ) /\ X e. V ) -> ( k .x. X ) e. V )
14 13 an32s 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> ( k .x. X ) e. V )
15 eleq1a 
 |-  ( ( k .x. X ) e. V -> ( v = ( k .x. X ) -> v e. V ) )
16 14 15 syl 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> ( v = ( k .x. X ) -> v e. V ) )
17 16 rexlimdva 
 |-  ( ( W e. LMod /\ X e. V ) -> ( E. k e. K v = ( k .x. X ) -> v e. V ) )
18 17 abssdv 
 |-  ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } C_ V )
19 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
20 2 4 19 lmod0cl 
 |-  ( W e. LMod -> ( 0g ` F ) e. K )
21 20 adantr 
 |-  ( ( W e. LMod /\ X e. V ) -> ( 0g ` F ) e. K )
22 nfcv 
 |-  F/_ k ( 0g ` F )
23 nfre1 
 |-  F/ k E. k e. K v = ( k .x. X )
24 23 nfab 
 |-  F/_ k { v | E. k e. K v = ( k .x. X ) }
25 nfcv 
 |-  F/_ k (/)
26 24 25 nfne 
 |-  F/ k { v | E. k e. K v = ( k .x. X ) } =/= (/)
27 biidd 
 |-  ( k = ( 0g ` F ) -> ( { v | E. k e. K v = ( k .x. X ) } =/= (/) <-> { v | E. k e. K v = ( k .x. X ) } =/= (/) ) )
28 ovex 
 |-  ( k .x. X ) e. _V
29 28 elabrex 
 |-  ( k e. K -> ( k .x. X ) e. { v | E. k e. K v = ( k .x. X ) } )
30 29 ne0d 
 |-  ( k e. K -> { v | E. k e. K v = ( k .x. X ) } =/= (/) )
31 22 26 27 30 vtoclgaf 
 |-  ( ( 0g ` F ) e. K -> { v | E. k e. K v = ( k .x. X ) } =/= (/) )
32 21 31 syl 
 |-  ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } =/= (/) )
33 vex 
 |-  a e. _V
34 eqeq1 
 |-  ( v = a -> ( v = ( k .x. X ) <-> a = ( k .x. X ) ) )
35 34 rexbidv 
 |-  ( v = a -> ( E. k e. K v = ( k .x. X ) <-> E. k e. K a = ( k .x. X ) ) )
36 33 35 elab 
 |-  ( a e. { v | E. k e. K v = ( k .x. X ) } <-> E. k e. K a = ( k .x. X ) )
37 oveq1 
 |-  ( k = y -> ( k .x. X ) = ( y .x. X ) )
38 37 eqeq2d 
 |-  ( k = y -> ( a = ( k .x. X ) <-> a = ( y .x. X ) ) )
39 38 cbvrexvw 
 |-  ( E. k e. K a = ( k .x. X ) <-> E. y e. K a = ( y .x. X ) )
40 36 39 bitri 
 |-  ( a e. { v | E. k e. K v = ( k .x. X ) } <-> E. y e. K a = ( y .x. X ) )
41 vex 
 |-  b e. _V
42 eqeq1 
 |-  ( v = b -> ( v = ( k .x. X ) <-> b = ( k .x. X ) ) )
43 42 rexbidv 
 |-  ( v = b -> ( E. k e. K v = ( k .x. X ) <-> E. k e. K b = ( k .x. X ) ) )
44 41 43 elab 
 |-  ( b e. { v | E. k e. K v = ( k .x. X ) } <-> E. k e. K b = ( k .x. X ) )
45 oveq1 
 |-  ( k = z -> ( k .x. X ) = ( z .x. X ) )
46 45 eqeq2d 
 |-  ( k = z -> ( b = ( k .x. X ) <-> b = ( z .x. X ) ) )
47 46 cbvrexvw 
 |-  ( E. k e. K b = ( k .x. X ) <-> E. z e. K b = ( z .x. X ) )
48 44 47 bitri 
 |-  ( b e. { v | E. k e. K v = ( k .x. X ) } <-> E. z e. K b = ( z .x. X ) )
49 40 48 anbi12i 
 |-  ( ( a e. { v | E. k e. K v = ( k .x. X ) } /\ b e. { v | E. k e. K v = ( k .x. X ) } ) <-> ( E. y e. K a = ( y .x. X ) /\ E. z e. K b = ( z .x. X ) ) )
50 reeanv 
 |-  ( E. y e. K E. z e. K ( a = ( y .x. X ) /\ b = ( z .x. X ) ) <-> ( E. y e. K a = ( y .x. X ) /\ E. z e. K b = ( z .x. X ) ) )
51 49 50 bitr4i 
 |-  ( ( a e. { v | E. k e. K v = ( k .x. X ) } /\ b e. { v | E. k e. K v = ( k .x. X ) } ) <-> E. y e. K E. z e. K ( a = ( y .x. X ) /\ b = ( z .x. X ) ) )
52 simpll 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> W e. LMod )
53 simprr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> x e. K )
54 simprll 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> y e. K )
55 eqid 
 |-  ( .r ` F ) = ( .r ` F )
56 2 4 55 lmodmcl 
 |-  ( ( W e. LMod /\ x e. K /\ y e. K ) -> ( x ( .r ` F ) y ) e. K )
57 52 53 54 56 syl3anc 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( x ( .r ` F ) y ) e. K )
58 simprlr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> z e. K )
59 eqid 
 |-  ( +g ` F ) = ( +g ` F )
60 2 4 59 lmodacl 
 |-  ( ( W e. LMod /\ ( x ( .r ` F ) y ) e. K /\ z e. K ) -> ( ( x ( .r ` F ) y ) ( +g ` F ) z ) e. K )
61 52 57 58 60 syl3anc 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( ( x ( .r ` F ) y ) ( +g ` F ) z ) e. K )
62 simplr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> X e. V )
63 eqid 
 |-  ( +g ` W ) = ( +g ` W )
64 1 63 2 3 4 59 lmodvsdir 
 |-  ( ( W e. LMod /\ ( ( x ( .r ` F ) y ) e. K /\ z e. K /\ X e. V ) ) -> ( ( ( x ( .r ` F ) y ) ( +g ` F ) z ) .x. X ) = ( ( ( x ( .r ` F ) y ) .x. X ) ( +g ` W ) ( z .x. X ) ) )
65 52 57 58 62 64 syl13anc 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( ( ( x ( .r ` F ) y ) ( +g ` F ) z ) .x. X ) = ( ( ( x ( .r ` F ) y ) .x. X ) ( +g ` W ) ( z .x. X ) ) )
66 1 2 3 4 55 lmodvsass 
 |-  ( ( W e. LMod /\ ( x e. K /\ y e. K /\ X e. V ) ) -> ( ( x ( .r ` F ) y ) .x. X ) = ( x .x. ( y .x. X ) ) )
67 52 53 54 62 66 syl13anc 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( ( x ( .r ` F ) y ) .x. X ) = ( x .x. ( y .x. X ) ) )
68 67 oveq1d 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( ( ( x ( .r ` F ) y ) .x. X ) ( +g ` W ) ( z .x. X ) ) = ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) )
69 65 68 eqtr2d 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) = ( ( ( x ( .r ` F ) y ) ( +g ` F ) z ) .x. X ) )
70 oveq1 
 |-  ( k = ( ( x ( .r ` F ) y ) ( +g ` F ) z ) -> ( k .x. X ) = ( ( ( x ( .r ` F ) y ) ( +g ` F ) z ) .x. X ) )
71 70 rspceeqv 
 |-  ( ( ( ( x ( .r ` F ) y ) ( +g ` F ) z ) e. K /\ ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) = ( ( ( x ( .r ` F ) y ) ( +g ` F ) z ) .x. X ) ) -> E. k e. K ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) = ( k .x. X ) )
72 61 69 71 syl2anc 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> E. k e. K ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) = ( k .x. X ) )
73 oveq2 
 |-  ( a = ( y .x. X ) -> ( x .x. a ) = ( x .x. ( y .x. X ) ) )
74 oveq12 
 |-  ( ( ( x .x. a ) = ( x .x. ( y .x. X ) ) /\ b = ( z .x. X ) ) -> ( ( x .x. a ) ( +g ` W ) b ) = ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) )
75 73 74 sylan 
 |-  ( ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> ( ( x .x. a ) ( +g ` W ) b ) = ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) )
76 75 eqeq1d 
 |-  ( ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> ( ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) <-> ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) = ( k .x. X ) ) )
77 76 rexbidv 
 |-  ( ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> ( E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) <-> E. k e. K ( ( x .x. ( y .x. X ) ) ( +g ` W ) ( z .x. X ) ) = ( k .x. X ) ) )
78 72 77 syl5ibrcom 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( ( y e. K /\ z e. K ) /\ x e. K ) ) -> ( ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) )
79 78 expr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( y e. K /\ z e. K ) ) -> ( x e. K -> ( ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) ) )
80 79 com23 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( y e. K /\ z e. K ) ) -> ( ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> ( x e. K -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) ) )
81 80 rexlimdvva 
 |-  ( ( W e. LMod /\ X e. V ) -> ( E. y e. K E. z e. K ( a = ( y .x. X ) /\ b = ( z .x. X ) ) -> ( x e. K -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) ) )
82 51 81 syl5bi 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( a e. { v | E. k e. K v = ( k .x. X ) } /\ b e. { v | E. k e. K v = ( k .x. X ) } ) -> ( x e. K -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) ) )
83 82 expcomd 
 |-  ( ( W e. LMod /\ X e. V ) -> ( b e. { v | E. k e. K v = ( k .x. X ) } -> ( a e. { v | E. k e. K v = ( k .x. X ) } -> ( x e. K -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) ) ) )
84 83 com24 
 |-  ( ( W e. LMod /\ X e. V ) -> ( x e. K -> ( a e. { v | E. k e. K v = ( k .x. X ) } -> ( b e. { v | E. k e. K v = ( k .x. X ) } -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) ) ) )
85 84 3imp2 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( x e. K /\ a e. { v | E. k e. K v = ( k .x. X ) } /\ b e. { v | E. k e. K v = ( k .x. X ) } ) ) -> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) )
86 ovex 
 |-  ( ( x .x. a ) ( +g ` W ) b ) e. _V
87 eqeq1 
 |-  ( v = ( ( x .x. a ) ( +g ` W ) b ) -> ( v = ( k .x. X ) <-> ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) )
88 87 rexbidv 
 |-  ( v = ( ( x .x. a ) ( +g ` W ) b ) -> ( E. k e. K v = ( k .x. X ) <-> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) ) )
89 86 88 elab 
 |-  ( ( ( x .x. a ) ( +g ` W ) b ) e. { v | E. k e. K v = ( k .x. X ) } <-> E. k e. K ( ( x .x. a ) ( +g ` W ) b ) = ( k .x. X ) )
90 85 89 sylibr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ ( x e. K /\ a e. { v | E. k e. K v = ( k .x. X ) } /\ b e. { v | E. k e. K v = ( k .x. X ) } ) ) -> ( ( x .x. a ) ( +g ` W ) b ) e. { v | E. k e. K v = ( k .x. X ) } )
91 6 7 8 9 10 11 18 32 90 islssd 
 |-  ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } e. S )