Description: A basis element is in the orthocomplement of a subset of the basis iff it is not in the subset. (Contributed by Mario Carneiro, 23-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | obselocv.o | |
|
Assertion | obselocv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | obselocv.o | |
|
2 | eqid | |
|
3 | 2 | obsne0 | |
4 | 3 | 3adant2 | |
5 | elin | |
|
6 | obsrcl | |
|
7 | 6 | 3ad2ant1 | |
8 | phllmod | |
|
9 | 7 8 | syl | |
10 | simp2 | |
|
11 | eqid | |
|
12 | 11 | obsss | |
13 | 12 | 3ad2ant1 | |
14 | 10 13 | sstrd | |
15 | eqid | |
|
16 | 11 15 | lspssid | |
17 | 9 14 16 | syl2anc | |
18 | 17 | ssrind | |
19 | 11 1 15 | ocvlsp | |
20 | 7 14 19 | syl2anc | |
21 | 20 | ineq2d | |
22 | eqid | |
|
23 | 11 22 15 | lspcl | |
24 | 9 14 23 | syl2anc | |
25 | 1 22 2 | ocvin | |
26 | 7 24 25 | syl2anc | |
27 | 21 26 | eqtr3d | |
28 | 18 27 | sseqtrd | |
29 | 28 | sseld | |
30 | 5 29 | syl5bir | |
31 | elsni | |
|
32 | 30 31 | syl6 | |
33 | 32 | necon3ad | |
34 | 4 33 | mpd | |
35 | imnan | |
|
36 | 34 35 | sylibr | |
37 | 36 | con2d | |
38 | simpr | |
|
39 | eleq1 | |
|
40 | 38 39 | syl5ibrcom | |
41 | 40 | con3d | |
42 | simpl1 | |
|
43 | simpl3 | |
|
44 | 10 | sselda | |
45 | eqid | |
|
46 | eqid | |
|
47 | eqid | |
|
48 | eqid | |
|
49 | 11 45 46 47 48 | obsip | |
50 | 42 43 44 49 | syl3anc | |
51 | iffalse | |
|
52 | 51 | eqeq2d | |
53 | 50 52 | syl5ibcom | |
54 | 41 53 | syld | |
55 | 54 | ralrimdva | |
56 | simp3 | |
|
57 | 13 56 | sseldd | |
58 | 11 45 46 48 1 | elocv | |
59 | df-3an | |
|
60 | 58 59 | bitri | |
61 | 60 | baib | |
62 | 14 57 61 | syl2anc | |
63 | 55 62 | sylibrd | |
64 | 37 63 | impbid | |