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

Theorem oa23 936
Description: Derivation of OA from Godowski/Greechie Eq. II.
Hypothesis
Ref Expression
oa23.1 (c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ≤ a
Assertion
Ref Expression
oa23 ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Proof of Theorem oa23
StepHypRef Expression
1 ax-a2 31 . . . . . . 7 (bc) = (cb)
21ax-r4 37 . . . . . 6 (bc) = (cb)
3 ancom 74 . . . . . 6 ((a2 b) ∩ (a2 c)) = ((a2 c) ∩ (a2 b))
42, 32or 72 . . . . 5 ((bc) ∪ ((a2 b) ∩ (a2 c))) = ((cb) ∪ ((a2 c) ∩ (a2 b)))
54lan 77 . . . 4 ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))
65ax-r5 38 . . 3 (((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ∪ (a2 c)) = (((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))) ∪ (a2 c))
7 ax-a2 31 . . 3 (((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))) ∪ (a2 c)) = ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
8 ax-a3 32 . . . . . . . . . 10 (((a2 c) ∪ (a2 c)) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) = ((a2 c) ∪ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))))
98ax-r1 35 . . . . . . . . 9 ((a2 c) ∪ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) = (((a2 c) ∪ (a2 c)) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
10 oridm 110 . . . . . . . . . 10 ((a2 c) ∪ (a2 c)) = (a2 c)
1110ax-r5 38 . . . . . . . . 9 (((a2 c) ∪ (a2 c)) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) = ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
129, 11ax-r2 36 . . . . . . . 8 ((a2 c) ∪ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) = ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
13 u2lemonb 636 . . . . . . . 8 ((a2 c) ∪ c ) = 1
1412, 132an 79 . . . . . . 7 (((a2 c) ∪ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ∩ ((a2 c) ∪ c )) = (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ 1)
1514ax-r1 35 . . . . . 6 (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ 1) = (((a2 c) ∪ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ∩ ((a2 c) ∪ c ))
16 an1 106 . . . . . . 7 (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ 1) = ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
1716ax-r1 35 . . . . . 6 ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) = (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ 1)
18 comorr 184 . . . . . . 7 (a2 c) C ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
19 u2lemc1 681 . . . . . . . . 9 c C (a2 c)
2019comcom 453 . . . . . . . 8 (a2 c) C c
2120comcom2 183 . . . . . . 7 (a2 c) C c
2218, 21fh3 471 . . . . . 6 ((a2 c) ∪ (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ c )) = (((a2 c) ∪ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ∩ ((a2 c) ∪ c ))
2315, 17, 223tr1 63 . . . . 5 ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) = ((a2 c) ∪ (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ c ))
24 oa23.1 . . . . . . . . 9 (c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ≤ a
25 lea 160 . . . . . . . . 9 (c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ≤ c
2624, 25ler2an 173 . . . . . . . 8 (c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ≤ (ac )
27 ancom 74 . . . . . . . 8 (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ c ) = (c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))))
28 u2lemanb 616 . . . . . . . 8 ((a2 c) ∩ c ) = (ac )
2926, 27, 28le3tr1 140 . . . . . . 7 (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ c ) ≤ ((a2 c) ∩ c )
3029lelor 166 . . . . . 6 ((a2 c) ∪ (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ c )) ≤ ((a2 c) ∪ ((a2 c) ∩ c ))
31 orabs 120 . . . . . 6 ((a2 c) ∪ ((a2 c) ∩ c )) = (a2 c)
3230, 31lbtr 139 . . . . 5 ((a2 c) ∪ (((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ∩ c )) ≤ (a2 c)
3323, 32bltr 138 . . . 4 ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) ≤ (a2 c)
34 leo 158 . . . 4 (a2 c) ≤ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))
3533, 34lebi 145 . . 3 ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b))))) = (a2 c)
366, 7, 353tr 65 . 2 (((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ∪ (a2 c)) = (a2 c)
3736df-le1 130 1 ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
Colors of variables: term
Syntax hints:  wle 2   wn 4  wo 6  wa 7  1wt 8  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-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  oa43v  1028  oa63v  1032
  Copyright terms: Public domain W3C validator