Description: A nonzero scalar multiple of a unit vector not included in a support-restriction subspace is not included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 24-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frlmssuvc1.f | |
|
frlmssuvc1.u | |
||
frlmssuvc1.b | |
||
frlmssuvc1.k | |
||
frlmssuvc1.t | |
||
frlmssuvc1.z | |
||
frlmssuvc1.c | |
||
frlmssuvc1.r | |
||
frlmssuvc1.i | |
||
frlmssuvc1.j | |
||
frlmssuvc2.l | |
||
frlmssuvc2.x | |
||
Assertion | frlmssuvc2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frlmssuvc1.f | |
|
2 | frlmssuvc1.u | |
|
3 | frlmssuvc1.b | |
|
4 | frlmssuvc1.k | |
|
5 | frlmssuvc1.t | |
|
6 | frlmssuvc1.z | |
|
7 | frlmssuvc1.c | |
|
8 | frlmssuvc1.r | |
|
9 | frlmssuvc1.i | |
|
10 | frlmssuvc1.j | |
|
11 | frlmssuvc2.l | |
|
12 | frlmssuvc2.x | |
|
13 | fveq2 | |
|
14 | 13 | neeq1d | |
15 | 11 | eldifad | |
16 | 12 | eldifad | |
17 | 2 1 3 | uvcff | |
18 | 8 9 17 | syl2anc | |
19 | 18 15 | ffvelrnd | |
20 | eqid | |
|
21 | 1 3 4 9 16 19 15 5 20 | frlmvscaval | |
22 | eqid | |
|
23 | 2 8 9 15 22 | uvcvv1 | |
24 | 23 | oveq2d | |
25 | 4 20 22 | ringridm | |
26 | 8 16 25 | syl2anc | |
27 | 21 24 26 | 3eqtrd | |
28 | eldifsni | |
|
29 | 12 28 | syl | |
30 | 27 29 | eqnetrd | |
31 | 14 15 30 | elrabd | |
32 | 11 | eldifbd | |
33 | nelss | |
|
34 | 31 32 33 | syl2anc | |
35 | 1 | frlmlmod | |
36 | 8 9 35 | syl2anc | |
37 | 1 | frlmsca | |
38 | 8 9 37 | syl2anc | |
39 | 38 | fveq2d | |
40 | 4 39 | eqtrid | |
41 | 16 40 | eleqtrd | |
42 | eqid | |
|
43 | eqid | |
|
44 | 3 42 5 43 | lmodvscl | |
45 | 36 41 19 44 | syl3anc | |
46 | 1 4 3 | frlmbasf | |
47 | 9 45 46 | syl2anc | |
48 | 47 | ffnd | |
49 | 6 | fvexi | |
50 | 49 | a1i | |
51 | suppvalfn | |
|
52 | 48 9 50 51 | syl3anc | |
53 | 52 | sseq1d | |
54 | 34 53 | mtbird | |
55 | 54 | intnand | |
56 | oveq1 | |
|
57 | 56 | sseq1d | |
58 | 57 7 | elrab2 | |
59 | 55 58 | sylnibr | |