Description: Lemma for lclkr . When B is nonzero, the vectors X and Y can't both belong to the hyperplane generated by B . (Contributed by NM, 17-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lclkrlem2m.v | |
|
lclkrlem2m.t | |
||
lclkrlem2m.s | |
||
lclkrlem2m.q | |
||
lclkrlem2m.z | |
||
lclkrlem2m.i | |
||
lclkrlem2m.m | |
||
lclkrlem2m.f | |
||
lclkrlem2m.d | |
||
lclkrlem2m.p | |
||
lclkrlem2m.x | |
||
lclkrlem2m.y | |
||
lclkrlem2m.e | |
||
lclkrlem2m.g | |
||
lclkrlem2n.n | |
||
lclkrlem2n.l | |
||
lclkrlem2o.h | |
||
lclkrlem2o.o | |
||
lclkrlem2o.u | |
||
lclkrlem2o.a | |
||
lclkrlem2o.k | |
||
lclkrlem2o.b | |
||
lclkrlem2o.n | |
||
lclkrlem2o.bn | |
||
Assertion | lclkrlem2o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lclkrlem2m.v | |
|
2 | lclkrlem2m.t | |
|
3 | lclkrlem2m.s | |
|
4 | lclkrlem2m.q | |
|
5 | lclkrlem2m.z | |
|
6 | lclkrlem2m.i | |
|
7 | lclkrlem2m.m | |
|
8 | lclkrlem2m.f | |
|
9 | lclkrlem2m.d | |
|
10 | lclkrlem2m.p | |
|
11 | lclkrlem2m.x | |
|
12 | lclkrlem2m.y | |
|
13 | lclkrlem2m.e | |
|
14 | lclkrlem2m.g | |
|
15 | lclkrlem2n.n | |
|
16 | lclkrlem2n.l | |
|
17 | lclkrlem2o.h | |
|
18 | lclkrlem2o.o | |
|
19 | lclkrlem2o.u | |
|
20 | lclkrlem2o.a | |
|
21 | lclkrlem2o.k | |
|
22 | lclkrlem2o.b | |
|
23 | lclkrlem2o.n | |
|
24 | lclkrlem2o.bn | |
|
25 | eqid | |
|
26 | 17 19 21 | dvhlvec | |
27 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 22 23 | lclkrlem2m | |
28 | 27 | simpld | |
29 | eldifsn | |
|
30 | 28 24 29 | sylanbrc | |
31 | 17 18 19 1 25 21 30 | dochnel | |
32 | 17 19 21 | dvhlmod | |
33 | 32 | adantr | |
34 | 28 | snssd | |
35 | eqid | |
|
36 | 17 19 1 35 18 | dochlss | |
37 | 21 34 36 | syl2anc | |
38 | 37 | adantr | |
39 | simprl | |
|
40 | 3 | lmodring | |
41 | 32 40 | syl | |
42 | 8 9 10 32 13 14 | ldualvaddcl | |
43 | eqid | |
|
44 | 3 43 1 8 | lflcl | |
45 | 32 42 11 44 | syl3anc | |
46 | 3 | lvecdrng | |
47 | 26 46 | syl | |
48 | 3 43 1 8 | lflcl | |
49 | 32 42 12 48 | syl3anc | |
50 | 43 5 6 | drnginvrcl | |
51 | 47 49 23 50 | syl3anc | |
52 | 43 4 | ringcl | |
53 | 41 45 51 52 | syl3anc | |
54 | 53 | adantr | |
55 | simprr | |
|
56 | 3 2 43 35 | lssvscl | |
57 | 33 38 54 55 56 | syl22anc | |
58 | 7 35 | lssvsubcl | |
59 | 33 38 39 57 58 | syl22anc | |
60 | 22 59 | eqeltrid | |
61 | 31 60 | mtand | |
62 | ianor | |
|
63 | 61 62 | sylib | |