QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  sadm3 Unicode version
Theorem sadm3 838
Description: Weak DeMorgan's law for attempt at Sasaki algebra.
Assertion
Ref Expression
sadm3 (((a' ->1 c) ^ (b' ->1 c)) ->1 c) =< ((a ->1 c) v (b ->1 c))
Proof of Theorem sadm3
StepHypRef Expression
1 oran3 93 . . . . . . 7 ((a' ->1 c)' v (b' ->1 c)') = ((a' ->1 c) ^ (b' ->1 c))'
21ax-r1 35 . . . . . 6 ((a' ->1 c) ^ (b' ->1 c))' = ((a' ->1 c)' v (b' ->1 c)')
3 u1lem9a 777 . . . . . . 7 (a' ->1 c)' =< a'
4 u1lem9a 777 . . . . . . 7 (b' ->1 c)' =< b'
53, 4le2or 168 . . . . . 6 ((a' ->1 c)' v (b' ->1 c)') =< (a' v b')
62, 5bltr 138 . . . . 5 ((a' ->1 c) ^ (b' ->1 c))' =< (a' v b')
7 an32 83 . . . . . 6 (((a' ->1 c) ^ (b' ->1 c)) ^ c) = (((a' ->1 c) ^ c) ^ (b' ->1 c))
8 lea 160 . . . . . 6 (((a' ->1 c) ^ c) ^ (b' ->1 c)) =< ((a' ->1 c) ^ c)
97, 8bltr 138 . . . . 5 (((a' ->1 c) ^ (b' ->1 c)) ^ c) =< ((a' ->1 c) ^ c)
106, 9le2or 168 . . . 4 (((a' ->1 c) ^ (b' ->1 c))' v (((a' ->1 c) ^ (b' ->1 c)) ^ c)) =< ((a' v b') v ((a' ->1 c) ^ c))
11 leo 158 . . . . . 6 (a' v b') =< ((a' v b') v (a ^ c))
12 or32 82 . . . . . 6 ((a' v b') v (a ^ c)) = ((a' v (a ^ c)) v b')
1311, 12lbtr 139 . . . . 5 (a' v b') =< ((a' v (a ^ c)) v b')
14 u1lemab 610 . . . . . . 7 ((a' ->1 c) ^ c) = ((a' ^ c) v (a'' ^ c))
15 lea 160 . . . . . . . 8 (a' ^ c) =< a'
16 ax-a1 30 . . . . . . . . . . 11 a = a''
1716ax-r1 35 . . . . . . . . . 10 a'' = a
1817bile 142 . . . . . . . . 9 a'' =< a
1918leran 153 . . . . . . . 8 (a'' ^ c) =< (a ^ c)
2015, 19le2or 168 . . . . . . 7 ((a' ^ c) v (a'' ^ c)) =< (a' v (a ^ c))
2114, 20bltr 138 . . . . . 6 ((a' ->1 c) ^ c) =< (a' v (a ^ c))
22 leo 158 . . . . . 6 (a' v (a ^ c)) =< ((a' v (a ^ c)) v b')
2321, 22letr 137 . . . . 5 ((a' ->1 c) ^ c) =< ((a' v (a ^ c)) v b')
2413, 23lel2or 170 . . . 4 ((a' v b') v ((a' ->1 c) ^ c)) =< ((a' v (a ^ c)) v b')
2510, 24letr 137 . . 3 (((a' ->1 c) ^ (b' ->1 c))' v (((a' ->1 c) ^ (b' ->1 c)) ^ c)) =< ((a' v (a ^ c)) v b')
26 leo 158 . . . 4 b' =< (b' v (b ^ c))
2726lelor 166 . . 3 ((a' v (a ^ c)) v b') =< ((a' v (a ^ c)) v (b' v (b ^ c)))
2825, 27letr 137 . 2 (((a' ->1 c) ^ (b' ->1 c))' v (((a' ->1 c) ^ (b' ->1 c)) ^ c)) =< ((a' v (a ^ c)) v (b' v (b ^ c)))
29 df-i1 44 . 2 (((a' ->1 c) ^ (b' ->1 c)) ->1 c) = (((a' ->1 c) ^ (b' ->1 c))' v (((a' ->1 c) ^ (b' ->1 c)) ^ c))
30 df-i1 44 . . 3 (a ->1 c) = (a' v (a ^ c))
31 df-i1 44 . . 3 (b ->1 c) = (b' v (b ^ c))
3230, 312or 72 . 2 ((a ->1 c) v (b ->1 c)) = ((a' v (a ^ c)) v (b' v (b ^ c)))
3328, 29, 32le3tr1 140 1 (((a' ->1 c) ^ (b' ->1 c)) ->1 c) =< ((a ->1 c) v (b ->1 c))
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   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
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