QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  distoa Unicode version
Theorem distoa 944
Description: Derivation in OM of OA, assuming OA distributive law oadistd 1023.
Hypotheses
Ref Expression
distoa.1 d = (a ->2 b)
distoa.2 e = ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))
distoa.3 f = ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))
distoa.4 (d ^ (e v f)) = ((d ^ e) v (d ^ f))
Assertion
Ref Expression
distoa ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Proof of Theorem distoa
StepHypRef Expression
1 1oa 820 . . 3 ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
2 2oath1 826 . . . 4 ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (a ->2 c))
3 lear 161 . . . 4 ((a ->2 b) ^ (a ->2 c)) =< (a ->2 c)
42, 3bltr 138 . . 3 ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
51, 4le2or 168 . 2 (((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) =< ((a ->2 c) v (a ->2 c))
6 distoa.4 . . . . 5 (d ^ (e v f)) = ((d ^ e) v (d ^ f))
7 distoa.1 . . . . . 6 d = (a ->2 b)
8 distoa.2 . . . . . . 7 e = ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))
9 distoa.3 . . . . . . 7 f = ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))
108, 92or 72 . . . . . 6 (e v f) = (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))
117, 102an 79 . . . . 5 (d ^ (e v f)) = ((a ->2 b) ^ (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
127, 82an 79 . . . . . 6 (d ^ e) = ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c))))
137, 92an 79 . . . . . 6 (d ^ f) = ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))
1412, 132or 72 . . . . 5 ((d ^ e) v (d ^ f)) = (((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
156, 11, 143tr2 64 . . . 4 ((a ->2 b) ^ (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
1615ax-r1 35 . . 3 (((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = ((a ->2 b) ^ (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
17 u12lem 771 . . . . 5 (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))
18 df-i0 43 . . . . 5 ((b v c) ->0 ((a ->2 b) ^ (a ->2 c))) = ((b v c)' v ((a ->2 b) ^ (a ->2 c)))
1917, 18ax-r2 36 . . . 4 (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((b v c)' v ((a ->2 b) ^ (a ->2 c)))
2019lan 77 . . 3 ((a ->2 b) ^ (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c))))
2116, 20ax-r2 36 . 2 (((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c))))
22 oridm 110 . 2 ((a ->2 c) v (a ->2 c)) = (a ->2 c)
235, 21, 22le3tr2 141 1 ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v 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