Description: Lemma for lclkr . When the hypotheses of lclkrlem2u and lclkrlem2u are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid , which requires the orthomodular law dihoml4 (Lemma 3.3 of Holland95 p. 214). (Contributed by NM, 16-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 | |
||
lclkrlem2q.le | |
||
lclkrlem2q.lg | |
||
lclkrlem2v.j | |
||
lclkrlem2v.k | |
||
Assertion | lclkrlem2v | |
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 | lclkrlem2q.le | |
|
23 | lclkrlem2q.lg | |
|
24 | lclkrlem2v.j | |
|
25 | lclkrlem2v.k | |
|
26 | 17 19 21 | dvhlmod | |
27 | 8 9 10 26 13 14 | ldualvaddcl | |
28 | 1 8 16 26 27 | lkrssv | |
29 | eqid | |
|
30 | 1 29 15 26 11 12 | lspprcl | |
31 | eqid | |
|
32 | 17 19 1 15 31 21 11 12 | dihprrn | |
33 | 1 29 | lssss | |
34 | 30 33 | syl | |
35 | 17 31 19 1 18 21 34 | dochoccl | |
36 | 32 35 | mpbid | |
37 | 17 18 19 1 29 20 21 30 36 | dochexmid | |
38 | 17 19 21 | dvhlvec | |
39 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 38 24 25 | lclkrlem2n | |
40 | 11 | snssd | |
41 | 12 | snssd | |
42 | 17 19 1 18 | dochdmj1 | |
43 | 21 40 41 42 | syl3anc | |
44 | df-pr | |
|
45 | 44 | fveq2i | |
46 | 45 | fveq2i | |
47 | 40 41 | unssd | |
48 | 17 19 18 1 15 21 47 | dochocsp | |
49 | 46 48 | eqtrid | |
50 | 22 23 | ineq12d | |
51 | 43 49 50 | 3eqtr4d | |
52 | 8 16 9 10 26 13 14 | lkrin | |
53 | 51 52 | eqsstrd | |
54 | 29 | lsssssubg | |
55 | 26 54 | syl | |
56 | 55 30 | sseldd | |
57 | 17 19 1 29 18 | dochlss | |
58 | 21 34 57 | syl2anc | |
59 | 55 58 | sseldd | |
60 | 8 16 29 | lkrlss | |
61 | 26 27 60 | syl2anc | |
62 | 55 61 | sseldd | |
63 | 20 | lsmlub | |
64 | 56 59 62 63 | syl3anc | |
65 | 39 53 64 | mpbi2and | |
66 | 37 65 | eqsstrrd | |
67 | 28 66 | eqssd | |