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

 Description: OA Distributive law. This is equivalent to the 6-variable OA law, as shown by theorem d6oa 997.
Hypotheses
Ref Expression
4oa.1 e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))
4oa.2 f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)
4oadist.4 (h ∩ (b1 d)) ≤ k
Assertion
Ref Expression
4oadist (h ∩ (jk)) = ((hj) ∪ (hk))

StepHypRef Expression
1 4oadist.2 . . . . . . . . . 10 jf
2 4oadist.3 . . . . . . . . . 10 kf
31, 2le2or 168 . . . . . . . . 9 (jk) ≤ (ff)
4 oridm 110 . . . . . . . . 9 (ff) = f
53, 4lbtr 139 . . . . . . . 8 (jk) ≤ f
65lelan 167 . . . . . . 7 (h ∩ (jk)) ≤ (hf)
76df2le2 136 . . . . . 6 ((h ∩ (jk)) ∩ (hf)) = (h ∩ (jk))
87ax-r1 35 . . . . 5 (h ∩ (jk)) = ((h ∩ (jk)) ∩ (hf))
9 4oa.2 . . . . . . . . 9 f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)
10 or32 82 . . . . . . . . 9 (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e) = (((ab) ∪ e) ∪ ((a1 d) ∩ (b1 d)))
119, 10ax-r2 36 . . . . . . . 8 f = (((ab) ∪ e) ∪ ((a1 d) ∩ (b1 d)))
1211lan 77 . . . . . . 7 (hf) = (h ∩ (((ab) ∪ e) ∪ ((a1 d) ∩ (b1 d))))
13 4oa.1 . . . . . . . 8 e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))
14 leo 158 . . . . . . . . 9 ((ab) ∪ e) ≤ (((ab) ∪ e) ∪ ((a1 d) ∩ (b1 d)))
1511ax-r1 35 . . . . . . . . 9 (((ab) ∪ e) ∪ ((a1 d) ∩ (b1 d))) = f
1614, 15lbtr 139 . . . . . . . 8 ((ab) ∪ e) ≤ f
17 4oadist.1 . . . . . . . 8 h ≤ (a1 d)
1813, 9, 16, 174oagen1b 1043 . . . . . . 7 (h ∩ (((ab) ∪ e) ∪ ((a1 d) ∩ (b1 d)))) = (h ∩ (b1 d))
1912, 18ax-r2 36 . . . . . 6 (hf) = (h ∩ (b1 d))
2019lan 77 . . . . 5 ((h ∩ (jk)) ∩ (hf)) = ((h ∩ (jk)) ∩ (h ∩ (b1 d)))
218, 20ax-r2 36 . . . 4 (h ∩ (jk)) = ((h ∩ (jk)) ∩ (h ∩ (b1 d)))
22 lear 161 . . . . 5 ((h ∩ (jk)) ∩ (h ∩ (b1 d))) ≤ (h ∩ (b1 d))
23 4oadist.4 . . . . . . . . 9 (h ∩ (b1 d)) ≤ k
2423df2le2 136 . . . . . . . 8 ((h ∩ (b1 d)) ∩ k) = (h ∩ (b1 d))
2524ax-r1 35 . . . . . . 7 (h ∩ (b1 d)) = ((h ∩ (b1 d)) ∩ k)
26 an32 83 . . . . . . 7 ((h ∩ (b1 d)) ∩ k) = ((hk) ∩ (b1 d))
2725, 26ax-r2 36 . . . . . 6 (h ∩ (b1 d)) = ((hk) ∩ (b1 d))
28 lea 160 . . . . . 6 ((hk) ∩ (b1 d)) ≤ (hk)
2927, 28bltr 138 . . . . 5 (h ∩ (b1 d)) ≤ (hk)
3022, 29letr 137 . . . 4 ((h ∩ (jk)) ∩ (h ∩ (b1 d))) ≤ (hk)
3121, 30bltr 138 . . 3 (h ∩ (jk)) ≤ (hk)
32 leor 159 . . 3 (hk) ≤ ((hj) ∪ (hk))
3331, 32letr 137 . 2 (h ∩ (jk)) ≤ ((hj) ∪ (hk))
34 ledi 174 . 2 ((hj) ∪ (hk)) ≤ (h ∩ (jk))
3533, 34lebi 145 1 (h ∩ (jk)) = ((hj) ∪ (hk))
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7   →1 wi1 12 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-4oa 1033 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator