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 e. ~H
nonbool.2 
|- B e. ~H
nonbool.3 
|- F = ( span ` { A } )
nonbool.4 
|- G = ( span ` { B } )
nonbool.5 
|- H = ( span ` { ( A +h B ) } )
Assertion nonbooli 
|- ( -. ( A e. G \/ B e. F ) -> ( H i^i ( F vH G ) ) =/= ( ( H i^i F ) vH ( H i^i G ) ) )

Proof

Step Hyp Ref Expression
1 nonbool.1 
 |-  A e. ~H
2 nonbool.2 
 |-  B e. ~H
3 nonbool.3 
 |-  F = ( span ` { A } )
4 nonbool.4 
 |-  G = ( span ` { B } )
5 nonbool.5 
 |-  H = ( span ` { ( A +h B ) } )
6 1 2 hvaddcli 
 |-  ( A +h B ) e. ~H
7 spansnid 
 |-  ( ( A +h B ) e. ~H -> ( A +h B ) e. ( span ` { ( A +h B ) } ) )
8 6 7 ax-mp 
 |-  ( A +h B ) e. ( span ` { ( A +h B ) } )
9 8 5 eleqtrri 
 |-  ( A +h B ) e. H
10 1 spansnchi 
 |-  ( span ` { A } ) e. CH
11 10 chshii 
 |-  ( span ` { A } ) e. SH
12 3 11 eqeltri 
 |-  F e. SH
13 2 spansnchi 
 |-  ( span ` { B } ) e. CH
14 13 chshii 
 |-  ( span ` { B } ) e. SH
15 4 14 eqeltri 
 |-  G e. SH
16 12 15 shsleji 
 |-  ( F +H G ) C_ ( F vH G )
17 spansnid 
 |-  ( A e. ~H -> A e. ( span ` { A } ) )
18 1 17 ax-mp 
 |-  A e. ( span ` { A } )
19 18 3 eleqtrri 
 |-  A e. F
20 spansnid 
 |-  ( B e. ~H -> B e. ( span ` { B } ) )
21 2 20 ax-mp 
 |-  B e. ( span ` { B } )
22 21 4 eleqtrri 
 |-  B e. G
23 12 15 shsvai 
 |-  ( ( A e. F /\ B e. G ) -> ( A +h B ) e. ( F +H G ) )
24 19 22 23 mp2an 
 |-  ( A +h B ) e. ( F +H G )
25 16 24 sselii 
 |-  ( A +h B ) e. ( F vH G )
26 elin 
 |-  ( ( A +h B ) e. ( H i^i ( F vH G ) ) <-> ( ( A +h B ) e. H /\ ( A +h B ) e. ( F vH G ) ) )
27 9 25 26 mpbir2an 
 |-  ( A +h B ) e. ( H i^i ( F vH G ) )
28 eleq2 
 |-  ( ( H i^i ( F vH G ) ) = 0H -> ( ( A +h B ) e. ( H i^i ( F vH G ) ) <-> ( A +h B ) e. 0H ) )
29 27 28 mpbii 
 |-  ( ( H i^i ( F vH G ) ) = 0H -> ( A +h B ) e. 0H )
30 elch0 
 |-  ( ( A +h B ) e. 0H <-> ( A +h B ) = 0h )
31 29 30 sylib 
 |-  ( ( H i^i ( F vH G ) ) = 0H -> ( A +h B ) = 0h )
32 ch0 
 |-  ( ( span ` { A } ) e. CH -> 0h e. ( span ` { A } ) )
33 10 32 ax-mp 
 |-  0h e. ( span ` { A } )
34 31 33 eqeltrdi 
 |-  ( ( H i^i ( F vH G ) ) = 0H -> ( A +h B ) e. ( span ` { A } ) )
35 3 eleq2i 
 |-  ( B e. F <-> B e. ( span ` { A } ) )
36 sumspansn 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) )
37 1 2 36 mp2an 
 |-  ( ( A +h B ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) )
38 35 37 bitr4i 
 |-  ( B e. F <-> ( A +h B ) e. ( span ` { A } ) )
39 34 38 sylibr 
 |-  ( ( H i^i ( F vH G ) ) = 0H -> B e. F )
40 39 con3i 
 |-  ( -. B e. F -> -. ( H i^i ( F vH G ) ) = 0H )
41 40 adantl 
 |-  ( ( -. A e. G /\ -. B e. F ) -> -. ( H i^i ( F vH G ) ) = 0H )
42 5 3 ineq12i 
 |-  ( H i^i F ) = ( ( span ` { ( A +h B ) } ) i^i ( span ` { A } ) )
43 6 1 spansnm0i 
 |-  ( -. ( A +h B ) e. ( span ` { A } ) -> ( ( span ` { ( A +h B ) } ) i^i ( span ` { A } ) ) = 0H )
44 38 43 sylnbi 
 |-  ( -. B e. F -> ( ( span ` { ( A +h B ) } ) i^i ( span ` { A } ) ) = 0H )
45 42 44 syl5eq 
 |-  ( -. B e. F -> ( H i^i F ) = 0H )
46 5 4 ineq12i 
 |-  ( H i^i G ) = ( ( span ` { ( A +h B ) } ) i^i ( span ` { B } ) )
47 sumspansn 
 |-  ( ( B e. ~H /\ A e. ~H ) -> ( ( B +h A ) e. ( span ` { B } ) <-> A e. ( span ` { B } ) ) )
48 2 1 47 mp2an 
 |-  ( ( B +h A ) e. ( span ` { B } ) <-> A e. ( span ` { B } ) )
49 1 2 hvcomi 
 |-  ( A +h B ) = ( B +h A )
50 49 eleq1i 
 |-  ( ( A +h B ) e. ( span ` { B } ) <-> ( B +h A ) e. ( span ` { B } ) )
51 4 eleq2i 
 |-  ( A e. G <-> A e. ( span ` { B } ) )
52 48 50 51 3bitr4ri 
 |-  ( A e. G <-> ( A +h B ) e. ( span ` { B } ) )
53 6 2 spansnm0i 
 |-  ( -. ( A +h B ) e. ( span ` { B } ) -> ( ( span ` { ( A +h B ) } ) i^i ( span ` { B } ) ) = 0H )
54 52 53 sylnbi 
 |-  ( -. A e. G -> ( ( span ` { ( A +h B ) } ) i^i ( span ` { B } ) ) = 0H )
55 46 54 syl5eq 
 |-  ( -. A e. G -> ( H i^i G ) = 0H )
56 45 55 oveqan12rd 
 |-  ( ( -. A e. G /\ -. B e. F ) -> ( ( H i^i F ) vH ( H i^i G ) ) = ( 0H vH 0H ) )
57 h0elch 
 |-  0H e. CH
58 57 chj0i 
 |-  ( 0H vH 0H ) = 0H
59 56 58 eqtrdi 
 |-  ( ( -. A e. G /\ -. B e. F ) -> ( ( H i^i F ) vH ( H i^i G ) ) = 0H )
60 eqeq2 
 |-  ( ( ( H i^i F ) vH ( H i^i G ) ) = 0H -> ( ( H i^i ( F vH G ) ) = ( ( H i^i F ) vH ( H i^i G ) ) <-> ( H i^i ( F vH G ) ) = 0H ) )
61 60 notbid 
 |-  ( ( ( H i^i F ) vH ( H i^i G ) ) = 0H -> ( -. ( H i^i ( F vH G ) ) = ( ( H i^i F ) vH ( H i^i G ) ) <-> -. ( H i^i ( F vH G ) ) = 0H ) )
62 61 biimparc 
 |-  ( ( -. ( H i^i ( F vH G ) ) = 0H /\ ( ( H i^i F ) vH ( H i^i G ) ) = 0H ) -> -. ( H i^i ( F vH G ) ) = ( ( H i^i F ) vH ( H i^i G ) ) )
63 41 59 62 syl2anc 
 |-  ( ( -. A e. G /\ -. B e. F ) -> -. ( H i^i ( F vH G ) ) = ( ( H i^i F ) vH ( H i^i G ) ) )
64 ioran 
 |-  ( -. ( A e. G \/ B e. F ) <-> ( -. A e. G /\ -. B e. F ) )
65 df-ne 
 |-  ( ( H i^i ( F vH G ) ) =/= ( ( H i^i F ) vH ( H i^i G ) ) <-> -. ( H i^i ( F vH G ) ) = ( ( H i^i F ) vH ( H i^i G ) ) )
66 63 64 65 3imtr4i 
 |-  ( -. ( A e. G \/ B e. F ) -> ( H i^i ( F vH G ) ) =/= ( ( H i^i F ) vH ( H i^i G ) ) )