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

Theorem oa4uto4 977
Description: Derivation of standard 4-variable proper OA law from "universal" variant oa4to4u2 974. (Contributed by NM, 30-Dec-1998.)
Hypothesis
Ref Expression
oa4uto4.1 ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d
Assertion
Ref Expression
oa4uto4 ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Proof of Theorem oa4uto4
StepHypRef Expression
1 u1lem9a 777 . . . . 5 (a1 d)a
21lecon1 155 . . . 4 a ≤ (a1 d)
3 u1lem9a 777 . . . . . 6 (b1 d)b
43lecon1 155 . . . . 5 b ≤ (b1 d)
5 ax-a2 31 . . . . . . 7 ((ab) ∪ ((a1 d) ∩ (b1 d))) = (((a1 d) ∩ (b1 d)) ∪ (ab))
62, 4le2an 169 . . . . . . . 8 (ab) ≤ ((a1 d) ∩ (b1 d))
76lelor 166 . . . . . . 7 (((a1 d) ∩ (b1 d)) ∪ (ab)) ≤ (((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d)))
85, 7bltr 138 . . . . . 6 ((ab) ∪ ((a1 d) ∩ (b1 d))) ≤ (((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d)))
9 ax-a2 31 . . . . . . . 8 ((ac) ∪ ((a1 d) ∩ (c1 d))) = (((a1 d) ∩ (c1 d)) ∪ (ac))
10 u1lem9a 777 . . . . . . . . . . 11 (c1 d)c
1110lecon1 155 . . . . . . . . . 10 c ≤ (c1 d)
122, 11le2an 169 . . . . . . . . 9 (ac) ≤ ((a1 d) ∩ (c1 d))
1312lelor 166 . . . . . . . 8 (((a1 d) ∩ (c1 d)) ∪ (ac)) ≤ (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))
149, 13bltr 138 . . . . . . 7 ((ac) ∪ ((a1 d) ∩ (c1 d))) ≤ (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))
15 ax-a2 31 . . . . . . . 8 ((bc) ∪ ((b1 d) ∩ (c1 d))) = (((b1 d) ∩ (c1 d)) ∪ (bc))
164, 11le2an 169 . . . . . . . . 9 (bc) ≤ ((b1 d) ∩ (c1 d))
1716lelor 166 . . . . . . . 8 (((b1 d) ∩ (c1 d)) ∪ (bc)) ≤ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))
1815, 17bltr 138 . . . . . . 7 ((bc) ∪ ((b1 d) ∩ (c1 d))) ≤ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))
1914, 18le2an 169 . . . . . 6 (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))) ≤ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))
208, 19le2or 168 . . . . 5 (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))) ≤ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))
214, 20le2an 169 . . . 4 (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))
222, 21le2or 168 . . 3 (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))))) ≤ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))
2322lelan 167 . 2 ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))))
24 oa4uto4.1 . 2 ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d
2523, 24letr 137 1 ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d
Colors of variables: term
Syntax hints:  wle 2   wn 4  wo 6  wa 7  1 wi1 12
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131
This theorem is referenced by:  d6oa  997  axoa4  1034
  Copyright terms: Public domain W3C validator