Metamath Proof Explorer


Theorem nonbooli

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 A
nonbool.2 B
nonbool.3 F=spanA
nonbool.4 G=spanB
nonbool.5 H=spanA+B
Assertion nonbooli ¬AGBFHFGHFHG

Proof

Step Hyp Ref Expression
1 nonbool.1 A
2 nonbool.2 B
3 nonbool.3 F=spanA
4 nonbool.4 G=spanB
5 nonbool.5 H=spanA+B
6 1 2 hvaddcli A+B
7 spansnid A+BA+BspanA+B
8 6 7 ax-mp A+BspanA+B
9 8 5 eleqtrri A+BH
10 1 spansnchi spanAC
11 10 chshii spanAS
12 3 11 eqeltri FS
13 2 spansnchi spanBC
14 13 chshii spanBS
15 4 14 eqeltri GS
16 12 15 shsleji F+GFG
17 spansnid AAspanA
18 1 17 ax-mp AspanA
19 18 3 eleqtrri AF
20 spansnid BBspanB
21 2 20 ax-mp BspanB
22 21 4 eleqtrri BG
23 12 15 shsvai AFBGA+BF+G
24 19 22 23 mp2an A+BF+G
25 16 24 sselii A+BFG
26 elin A+BHFGA+BHA+BFG
27 9 25 26 mpbir2an A+BHFG
28 eleq2 HFG=0A+BHFGA+B0
29 27 28 mpbii HFG=0A+B0
30 elch0 A+B0A+B=0
31 29 30 sylib HFG=0A+B=0
32 ch0 spanAC0spanA
33 10 32 ax-mp 0spanA
34 31 33 eqeltrdi HFG=0A+BspanA
35 3 eleq2i BFBspanA
36 sumspansn ABA+BspanABspanA
37 1 2 36 mp2an A+BspanABspanA
38 35 37 bitr4i BFA+BspanA
39 34 38 sylibr HFG=0BF
40 39 con3i ¬BF¬HFG=0
41 40 adantl ¬AG¬BF¬HFG=0
42 5 3 ineq12i HF=spanA+BspanA
43 6 1 spansnm0i ¬A+BspanAspanA+BspanA=0
44 38 43 sylnbi ¬BFspanA+BspanA=0
45 42 44 eqtrid ¬BFHF=0
46 5 4 ineq12i HG=spanA+BspanB
47 sumspansn BAB+AspanBAspanB
48 2 1 47 mp2an B+AspanBAspanB
49 1 2 hvcomi A+B=B+A
50 49 eleq1i A+BspanBB+AspanB
51 4 eleq2i AGAspanB
52 48 50 51 3bitr4ri AGA+BspanB
53 6 2 spansnm0i ¬A+BspanBspanA+BspanB=0
54 52 53 sylnbi ¬AGspanA+BspanB=0
55 46 54 eqtrid ¬AGHG=0
56 45 55 oveqan12rd ¬AG¬BFHFHG=00
57 h0elch 0C
58 57 chj0i 00=0
59 56 58 eqtrdi ¬AG¬BFHFHG=0
60 eqeq2 HFHG=0HFG=HFHGHFG=0
61 60 notbid HFHG=0¬HFG=HFHG¬HFG=0
62 61 biimparc ¬HFG=0HFHG=0¬HFG=HFHG
63 41 59 62 syl2anc ¬AG¬BF¬HFG=HFHG
64 ioran ¬AGBF¬AG¬BF
65 df-ne HFGHFHG¬HFG=HFHG
66 63 64 65 3imtr4i ¬AGBFHFGHFHG