Theorem mlaconj4 844

Description: For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper. (Contributed by NM, 8-Jul-2000.)

Hypotheses

Ref	Expression
mlaconj4.1	((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (d ≡ c)
mlaconj4.2	d = (a ∪ b)
mlaconj4.3	e = (a ∩ b)

Assertion

Ref	Expression
mlaconj4	((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)

Proof of Theorem mlaconj4

Step	Hyp	Ref	Expression
1		biao 799	. . . . 5 (a ≡ b) = ((a ∩ b) ≡ (a ∪ b))
2		bicom 96	. . . . 5 ((a ∩ b) ≡ (a ∪ b)) = ((a ∪ b) ≡ (a ∩ b))
3	1, 2	ax-r2 36	. . . 4 (a ≡ b) = ((a ∪ b) ≡ (a ∩ b))
4	3	bile 142	. . 3 (a ≡ b) ≤ ((a ∪ b) ≡ (a ∩ b))
5		orbile 843	. . . 4 ((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b) →2 c) ∩ (c →1 (a ∪ b)))
6		imp3 841	. . . 4 (((a ∩ b) →2 c) ∩ (c →1 (a ∪ b))) = (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b)))
7	5, 6	lbtr 139	. . 3 ((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b)))
8	4, 7	le2an 169	. 2 ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b))))
9		mlaconj4.2	. . . . . 6 d = (a ∪ b)
10		mlaconj4.3	. . . . . 6 e = (a ∩ b)
11	9, 10	2bi 99	. . . . 5 (d ≡ e) = ((a ∪ b) ≡ (a ∩ b))
12	10	ax-r4 37	. . . . . . 7 e⊥ = (a ∩ b)⊥
13	12	ran 78	. . . . . 6 (e⊥ ∩ c⊥ ) = ((a ∩ b)⊥ ∩ c⊥ )
14		ancom 74	. . . . . . 7 (d ∩ c) = (c ∩ d)
15	9	lan 77	. . . . . . 7 (c ∩ d) = (c ∩ (a ∪ b))
16	14, 15	ax-r2 36	. . . . . 6 (d ∩ c) = (c ∩ (a ∪ b))
17	13, 16	2or 72	. . . . 5 ((e⊥ ∩ c⊥ ) ∪ (d ∩ c)) = (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b)))
18	11, 17	2an 79	. . . 4 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) = (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b))))
19	18	ax-r1 35	. . 3 (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b)))) = ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c)))
20		lea 160	. . . . . 6 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (d ≡ e)
21		bicom 96	. . . . . . 7 ((a ∪ b) ≡ (a ∩ b)) = ((a ∩ b) ≡ (a ∪ b))
22	21, 11, 1	3tr1 63	. . . . . 6 (d ≡ e) = (a ≡ b)
23	20, 22	lbtr 139	. . . . 5 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (a ≡ b)
24		mlaconj4.1	. . . . . 6 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (d ≡ c)
25	9	rbi 98	. . . . . 6 (d ≡ c) = ((a ∪ b) ≡ c)
26	24, 25	lbtr 139	. . . . 5 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ ((a ∪ b) ≡ c)
27	23, 26	ler2an 173	. . . 4 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ ((a ≡ b) ∩ ((a ∪ b) ≡ c))
28		anass 76	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
29		coman1 185	. . . . . . . . . . . 12 (a⊥ ∩ (b⊥ ∩ c⊥ )) C a⊥
30	29	comcom7 460	. . . . . . . . . . 11 (a⊥ ∩ (b⊥ ∩ c⊥ )) C a
31	28, 30	bctr 181	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C a
32		an32 83	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ c⊥ ) ∩ b⊥ )
33		coman2 186	. . . . . . . . . . . 12 ((a⊥ ∩ c⊥ ) ∩ b⊥ ) C b⊥
34	33	comcom7 460	. . . . . . . . . . 11 ((a⊥ ∩ c⊥ ) ∩ b⊥ ) C b
35	32, 34	bctr 181	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C b
36	31, 35	com2an 484	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C (a ∩ b)
37		coman1 185	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C (a⊥ ∩ b⊥ )
38	36, 37	com2or 483	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
39	31, 35	com2or 483	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C (a ∪ b)
40		coman2 186	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C c⊥
41	40	comcom7 460	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C c
42	39, 41	com2an 484	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C ((a ∪ b) ∩ c)
43	38, 42	fh2c 477	. . . . . . 7 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ (((a ∪ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))) = ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a ∪ b) ∩ c)) ∪ (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )))
44		anor3 90	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
45		comanr1 464	. . . . . . . . . . . 12 (a ∪ b) C ((a ∪ b) ∩ c)
46	45	comcom3 454	. . . . . . . . . . 11 (a ∪ b)⊥ C ((a ∪ b) ∩ c)
47	44, 46	bctr 181	. . . . . . . . . 10 (a⊥ ∩ b⊥ ) C ((a ∪ b) ∩ c)
48		coman1 185	. . . . . . . . . . . 12 (a⊥ ∩ b⊥ ) C a⊥
49	48	comcom7 460	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) C a
50		coman2 186	. . . . . . . . . . . 12 (a⊥ ∩ b⊥ ) C b⊥
51	50	comcom7 460	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) C b
52	49, 51	com2an 484	. . . . . . . . . 10 (a⊥ ∩ b⊥ ) C (a ∩ b)
53	47, 52	fh2rc 480	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a ∪ b) ∩ c)) = (((a ∩ b) ∩ ((a ∪ b) ∩ c)) ∪ ((a⊥ ∩ b⊥ ) ∩ ((a ∪ b) ∩ c)))
54		anass 76	. . . . . . . . . . . 12 (((a ∩ b) ∩ (a ∪ b)) ∩ c) = ((a ∩ b) ∩ ((a ∪ b) ∩ c))
55	54	ax-r1 35	. . . . . . . . . . 11 ((a ∩ b) ∩ ((a ∪ b) ∩ c)) = (((a ∩ b) ∩ (a ∪ b)) ∩ c)
56		leao1 162	. . . . . . . . . . . . 13 (a ∩ b) ≤ (a ∪ b)
57	56	df2le2 136	. . . . . . . . . . . 12 ((a ∩ b) ∩ (a ∪ b)) = (a ∩ b)
58	57	ran 78	. . . . . . . . . . 11 (((a ∩ b) ∩ (a ∪ b)) ∩ c) = ((a ∩ b) ∩ c)
59	55, 58	ax-r2 36	. . . . . . . . . 10 ((a ∩ b) ∩ ((a ∪ b) ∩ c)) = ((a ∩ b) ∩ c)
60		dff 101	. . . . . . . . . . . . . 14 0 = ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )⊥ )
61		oran 87	. . . . . . . . . . . . . . . 16 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
62	61	lan 77	. . . . . . . . . . . . . . 15 ((a⊥ ∩ b⊥ ) ∩ (a ∪ b)) = ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )⊥ )
63	62	ax-r1 35	. . . . . . . . . . . . . 14 ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )⊥ ) = ((a⊥ ∩ b⊥ ) ∩ (a ∪ b))
64	60, 63	ax-r2 36	. . . . . . . . . . . . 13 0 = ((a⊥ ∩ b⊥ ) ∩ (a ∪ b))
65	64	ran 78	. . . . . . . . . . . 12 (0 ∩ c) = (((a⊥ ∩ b⊥ ) ∩ (a ∪ b)) ∩ c)
66	65	ax-r1 35	. . . . . . . . . . 11 (((a⊥ ∩ b⊥ ) ∩ (a ∪ b)) ∩ c) = (0 ∩ c)
67		anass 76	. . . . . . . . . . 11 (((a⊥ ∩ b⊥ ) ∩ (a ∪ b)) ∩ c) = ((a⊥ ∩ b⊥ ) ∩ ((a ∪ b) ∩ c))
68		an0r 109	. . . . . . . . . . 11 (0 ∩ c) = 0
69	66, 67, 68	3tr2 64	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ ((a ∪ b) ∩ c)) = 0
70	59, 69	2or 72	. . . . . . . . 9 (((a ∩ b) ∩ ((a ∪ b) ∩ c)) ∪ ((a⊥ ∩ b⊥ ) ∩ ((a ∪ b) ∩ c))) = (((a ∩ b) ∩ c) ∪ 0)
71		or0 102	. . . . . . . . 9 (((a ∩ b) ∩ c) ∪ 0) = ((a ∩ b) ∩ c)
72	53, 70, 71	3tr 65	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a ∪ b) ∩ c)) = ((a ∩ b) ∩ c)
73		comanr1 464	. . . . . . . . . 10 (a⊥ ∩ b⊥ ) C ((a⊥ ∩ b⊥ ) ∩ c⊥ )
74	73, 52	fh2rc 480	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = (((a ∩ b) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )))
75		an4 86	. . . . . . . . . . 11 ((a ∩ b) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = ((a ∩ (a⊥ ∩ b⊥ )) ∩ (b ∩ c⊥ ))
76		dff 101	. . . . . . . . . . . . . . 15 0 = (a ∩ a⊥ )
77	76	ran 78	. . . . . . . . . . . . . 14 (0 ∩ b⊥ ) = ((a ∩ a⊥ ) ∩ b⊥ )
78		an0r 109	. . . . . . . . . . . . . 14 (0 ∩ b⊥ ) = 0
79		anass 76	. . . . . . . . . . . . . 14 ((a ∩ a⊥ ) ∩ b⊥ ) = (a ∩ (a⊥ ∩ b⊥ ))
80	77, 78, 79	3tr2 64	. . . . . . . . . . . . 13 0 = (a ∩ (a⊥ ∩ b⊥ ))
81	80	ran 78	. . . . . . . . . . . 12 (0 ∩ (b ∩ c⊥ )) = ((a ∩ (a⊥ ∩ b⊥ )) ∩ (b ∩ c⊥ ))
82	81	ax-r1 35	. . . . . . . . . . 11 ((a ∩ (a⊥ ∩ b⊥ )) ∩ (b ∩ c⊥ )) = (0 ∩ (b ∩ c⊥ ))
83		an0r 109	. . . . . . . . . . 11 (0 ∩ (b ∩ c⊥ )) = 0
84	75, 82, 83	3tr 65	. . . . . . . . . 10 ((a ∩ b) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = 0
85		anass 76	. . . . . . . . . . . 12 (((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )) ∩ c⊥ ) = ((a⊥ ∩ b⊥ ) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
86	85	ax-r1 35	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = (((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )) ∩ c⊥ )
87		anidm 111	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
88	87	ran 78	. . . . . . . . . . 11 (((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )) ∩ c⊥ ) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
89	86, 88	ax-r2 36	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
90	84, 89	2or 72	. . . . . . . . 9 (((a ∩ b) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))) = (0 ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
91		or0r 103	. . . . . . . . 9 (0 ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
92	74, 90, 91	3tr 65	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
93	72, 92	2or 72	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a ∪ b) ∩ c)) ∪ (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))) = (((a ∩ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
94	43, 93	ax-r2 36	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ (((a ∪ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))) = (((a ∩ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
95		dfb 94	. . . . . . 7 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
96		dfb 94	. . . . . . . 8 ((a ∪ b) ≡ c) = (((a ∪ b) ∩ c) ∪ ((a ∪ b)⊥ ∩ c⊥ ))
97	44	ran 78	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a ∪ b)⊥ ∩ c⊥ )
98	97	lor 70	. . . . . . . . 9 (((a ∪ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ )) = (((a ∪ b) ∩ c) ∪ ((a ∪ b)⊥ ∩ c⊥ ))
99	98	ax-r1 35	. . . . . . . 8 (((a ∪ b) ∩ c) ∪ ((a ∪ b)⊥ ∩ c⊥ )) = (((a ∪ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
100	96, 99	ax-r2 36	. . . . . . 7 ((a ∪ b) ≡ c) = (((a ∪ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
101	95, 100	2an 79	. . . . . 6 ((a ≡ b) ∩ ((a ∪ b) ≡ c)) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∩ (((a ∪ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ )))
102		bi3 839	. . . . . 6 ((a ≡ b) ∩ (b ≡ c)) = (((a ∩ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
103	94, 101, 102	3tr1 63	. . . . 5 ((a ≡ b) ∩ ((a ∪ b) ≡ c)) = ((a ≡ b) ∩ (b ≡ c))
104		mlaoml 833	. . . . 5 ((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)
105	103, 104	bltr 138	. . . 4 ((a ≡ b) ∩ ((a ∪ b) ≡ c)) ≤ (a ≡ c)
106	27, 105	letr 137	. . 3 ((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (a ≡ c)
107	19, 106	bltr 138	. 2 (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)⊥ ∩ c⊥ ) ∪ (c ∩ (a ∪ b)))) ≤ (a ≡ c)
108	8, 107	letr 137	1 ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  0wf 9   →₁ wi1 12   →₂ wi2 13

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)