QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  4oadist Unicode version
Theorem 4oadist 1044
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 = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
4oa.2 f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
4oadist.1 h =< (a ->1 d)
4oadist.2 j =< f
4oadist.3 k =< f
4oadist.4 (h ^ (b ->1 d)) =< k
Assertion
Ref Expression
4oadist (h ^ (j v k)) = ((h ^ j) v (h ^ k))
Proof of Theorem 4oadist
StepHypRef Expression
1 4oadist.2 . . . . . . . . . 10 j =< f
2 4oadist.3 . . . . . . . . . 10 k =< f
31, 2le2or 168 . . . . . . . . 9 (j v k) =< (f v f)
4 oridm 110 . . . . . . . . 9 (f v f) = f
53, 4lbtr 139 . . . . . . . 8 (j v k) =< f
65lelan 167 . . . . . . 7 (h ^ (j v k)) =< (h ^ f)
76df2le2 136 . . . . . 6 ((h ^ (j v k)) ^ (h ^ f)) = (h ^ (j v k))
87ax-r1 35 . . . . 5 (h ^ (j v k)) = ((h ^ (j v k)) ^ (h ^ f))
9 4oa.2 . . . . . . . . 9 f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
10 or32 82 . . . . . . . . 9 (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e) = (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))
119, 10ax-r2 36 . . . . . . . 8 f = (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))
1211lan 77 . . . . . . 7 (h ^ f) = (h ^ (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d))))
13 4oa.1 . . . . . . . 8 e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
14 leo 158 . . . . . . . . 9 ((a ^ b) v e) =< (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))
1511ax-r1 35 . . . . . . . . 9 (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d))) = f
1614, 15lbtr 139 . . . . . . . 8 ((a ^ b) v e) =< f
17 4oadist.1 . . . . . . . 8 h =< (a ->1 d)
1813, 9, 16, 174oagen1b 1043 . . . . . . 7 (h ^ (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (b ->1 d))
1912, 18ax-r2 36 . . . . . 6 (h ^ f) = (h ^ (b ->1 d))
2019lan 77 . . . . 5 ((h ^ (j v k)) ^ (h ^ f)) = ((h ^ (j v k)) ^ (h ^ (b ->1 d)))
218, 20ax-r2 36 . . . 4 (h ^ (j v k)) = ((h ^ (j v k)) ^ (h ^ (b ->1 d)))
22 lear 161 . . . . 5 ((h ^ (j v k)) ^ (h ^ (b ->1 d))) =< (h ^ (b ->1 d))
23 4oadist.4 . . . . . . . . 9 (h ^ (b ->1 d)) =< k
2423df2le2 136 . . . . . . . 8 ((h ^ (b ->1 d)) ^ k) = (h ^ (b ->1 d))
2524ax-r1 35 . . . . . . 7 (h ^ (b ->1 d)) = ((h ^ (b ->1 d)) ^ k)
26 an32 83 . . . . . . 7 ((h ^ (b ->1 d)) ^ k) = ((h ^ k) ^ (b ->1 d))
2725, 26ax-r2 36 . . . . . 6 (h ^ (b ->1 d)) = ((h ^ k) ^ (b ->1 d))
28 lea 160 . . . . . 6 ((h ^ k) ^ (b ->1 d)) =< (h ^ k)
2927, 28bltr 138 . . . . 5 (h ^ (b ->1 d)) =< (h ^ k)
3022, 29letr 137 . . . 4 ((h ^ (j v k)) ^ (h ^ (b ->1 d))) =< (h ^ k)
3121, 30bltr 138 . . 3 (h ^ (j v k)) =< (h ^ k)
32 leor 159 . . 3 (h ^ k) =< ((h ^ j) v (h ^ k))
3331, 32letr 137 . 2 (h ^ (j v k)) =< ((h ^ j) v (h ^ k))
34 ledi 174 . 2 ((h ^ j) v (h ^ k)) =< (h ^ (j v k))
3533, 34lebi 145 1 (h ^ (j v k)) = ((h ^ j) v (h ^ k))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2   v 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