Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa6todual 932

Description: Conventional to dual 6-variable OA law.

**Hypothesis**
Ref	Expression
oa6todual.1	(((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ )) ∩ (e^⊥ ∪ f^⊥ )) ≤ (b^⊥ ∪ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))))

**Assertion**
Ref	Expression
oa6todual	(b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))

**Proof of Theorem oa6todual**
Step	Hyp	Ref	Expression
1		oa6todual.1	. . 3 (((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ )) ∩ (e^⊥ ∪ f^⊥ )) ≤ (b^⊥ ∪ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))))
2	1	lecon 146	. 2 (b^⊥ ∪ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))))^⊥ ≤ (((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ )) ∩ (e^⊥ ∪ f^⊥ ))^⊥
3		ax-a1 29	. . . 4 b = b^⊥ ^⊥
4		ax-a1 29	. . . . . 6 a = a^⊥ ^⊥
5		ax-a1 29	. . . . . . . 8 c = c^⊥ ^⊥
6		df-a 39	. . . . . . . . . . . 12 (a ∩ c) = (a^⊥ ∪ c^⊥ )^⊥
7		df-a 39	. . . . . . . . . . . 12 (b ∩ d) = (b^⊥ ∪ d^⊥ )^⊥
8	6, 7	2or 67	. . . . . . . . . . 11 ((a ∩ c) ∪ (b ∩ d)) = ((a^⊥ ∪ c^⊥ )^⊥ ∪ (b^⊥ ∪ d^⊥ )^⊥ )
9		oran3 85	. . . . . . . . . . 11 ((a^⊥ ∪ c^⊥ )^⊥ ∪ (b^⊥ ∪ d^⊥ )^⊥ ) = ((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ ))^⊥
10	8, 9	ax-r2 35	. . . . . . . . . 10 ((a ∩ c) ∪ (b ∩ d)) = ((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ ))^⊥
11		df-a 39	. . . . . . . . . . . . . 14 (a ∩ e) = (a^⊥ ∪ e^⊥ )^⊥
12		df-a 39	. . . . . . . . . . . . . 14 (b ∩ f) = (b^⊥ ∪ f^⊥ )^⊥
13	11, 12	2or 67	. . . . . . . . . . . . 13 ((a ∩ e) ∪ (b ∩ f)) = ((a^⊥ ∪ e^⊥ )^⊥ ∪ (b^⊥ ∪ f^⊥ )^⊥ )
14		oran3 85	. . . . . . . . . . . . 13 ((a^⊥ ∪ e^⊥ )^⊥ ∪ (b^⊥ ∪ f^⊥ )^⊥ ) = ((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ ))^⊥
15	13, 14	ax-r2 35	. . . . . . . . . . . 12 ((a ∩ e) ∪ (b ∩ f)) = ((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ ))^⊥
16		df-a 39	. . . . . . . . . . . . . 14 (c ∩ e) = (c^⊥ ∪ e^⊥ )^⊥
17		df-a 39	. . . . . . . . . . . . . 14 (d ∩ f) = (d^⊥ ∪ f^⊥ )^⊥
18	16, 17	2or 67	. . . . . . . . . . . . 13 ((c ∩ e) ∪ (d ∩ f)) = ((c^⊥ ∪ e^⊥ )^⊥ ∪ (d^⊥ ∪ f^⊥ )^⊥ )
19		oran3 85	. . . . . . . . . . . . 13 ((c^⊥ ∪ e^⊥ )^⊥ ∪ (d^⊥ ∪ f^⊥ )^⊥ ) = ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))^⊥
20	18, 19	ax-r2 35	. . . . . . . . . . . 12 ((c ∩ e) ∪ (d ∩ f)) = ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))^⊥
21	15, 20	2an 72	. . . . . . . . . . 11 (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))) = (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ ))^⊥ ∩ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))^⊥ )
22		anor3 82	. . . . . . . . . . 11 (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ ))^⊥ ∩ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))^⊥ ) = (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))^⊥
23	21, 22	ax-r2 35	. . . . . . . . . 10 (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))) = (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))^⊥
24	10, 23	2or 67	. . . . . . . . 9 (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))) = (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ ))^⊥ ∪ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))^⊥ )
25		oran3 85	. . . . . . . . 9 (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ ))^⊥ ∪ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))^⊥ ) = (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))^⊥
26	24, 25	ax-r2 35	. . . . . . . 8 (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))) = (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))^⊥
27	5, 26	2an 72	. . . . . . 7 (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))) = (c^⊥ ^⊥ ∩ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))^⊥ )
28		anor3 82	. . . . . . 7 (c^⊥ ^⊥ ∩ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))^⊥ ) = (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))^⊥
29	27, 28	ax-r2 35	. . . . . 6 (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))) = (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))^⊥
30	4, 29	2or 67	. . . . 5 (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))))) = (a^⊥ ^⊥ ∪ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))^⊥ )
31		oran3 85	. . . . 5 (a^⊥ ^⊥ ∪ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))^⊥ ) = (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))))^⊥
32	30, 31	ax-r2 35	. . . 4 (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))))) = (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))))^⊥
33	3, 32	2an 72	. . 3 (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) = (b^⊥ ^⊥ ∩ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))))^⊥ )
34		anor3 82	. . 3 (b^⊥ ^⊥ ∩ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ ))))))^⊥ ) = (b^⊥ ∪ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))))^⊥
35	33, 34	ax-r2 35	. 2 (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) = (b^⊥ ∪ (a^⊥ ∩ (c^⊥ ∪ (((a^⊥ ∪ c^⊥ ) ∩ (b^⊥ ∪ d^⊥ )) ∩ (((a^⊥ ∪ e^⊥ ) ∩ (b^⊥ ∪ f^⊥ )) ∪ ((c^⊥ ∪ e^⊥ ) ∩ (d^⊥ ∪ f^⊥ )))))))^⊥
36		df-a 39	. . . . . 6 (a ∩ b) = (a^⊥ ∪ b^⊥ )^⊥
37		df-a 39	. . . . . 6 (c ∩ d) = (c^⊥ ∪ d^⊥ )^⊥
38	36, 37	2or 67	. . . . 5 ((a ∩ b) ∪ (c ∩ d)) = ((a^⊥ ∪ b^⊥ )^⊥ ∪ (c^⊥ ∪ d^⊥ )^⊥ )
39		oran3 85	. . . . 5 ((a^⊥ ∪ b^⊥ )^⊥ ∪ (c^⊥ ∪ d^⊥ )^⊥ ) = ((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ ))^⊥
40	38, 39	ax-r2 35	. . . 4 ((a ∩ b) ∪ (c ∩ d)) = ((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ ))^⊥
41		df-a 39	. . . 4 (e ∩ f) = (e^⊥ ∪ f^⊥ )^⊥
42	40, 41	2or 67	. . 3 (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f)) = (((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ ))^⊥ ∪ (e^⊥ ∪ f^⊥ )^⊥ )
43		oran3 85	. . 3 (((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ ))^⊥ ∪ (e^⊥ ∪ f^⊥ )^⊥ ) = (((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ )) ∩ (e^⊥ ∪ f^⊥ ))^⊥
44	42, 43	ax-r2 35	. 2 (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f)) = (((a^⊥ ∪ b^⊥ ) ∩ (c^⊥ ∪ d^⊥ )) ∩ (e^⊥ ∪ f^⊥ ))^⊥
45	2, 35, 44	le3tr1 132	1 (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))

Colors of variables: term

Syntax hints: ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7

This theorem is referenced by: oa6to4 938

This theorem was proved from axioms: ax-a1 29 ax-a2 30 ax-a5 33 ax-r1 34 ax-r2 35 ax-r4 36 ax-r5 37

This theorem depends on definitions: df-a 39 df-le1 122 df-le2 123

metamath.org