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\in \mathscr{H}$$
	nonbool.2	$$⊢B\in \mathscr{H}$$
	nonbool.3	$$⊢F=\mathrm{span}\left(\left\{A\right\}\right)$$
	nonbool.4	$$⊢G=\mathrm{span}\left(\left\{B\right\}\right)$$
	nonbool.5	$$⊢H=\mathrm{span}\left(\left\{A{+}_{ℎ}B\right\}\right)$$
Assertion	nonbooli	$$⊢\neg \left(A\in G\vee B\in F\right)\to H\cap \left(F{\vee }_{\mathscr{H}}G\right)\ne \left(H\cap F\right){\vee }_{\mathscr{H}}\left(H\cap G\right)$$

Proof

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