Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3moa3 GIF version

Theorem oa3moa3 1029
 Description: 4-variable 3OA to 5-variable Mayet's 3OA. (Contributed by NM, 3-Apr-2009.) (Revised by NM, 31-Mar-2011.)
Hypotheses
Ref Expression
oa3moa3.1 ab
oa3moa3.2 cd
oa3moa3.3 de
oa3moa3.4 ec
Assertion
Ref Expression
oa3moa3 ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))

Proof of Theorem oa3moa3
StepHypRef Expression
1 oa3moa3.1 . . . . . 6 ab
21lecon3 157 . . . . 5 ba
3 oa3moa3.2 . . . . . . . 8 cd
43lecon3 157 . . . . . . 7 dc
5 oa3moa3.4 . . . . . . 7 ec
64, 5lel2or 170 . . . . . 6 (de) ≤ c
76lecon3 157 . . . . 5 c ≤ (de)
82, 7ax-oal4 1026 . . . 4 ((ba) ∩ (c ∪ (de))) ≤ (a ∪ (b ∩ (c ∪ ((bc) ∩ (a ∪ (de))))))
9 ax-a2 31 . . . . 5 (ab) = (ba)
10 ax-a3 32 . . . . 5 ((cd) ∪ e) = (c ∪ (de))
119, 102an 79 . . . 4 ((ab) ∩ ((cd) ∪ e)) = ((ba) ∩ (c ∪ (de)))
12 orass 75 . . . . . . . 8 ((ad) ∪ e) = (a ∪ (de))
1312lan 77 . . . . . . 7 ((bc) ∩ ((ad) ∪ e)) = ((bc) ∩ (a ∪ (de)))
1413lor 70 . . . . . 6 (c ∪ ((bc) ∩ ((ad) ∪ e))) = (c ∪ ((bc) ∩ (a ∪ (de))))
1514lan 77 . . . . 5 (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) = (b ∩ (c ∪ ((bc) ∩ (a ∪ (de)))))
1615lor 70 . . . 4 (a ∪ (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e))))) = (a ∪ (b ∩ (c ∪ ((bc) ∩ (a ∪ (de))))))
178, 11, 16le3tr1 140 . . 3 ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))))
18 oa3moa3.3 . . . . . . . . . 10 de
1918lecon3 157 . . . . . . . . 9 ed
203, 19lel2or 170 . . . . . . . 8 (ce) ≤ d
2120lecon3 157 . . . . . . 7 d ≤ (ce)
222, 21ax-oal4 1026 . . . . . 6 ((ba) ∩ (d ∪ (ce))) ≤ (a ∪ (b ∩ (d ∪ ((bd) ∩ (a ∪ (ce))))))
23 ax-a2 31 . . . . . . . . 9 (cd) = (dc)
2423ror 71 . . . . . . . 8 ((cd) ∪ e) = ((dc) ∪ e)
25 orass 75 . . . . . . . 8 ((dc) ∪ e) = (d ∪ (ce))
2624, 25tr 62 . . . . . . 7 ((cd) ∪ e) = (d ∪ (ce))
279, 262an 79 . . . . . 6 ((ab) ∩ ((cd) ∪ e)) = ((ba) ∩ (d ∪ (ce)))
28 orass 75 . . . . . . . . . 10 ((ac) ∪ e) = (a ∪ (ce))
2928lan 77 . . . . . . . . 9 ((bd) ∩ ((ac) ∪ e)) = ((bd) ∩ (a ∪ (ce)))
3029lor 70 . . . . . . . 8 (d ∪ ((bd) ∩ ((ac) ∪ e))) = (d ∪ ((bd) ∩ (a ∪ (ce))))
3130lan 77 . . . . . . 7 (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) = (b ∩ (d ∪ ((bd) ∩ (a ∪ (ce)))))
3231lor 70 . . . . . 6 (a ∪ (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e))))) = (a ∪ (b ∩ (d ∪ ((bd) ∩ (a ∪ (ce))))))
3322, 27, 32le3tr1 140 . . . . 5 ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))))
345lecon3 157 . . . . . . . . 9 ce
3534, 18lel2or 170 . . . . . . . 8 (cd) ≤ e
3635lecon3 157 . . . . . . 7 e ≤ (cd)
372, 36ax-oal4 1026 . . . . . 6 ((ba) ∩ (e ∪ (cd))) ≤ (a ∪ (b ∩ (e ∪ ((be) ∩ (a ∪ (cd))))))
38 ax-a2 31 . . . . . . 7 ((cd) ∪ e) = (e ∪ (cd))
399, 382an 79 . . . . . 6 ((ab) ∩ ((cd) ∪ e)) = ((ba) ∩ (e ∪ (cd)))
40 ax-a3 32 . . . . . . . . . 10 ((ac) ∪ d) = (a ∪ (cd))
4140lan 77 . . . . . . . . 9 ((be) ∩ ((ac) ∪ d)) = ((be) ∩ (a ∪ (cd)))
4241lor 70 . . . . . . . 8 (e ∪ ((be) ∩ ((ac) ∪ d))) = (e ∪ ((be) ∩ (a ∪ (cd))))
4342lan 77 . . . . . . 7 (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))) = (b ∩ (e ∪ ((be) ∩ (a ∪ (cd)))))
4443lor 70 . . . . . 6 (a ∪ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) = (a ∪ (b ∩ (e ∪ ((be) ∩ (a ∪ (cd))))))
4537, 39, 44le3tr1 140 . . . . 5 ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
4633, 45ler2an 173 . . . 4 ((ab) ∩ ((cd) ∪ e)) ≤ ((a ∪ (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
472lel 151 . . . . . . . . . 10 (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ≤ a
4847lecom 180 . . . . . . . . 9 (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) C a
4948comcom7 460 . . . . . . . 8 (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) C a
5049comcom 453 . . . . . . 7 a C (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e))))
512lel 151 . . . . . . . . . 10 (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))) ≤ a
5251lecom 180 . . . . . . . . 9 (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))) C a
5352comcom7 460 . . . . . . . 8 (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))) C a
5453comcom 453 . . . . . . 7 a C (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))
5550, 54fh3 471 . . . . . 6 (a ∪ ((b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = ((a ∪ (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
5655cm 61 . . . . 5 ((a ∪ (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = (a ∪ ((b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
57 anandi 114 . . . . . . 7 (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) = ((b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
5857cm 61 . . . . . 6 ((b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) = (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
5958lor 70 . . . . 5 (a ∪ ((b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
6056, 59tr 62 . . . 4 ((a ∪ (b ∩ (d ∪ ((bd) ∩ ((ac) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
6146, 60lbtr 139 . . 3 ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
6217, 61ler2an 173 . 2 ((ab) ∩ ((cd) ∪ e)) ≤ ((a ∪ (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))))
632lel 151 . . . . . . . 8 (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ≤ a
6463lecom 180 . . . . . . 7 (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) C a
6564comcom7 460 . . . . . 6 (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) C a
6665comcom 453 . . . . 5 a C (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e))))
672lel 151 . . . . . . . 8 (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) ≤ a
6867lecom 180 . . . . . . 7 (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) C a
6968comcom7 460 . . . . . 6 (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) C a
7069comcom 453 . . . . 5 a C (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
7166, 70fh3 471 . . . 4 (a ∪ ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))) = ((a ∪ (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))))
7271ax-r1 35 . . 3 ((a ∪ (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))) = (a ∪ ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))))
73 anass 76 . . . . . 6 ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))) = (b ∩ ((c ∪ ((bc) ∩ ((ad) ∪ e))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
7473cm 61 . . . . 5 (b ∩ ((c ∪ ((bc) ∩ ((ad) ∪ e))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
75 anandi 114 . . . . . 6 (b ∩ ((c ∪ ((bc) ∩ ((ad) ∪ e))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
7675ax-r1 35 . . . . 5 ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = (b ∩ ((c ∪ ((bc) ∩ ((ad) ∪ e))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))
77 anass 76 . . . . 5 (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))) = ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
7874, 76, 773tr1 63 . . . 4 ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))) = (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))
7978lor 70 . . 3 (a ∪ ((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))) = (a ∪ (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
8072, 79tr 62 . 2 ((a ∪ (b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((bd) ∩ ((ac) ∪ e))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d))))))) = (a ∪ (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
8162, 80lbtr 139 1 ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7 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  ax-oal4 1026 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator