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

Theorem distoa 944
Description: Derivation in OM of OA, assuming OA distributive law oadistd 1023. (Contributed by NM, 29-Nov-1998.)
Hypotheses
Ref Expression
distoa.1 d = (a2 b)
distoa.2 e = ((bc) →1 ((a2 b) ∩ (a2 c)))
distoa.3 f = ((bc) →2 ((a2 b) ∩ (a2 c)))
distoa.4 (d ∩ (ef)) = ((de) ∪ (df))
Assertion
Ref Expression
distoa ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Proof of Theorem distoa
StepHypRef Expression
1 1oa 820 . . 3 ((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
2 2oath1 826 . . . 4 ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ (a2 c))
3 lear 161 . . . 4 ((a2 b) ∩ (a2 c)) ≤ (a2 c)
42, 3bltr 138 . . 3 ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
51, 4le2or 168 . 2 (((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c))))) ≤ ((a2 c) ∪ (a2 c))
6 distoa.4 . . . . 5 (d ∩ (ef)) = ((de) ∪ (df))
7 distoa.1 . . . . . 6 d = (a2 b)
8 distoa.2 . . . . . . 7 e = ((bc) →1 ((a2 b) ∩ (a2 c)))
9 distoa.3 . . . . . . 7 f = ((bc) →2 ((a2 b) ∩ (a2 c)))
108, 92or 72 . . . . . 6 (ef) = (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))
117, 102an 79 . . . . 5 (d ∩ (ef)) = ((a2 b) ∩ (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c)))))
127, 82an 79 . . . . . 6 (de) = ((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c))))
137, 92an 79 . . . . . 6 (df) = ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c))))
1412, 132or 72 . . . . 5 ((de) ∪ (df)) = (((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))))
156, 11, 143tr2 64 . . . 4 ((a2 b) ∩ (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))) = (((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))))
1615ax-r1 35 . . 3 (((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c))))) = ((a2 b) ∩ (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c)))))
17 u12lem 771 . . . . 5 (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c)))) = ((bc) →0 ((a2 b) ∩ (a2 c)))
18 df-i0 43 . . . . 5 ((bc) →0 ((a2 b) ∩ (a2 c))) = ((bc) ∪ ((a2 b) ∩ (a2 c)))
1917, 18ax-r2 36 . . . 4 (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c)))) = ((bc) ∪ ((a2 b) ∩ (a2 c)))
2019lan 77 . . 3 ((a2 b) ∩ (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))) = ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))
2116, 20ax-r2 36 . 2 (((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c))))) = ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))
22 oridm 110 . 2 ((a2 c) ∪ (a2 c)) = (a2 c)
235, 21, 22le3tr2 141 1 ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  wo 6  wa 7  0 wi0 11  1 wi1 12  2 wi2 13
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
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i0 43  df-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator