Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem mlaconj4 826

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

**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 781	. . . . 5 (a ≡ b) = ((a ∩ b) ≡ (a ∪ b))
2		bicom 88	. . . . 5 ((a ∩ b) ≡ (a ∪ b)) = ((a ∪ b) ≡ (a ∩ b))
3	1, 2	ax-r2 35	. . . 4 (a ≡ b) = ((a ∪ b) ≡ (a ∩ b))
4	3	bile 134	. . 3 (a ≡ b) ≤ ((a ∪ b) ≡ (a ∩ b))
5		orbile 825	. . . 4 ((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b) →₂c) ∩ (c →₁(a ∪ b)))
6		imp3 823	. . . 4 (((a ∩ b) →₂c) ∩ (c →₁(a ∪ b))) = (((a ∩ b)^⊥ ∩ c^⊥ ) ∪ (c ∩ (a ∪ b)))
7	5, 6	lbtr 131	. . 3 ((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b)^⊥ ∩ c^⊥ ) ∪ (c ∩ (a ∪ b)))
8	4, 7	le2an 161	. 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 91	. . . . 5 (d ≡ e) = ((a ∪ b) ≡ (a ∩ b))
12	10	ax-r4 36	. . . . . . 7 e^⊥ = (a ∩ b)^⊥
13	12	ran 71	. . . . . 6 (e^⊥ ∩ c^⊥ ) = ((a ∩ b)^⊥ ∩ c^⊥ )
14		ancom 68	. . . . . . 7 (d ∩ c) = (c ∩ d)
15	9	lan 70	. . . . . . 7 (c ∩ d) = (c ∩ (a ∪ b))
16	14, 15	ax-r2 35	. . . . . 6 (d ∩ c) = (c ∩ (a ∪ b))
17	13, 16	2or 67	. . . . 5 ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c)) = (((a ∩ b)^⊥ ∩ c^⊥ ) ∪ (c ∩ (a ∪ b)))
18	11, 17	2an 72	. . . 4 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) = (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)^⊥ ∩ c^⊥ ) ∪ (c ∩ (a ∪ b))))
19	18	ax-r1 34	. . 3 (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)^⊥ ∩ c^⊥ ) ∪ (c ∩ (a ∪ b)))) = ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c)))
20		lea 152	. . . . . 6 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) ≤ (d ≡ e)
21		bicom 88	. . . . . . 7 ((a ∪ b) ≡ (a ∩ b)) = ((a ∩ b) ≡ (a ∪ b))
22	21, 11, 1	3tr1 60	. . . . . 6 (d ≡ e) = (a ≡ b)
23	20, 22	lbtr 131	. . . . 5 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) ≤ (a ≡ b)
24		mlaconj4.1	. . . . . 6 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) ≤ (d ≡ c)
25	9	rbi 90	. . . . . 6 (d ≡ c) = ((a ∪ b) ≡ c)
26	24, 25	lbtr 131	. . . . 5 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) ≤ ((a ∪ b) ≡ c)
27	23, 26	ler2an 165	. . . 4 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) ≤ ((a ≡ b) ∩ ((a ∪ b) ≡ c))
28		anass 69	. . . . . . . . . . 11 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = (a^⊥ ∩ (b^⊥ ∩ c^⊥ ))
29		coman1 177	. . . . . . . . . . . 12 (a^⊥ ∩ (b^⊥ ∩ c^⊥ )) C a^⊥
30	29	comcom7 442	. . . . . . . . . . 11 (a^⊥ ∩ (b^⊥ ∩ c^⊥ )) C a
31	28, 30	bctr 173	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C a
32		an32 76	. . . . . . . . . . 11 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = ((a^⊥ ∩ c^⊥ ) ∩ b^⊥ )
33		coman2 178	. . . . . . . . . . . 12 ((a^⊥ ∩ c^⊥ ) ∩ b^⊥ ) C b^⊥
34	33	comcom7 442	. . . . . . . . . . 11 ((a^⊥ ∩ c^⊥ ) ∩ b^⊥ ) C b
35	32, 34	bctr 173	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C b
36	31, 35	com2an 466	. . . . . . . . 9 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C (a ∩ b)
37		coman1 177	. . . . . . . . 9 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C (a^⊥ ∩ b^⊥ )
38	36, 37	com2or 465	. . . . . . . 8 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C ((a ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
39	31, 35	com2or 465	. . . . . . . . 9 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C (a ∪ b)
40		coman2 178	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C c^⊥
41	40	comcom7 442	. . . . . . . . 9 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C c
42	39, 41	com2an 466	. . . . . . . 8 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C ((a ∪ b) ∩ c)
43	38, 42	fh2c 459	. . . . . . 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 82	. . . . . . . . . . 11 (a^⊥ ∩ b^⊥ ) = (a ∪ b)^⊥
45		comanr1 446	. . . . . . . . . . . 12 (a ∪ b) C ((a ∪ b) ∩ c)
46	45	comcom3 436	. . . . . . . . . . 11 (a ∪ b)^⊥ C ((a ∪ b) ∩ c)
47	44, 46	bctr 173	. . . . . . . . . 10 (a^⊥ ∩ b^⊥ ) C ((a ∪ b) ∩ c)
48		coman1 177	. . . . . . . . . . . 12 (a^⊥ ∩ b^⊥ ) C a^⊥
49	48	comcom7 442	. . . . . . . . . . 11 (a^⊥ ∩ b^⊥ ) C a
50		coman2 178	. . . . . . . . . . . 12 (a^⊥ ∩ b^⊥ ) C b^⊥
51	50	comcom7 442	. . . . . . . . . . 11 (a^⊥ ∩ b^⊥ ) C b
52	49, 51	com2an 466	. . . . . . . . . 10 (a^⊥ ∩ b^⊥ ) C (a ∩ b)
53	47, 52	fh2rc 462	. . . . . . . . 9 (((a ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ ((a ∪ b) ∩ c)) = (((a ∩ b) ∩ ((a ∪ b) ∩ c)) ∪ ((a^⊥ ∩ b^⊥ ) ∩ ((a ∪ b) ∩ c)))
54		anass 69	. . . . . . . . . . . 12 (((a ∩ b) ∩ (a ∪ b)) ∩ c) = ((a ∩ b) ∩ ((a ∪ b) ∩ c))
55	54	ax-r1 34	. . . . . . . . . . 11 ((a ∩ b) ∩ ((a ∪ b) ∩ c)) = (((a ∩ b) ∩ (a ∪ b)) ∩ c)
56		leao1 154	. . . . . . . . . . . . 13 (a ∩ b) ≤ (a ∪ b)
57	56	df2le2 128	. . . . . . . . . . . 12 ((a ∩ b) ∩ (a ∪ b)) = (a ∩ b)
58	57	ran 71	. . . . . . . . . . 11 (((a ∩ b) ∩ (a ∪ b)) ∩ c) = ((a ∩ b) ∩ c)
59	55, 58	ax-r2 35	. . . . . . . . . 10 ((a ∩ b) ∩ ((a ∪ b) ∩ c)) = ((a ∩ b) ∩ c)
60		dff 93	. . . . . . . . . . . . . 14 0 = ((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )^⊥ )
61		oran 79	. . . . . . . . . . . . . . . 16 (a ∪ b) = (a^⊥ ∩ b^⊥ )^⊥
62	61	lan 70	. . . . . . . . . . . . . . 15 ((a^⊥ ∩ b^⊥ ) ∩ (a ∪ b)) = ((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )^⊥ )
63	62	ax-r1 34	. . . . . . . . . . . . . 14 ((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∩ (a ∪ b))
64	60, 63	ax-r2 35	. . . . . . . . . . . . 13 0 = ((a^⊥ ∩ b^⊥ ) ∩ (a ∪ b))
65	64	ran 71	. . . . . . . . . . . 12 (0 ∩ c) = (((a^⊥ ∩ b^⊥ ) ∩ (a ∪ b)) ∩ c)
66	65	ax-r1 34	. . . . . . . . . . 11 (((a^⊥ ∩ b^⊥ ) ∩ (a ∪ b)) ∩ c) = (0 ∩ c)
67		anass 69	. . . . . . . . . . 11 (((a^⊥ ∩ b^⊥ ) ∩ (a ∪ b)) ∩ c) = ((a^⊥ ∩ b^⊥ ) ∩ ((a ∪ b) ∩ c))
68		an0r 101	. . . . . . . . . . 11 (0 ∩ c) = 0
69	66, 67, 68	3tr2 61	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ ((a ∪ b) ∩ c)) = 0
70	59, 69	2or 67	. . . . . . . . 9 (((a ∩ b) ∩ ((a ∪ b) ∩ c)) ∪ ((a^⊥ ∩ b^⊥ ) ∩ ((a ∪ b) ∩ c))) = (((a ∩ b) ∩ c) ∪ 0)
71		or0 94	. . . . . . . . 9 (((a ∩ b) ∩ c) ∪ 0) = ((a ∩ b) ∩ c)
72	53, 70, 71	3tr 62	. . . . . . . 8 (((a ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ ((a ∪ b) ∩ c)) = ((a ∩ b) ∩ c)
73		comanr1 446	. . . . . . . . . 10 (a^⊥ ∩ b^⊥ ) C ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
74	73, 52	fh2rc 462	. . . . . . . . 9 (((a ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = (((a ∩ b) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∪ ((a^⊥ ∩ b^⊥ ) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )))
75		an4 78	. . . . . . . . . . 11 ((a ∩ b) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = ((a ∩ (a^⊥ ∩ b^⊥ )) ∩ (b ∩ c^⊥ ))
76		dff 93	. . . . . . . . . . . . . . 15 0 = (a ∩ a^⊥ )
77	76	ran 71	. . . . . . . . . . . . . 14 (0 ∩ b^⊥ ) = ((a ∩ a^⊥ ) ∩ b^⊥ )
78		an0r 101	. . . . . . . . . . . . . 14 (0 ∩ b^⊥ ) = 0
79		anass 69	. . . . . . . . . . . . . 14 ((a ∩ a^⊥ ) ∩ b^⊥ ) = (a ∩ (a^⊥ ∩ b^⊥ ))
80	77, 78, 79	3tr2 61	. . . . . . . . . . . . 13 0 = (a ∩ (a^⊥ ∩ b^⊥ ))
81	80	ran 71	. . . . . . . . . . . 12 (0 ∩ (b ∩ c^⊥ )) = ((a ∩ (a^⊥ ∩ b^⊥ )) ∩ (b ∩ c^⊥ ))
82	81	ax-r1 34	. . . . . . . . . . 11 ((a ∩ (a^⊥ ∩ b^⊥ )) ∩ (b ∩ c^⊥ )) = (0 ∩ (b ∩ c^⊥ ))
83		an0r 101	. . . . . . . . . . 11 (0 ∩ (b ∩ c^⊥ )) = 0
84	75, 82, 83	3tr 62	. . . . . . . . . 10 ((a ∩ b) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = 0
85		anass 69	. . . . . . . . . . . 12 (((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )) ∩ c^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
86	85	ax-r1 34	. . . . . . . . . . 11 ((a^⊥ ∩ b^⊥ ) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = (((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )) ∩ c^⊥ )
87		anidm 103	. . . . . . . . . . . 12 ((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )) = (a^⊥ ∩ b^⊥ )
88	87	ran 71	. . . . . . . . . . 11 (((a^⊥ ∩ b^⊥ ) ∩ (a^⊥ ∩ b^⊥ )) ∩ c^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
89	86, 88	ax-r2 35	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
90	84, 89	2or 67	. . . . . . . . 9 (((a ∩ b) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∪ ((a^⊥ ∩ b^⊥ ) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))) = (0 ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
91		or0r 95	. . . . . . . . 9 (0 ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
92	74, 90, 91	3tr 62	. . . . . . . 8 (((a ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
93	72, 92	2or 67	. . . . . . 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 35	. . . . . 6 (((a ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ (((a ∪ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))) = (((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
95		dfb 86	. . . . . . 7 (a ≡ b) = ((a ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
96		dfb 86	. . . . . . . 8 ((a ∪ b) ≡ c) = (((a ∪ b) ∩ c) ∪ ((a ∪ b)^⊥ ∩ c^⊥ ))
97	44	ran 71	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = ((a ∪ b)^⊥ ∩ c^⊥ )
98	97	lor 66	. . . . . . . . 9 (((a ∪ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = (((a ∪ b) ∩ c) ∪ ((a ∪ b)^⊥ ∩ c^⊥ ))
99	98	ax-r1 34	. . . . . . . 8 (((a ∪ b) ∩ c) ∪ ((a ∪ b)^⊥ ∩ c^⊥ )) = (((a ∪ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
100	96, 99	ax-r2 35	. . . . . . 7 ((a ∪ b) ≡ c) = (((a ∪ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
101	95, 100	2an 72	. . . . . 6 ((a ≡ b) ∩ ((a ∪ b) ≡ c)) = (((a ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ (((a ∪ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )))
102		bi3 821	. . . . . 6 ((a ≡ b) ∩ (b ≡ c)) = (((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
103	94, 101, 102	3tr1 60	. . . . 5 ((a ≡ b) ∩ ((a ∪ b) ≡ c)) = ((a ≡ b) ∩ (b ≡ c))
104		mlaoml 815	. . . . 5 ((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)
105	103, 104	bltr 130	. . . 4 ((a ≡ b) ∩ ((a ∪ b) ≡ c)) ≤ (a ≡ c)
106	27, 105	letr 129	. . 3 ((d ≡ e) ∩ ((e^⊥ ∩ c^⊥ ) ∪ (d ∩ c))) ≤ (a ≡ c)
107	19, 106	bltr 130	. 2 (((a ∪ b) ≡ (a ∩ b)) ∩ (((a ∩ b)^⊥ ∩ c^⊥ ) ∪ (c ∩ (a ∪ b)))) ≤ (a ≡ c)
108	8, 107	letr 129	1 ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)

Colors of variables: term

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

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

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i1 43 df-i2 44 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org