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	⊢ 𝐴 ∈ ℋ
	nonbool.2	⊢ 𝐵 ∈ ℋ
	nonbool.3	⊢ 𝐹 = ( span ‘ { 𝐴 } )
	nonbool.4	⊢ 𝐺 = ( span ‘ { 𝐵 } )
	nonbool.5	⊢ 𝐻 = ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } )
Assertion	nonbooli	⊢ ( ¬ ( 𝐴 ∈ 𝐺 ∨ 𝐵 ∈ 𝐹 ) → ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ≠ ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nonbool.1	⊢ 𝐴 ∈ ℋ
2		nonbool.2	⊢ 𝐵 ∈ ℋ
3		nonbool.3	⊢ 𝐹 = ( span ‘ { 𝐴 } )
4		nonbool.4	⊢ 𝐺 = ( span ‘ { 𝐵 } )
5		nonbool.5	⊢ 𝐻 = ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } )
6	1 2	hvaddcli	⊢ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ
7		spansnid	⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) )
8	6 7	ax-mp	⊢ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } )
9	8 5	eleqtrri	⊢ ( 𝐴 +ℎ 𝐵 ) ∈ 𝐻
10	1	spansnchi	⊢ ( span ‘ { 𝐴 } ) ∈ Cℋ
11	10	chshii	⊢ ( span ‘ { 𝐴 } ) ∈ Sℋ
12	3 11	eqeltri	⊢ 𝐹 ∈ Sℋ
13	2	spansnchi	⊢ ( span ‘ { 𝐵 } ) ∈ Cℋ
14	13	chshii	⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ
15	4 14	eqeltri	⊢ 𝐺 ∈ Sℋ
16	12 15	shsleji	⊢ ( 𝐹 +ℋ 𝐺 ) ⊆ ( 𝐹 ∨ℋ 𝐺 )
17		spansnid	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
18	1 17	ax-mp	⊢ 𝐴 ∈ ( span ‘ { 𝐴 } )
19	18 3	eleqtrri	⊢ 𝐴 ∈ 𝐹
20		spansnid	⊢ ( 𝐵 ∈ ℋ → 𝐵 ∈ ( span ‘ { 𝐵 } ) )
21	2 20	ax-mp	⊢ 𝐵 ∈ ( span ‘ { 𝐵 } )
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	⊢ ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ↔ ( 𝐴 +ℎ 𝐵 ) ∈ 0ℋ ) )
29	27 28	mpbii	⊢ ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ → ( 𝐴 +ℎ 𝐵 ) ∈ 0ℋ )
30		elch0	⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ 0ℋ ↔ ( 𝐴 +ℎ 𝐵 ) = 0ℎ )
31	29 30	sylib	⊢ ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ → ( 𝐴 +ℎ 𝐵 ) = 0ℎ )
32		ch0	⊢ ( ( span ‘ { 𝐴 } ) ∈ Cℋ → 0ℎ ∈ ( span ‘ { 𝐴 } ) )
33	10 32	ax-mp	⊢ 0ℎ ∈ ( span ‘ { 𝐴 } )
34	31 33	eqeltrdi	⊢ ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
35	3	eleq2i	⊢ ( 𝐵 ∈ 𝐹 ↔ 𝐵 ∈ ( span ‘ { 𝐴 } ) )
36		sumspansn	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( span ‘ { 𝐴 } ) ) )
37	1 2 36	mp2an	⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( span ‘ { 𝐴 } ) )
38	35 37	bitr4i	⊢ ( 𝐵 ∈ 𝐹 ↔ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
39	34 38	sylibr	⊢ ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ → 𝐵 ∈ 𝐹 )
40	39	con3i	⊢ ( ¬ 𝐵 ∈ 𝐹 → ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ )
41	40	adantl	⊢ ( ( ¬ 𝐴 ∈ 𝐺 ∧ ¬ 𝐵 ∈ 𝐹 ) → ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ )
42	5 3	ineq12i	⊢ ( 𝐻 ∩ 𝐹 ) = ( ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ∩ ( span ‘ { 𝐴 } ) )
43	6 1	spansnm0i	⊢ ( ¬ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) → ( ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ∩ ( span ‘ { 𝐴 } ) ) = 0ℋ )
44	38 43	sylnbi	⊢ ( ¬ 𝐵 ∈ 𝐹 → ( ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ∩ ( span ‘ { 𝐴 } ) ) = 0ℋ )
45	42 44	syl5eq	⊢ ( ¬ 𝐵 ∈ 𝐹 → ( 𝐻 ∩ 𝐹 ) = 0ℋ )
46	5 4	ineq12i	⊢ ( 𝐻 ∩ 𝐺 ) = ( ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ∩ ( span ‘ { 𝐵 } ) )
47		sumspansn	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝐵 +ℎ 𝐴 ) ∈ ( span ‘ { 𝐵 } ) ↔ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) )
48	2 1 47	mp2an	⊢ ( ( 𝐵 +ℎ 𝐴 ) ∈ ( span ‘ { 𝐵 } ) ↔ 𝐴 ∈ ( span ‘ { 𝐵 } ) )
49	1 2	hvcomi	⊢ ( 𝐴 +ℎ 𝐵 ) = ( 𝐵 +ℎ 𝐴 )
50	49	eleq1i	⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) ↔ ( 𝐵 +ℎ 𝐴 ) ∈ ( span ‘ { 𝐵 } ) )
51	4	eleq2i	⊢ ( 𝐴 ∈ 𝐺 ↔ 𝐴 ∈ ( span ‘ { 𝐵 } ) )
52	48 50 51	3bitr4ri	⊢ ( 𝐴 ∈ 𝐺 ↔ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) )
53	6 2	spansnm0i	⊢ ( ¬ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )
54	52 53	sylnbi	⊢ ( ¬ 𝐴 ∈ 𝐺 → ( ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )
55	46 54	syl5eq	⊢ ( ¬ 𝐴 ∈ 𝐺 → ( 𝐻 ∩ 𝐺 ) = 0ℋ )
56	45 55	oveqan12rd	⊢ ( ( ¬ 𝐴 ∈ 𝐺 ∧ ¬ 𝐵 ∈ 𝐹 ) → ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) = ( 0ℋ ∨ℋ 0ℋ ) )
57		h0elch	⊢ 0ℋ ∈ Cℋ
58	57	chj0i	⊢ ( 0ℋ ∨ℋ 0ℋ ) = 0ℋ
59	56 58	eqtrdi	⊢ ( ( ¬ 𝐴 ∈ 𝐺 ∧ ¬ 𝐵 ∈ 𝐹 ) → ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) = 0ℋ )
60		eqeq2	⊢ ( ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) = 0ℋ → ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) ↔ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ ) )
61	60	notbid	⊢ ( ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) = 0ℋ → ( ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) ↔ ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ ) )
62	61	biimparc	⊢ ( ( ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = 0ℋ ∧ ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) = 0ℋ ) → ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) )
63	41 59 62	syl2anc	⊢ ( ( ¬ 𝐴 ∈ 𝐺 ∧ ¬ 𝐵 ∈ 𝐹 ) → ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) )
64		ioran	⊢ ( ¬ ( 𝐴 ∈ 𝐺 ∨ 𝐵 ∈ 𝐹 ) ↔ ( ¬ 𝐴 ∈ 𝐺 ∧ ¬ 𝐵 ∈ 𝐹 ) )
65		df-ne	⊢ ( ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ≠ ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) ↔ ¬ ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) = ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) )
66	63 64 65	3imtr4i	⊢ ( ¬ ( 𝐴 ∈ 𝐺 ∨ 𝐵 ∈ 𝐹 ) → ( 𝐻 ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ≠ ( ( 𝐻 ∩ 𝐹 ) ∨ℋ ( 𝐻 ∩ 𝐺 ) ) )