Description: A Hilbert lattice with two or more dimensions fails the distributive law and therefore cannot be a Boolean algebra. This counterexample demonstrates a condition where ( ( H i^i F ) vH ( H i^i G ) ) = 0H but ( H i^i ( F vH G ) ) =/= 0H . The antecedent specifies that the vectors A and B are nonzero and non-colinear. The last three hypotheses assign one-dimensional subspaces to F , G , and H . (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nonbool.1 | |
|
nonbool.2 | |
||
nonbool.3 | |
||
nonbool.4 | |
||
nonbool.5 | |
||
Assertion | nonbooli | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nonbool.1 | |
|
2 | nonbool.2 | |
|
3 | nonbool.3 | |
|
4 | nonbool.4 | |
|
5 | nonbool.5 | |
|
6 | 1 2 | hvaddcli | |
7 | spansnid | |
|
8 | 6 7 | ax-mp | |
9 | 8 5 | eleqtrri | |
10 | 1 | spansnchi | |
11 | 10 | chshii | |
12 | 3 11 | eqeltri | |
13 | 2 | spansnchi | |
14 | 13 | chshii | |
15 | 4 14 | eqeltri | |
16 | 12 15 | shsleji | |
17 | spansnid | |
|
18 | 1 17 | ax-mp | |
19 | 18 3 | eleqtrri | |
20 | spansnid | |
|
21 | 2 20 | ax-mp | |
22 | 21 4 | eleqtrri | |
23 | 12 15 | shsvai | |
24 | 19 22 23 | mp2an | |
25 | 16 24 | sselii | |
26 | elin | |
|
27 | 9 25 26 | mpbir2an | |
28 | eleq2 | |
|
29 | 27 28 | mpbii | |
30 | elch0 | |
|
31 | 29 30 | sylib | |
32 | ch0 | |
|
33 | 10 32 | ax-mp | |
34 | 31 33 | eqeltrdi | |
35 | 3 | eleq2i | |
36 | sumspansn | |
|
37 | 1 2 36 | mp2an | |
38 | 35 37 | bitr4i | |
39 | 34 38 | sylibr | |
40 | 39 | con3i | |
41 | 40 | adantl | |
42 | 5 3 | ineq12i | |
43 | 6 1 | spansnm0i | |
44 | 38 43 | sylnbi | |
45 | 42 44 | eqtrid | |
46 | 5 4 | ineq12i | |
47 | sumspansn | |
|
48 | 2 1 47 | mp2an | |
49 | 1 2 | hvcomi | |
50 | 49 | eleq1i | |
51 | 4 | eleq2i | |
52 | 48 50 51 | 3bitr4ri | |
53 | 6 2 | spansnm0i | |
54 | 52 53 | sylnbi | |
55 | 46 54 | eqtrid | |
56 | 45 55 | oveqan12rd | |
57 | h0elch | |
|
58 | 57 | chj0i | |
59 | 56 58 | eqtrdi | |
60 | eqeq2 | |
|
61 | 60 | notbid | |
62 | 61 | biimparc | |
63 | 41 59 62 | syl2anc | |
64 | ioran | |
|
65 | df-ne | |
|
66 | 63 64 65 | 3imtr4i | |