QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-2to2s GIF version

Theorem oa3-2to2s 990
Description: Derivation of 3-OA variant from weaker version. (Contributed by NM, 25-Dec-1998.)
Hypotheses
Ref Expression
oa3-2to2s.1 ((a1 d) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 d) ∩ (b1 d)))))) ≤ d
oa3-2to2s.2 d = ((ac) ∪ (bc))
Assertion
Ref Expression
oa3-2to2s ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ ((ac) ∪ (bc))

Proof of Theorem oa3-2to2s
StepHypRef Expression
1 id 59 . . 3 (a1 c) = (a1 c)
2 id 59 . . 3 (b1 c) = (b1 c)
3 id 59 . . 3 (0 →1 c) = (0 →1 c)
4 leo 158 . . . . 5 a ≤ (a ∪ (ac))
5 df-i1 44 . . . . . . 7 (a1 c) = (a ∪ (ac))
65ax-r1 35 . . . . . 6 (a ∪ (ac)) = (a1 c)
7 ax-a1 30 . . . . . 6 (a1 c) = (a1 c)
86, 7ax-r2 36 . . . . 5 (a ∪ (ac)) = (a1 c)
94, 8lbtr 139 . . . 4 a ≤ (a1 c)
10 leo 158 . . . . 5 b ≤ (b ∪ (bc))
11 df-i1 44 . . . . . . 7 (b1 c) = (b ∪ (bc))
1211ax-r1 35 . . . . . 6 (b ∪ (bc)) = (b1 c)
13 ax-a1 30 . . . . . 6 (b1 c) = (b1 c)
1412, 13ax-r2 36 . . . . 5 (b ∪ (bc)) = (b1 c)
1510, 14lbtr 139 . . . 4 b ≤ (b1 c)
16 leo 158 . . . . 5 0 ≤ (0 ∪ (0 ∩ c))
17 df-i1 44 . . . . . . 7 (0 →1 c) = (0 ∪ (0 ∩ c))
1817ax-r1 35 . . . . . 6 (0 ∪ (0 ∩ c)) = (0 →1 c)
19 ax-a1 30 . . . . . 6 (0 →1 c) = (0 →1 c)
2018, 19ax-r2 36 . . . . 5 (0 ∪ (0 ∩ c)) = (0 →1 c)
2116, 20lbtr 139 . . . 4 0 ≤ (0 →1 c)
22 or0 102 . . . . . 6 (d ∪ 0) = d
2322ax-r1 35 . . . . 5 d = (d ∪ 0)
24 oa3-2to2s.2 . . . . . . 7 d = ((ac) ∪ (bc))
255lan 77 . . . . . . . . . . 11 (a ∩ (a1 c)) = (a ∩ (a ∪ (ac)))
26 omla 447 . . . . . . . . . . 11 (a ∩ (a ∪ (ac))) = (ac)
2725, 26ax-r2 36 . . . . . . . . . 10 (a ∩ (a1 c)) = (ac)
2827ax-r1 35 . . . . . . . . 9 (ac) = (a ∩ (a1 c))
29 ax-a1 30 . . . . . . . . . 10 a = a
3029, 72an 79 . . . . . . . . 9 (a ∩ (a1 c)) = (a ∩ (a1 c) )
3128, 30ax-r2 36 . . . . . . . 8 (ac) = (a ∩ (a1 c) )
3211lan 77 . . . . . . . . . . 11 (b ∩ (b1 c)) = (b ∩ (b ∪ (bc)))
33 omla 447 . . . . . . . . . . 11 (b ∩ (b ∪ (bc))) = (bc)
3432, 33ax-r2 36 . . . . . . . . . 10 (b ∩ (b1 c)) = (bc)
3534ax-r1 35 . . . . . . . . 9 (bc) = (b ∩ (b1 c))
36 ax-a1 30 . . . . . . . . . 10 b = b
3736, 132an 79 . . . . . . . . 9 (b ∩ (b1 c)) = (b ∩ (b1 c) )
3835, 37ax-r2 36 . . . . . . . 8 (bc) = (b ∩ (b1 c) )
3931, 382or 72 . . . . . . 7 ((ac) ∪ (bc)) = ((a ∩ (a1 c) ) ∪ (b ∩ (b1 c) ))
4024, 39ax-r2 36 . . . . . 6 d = ((a ∩ (a1 c) ) ∪ (b ∩ (b1 c) ))
41 an1 106 . . . . . . . 8 (0 ∩ 1) = 0
4241ax-r1 35 . . . . . . 7 0 = (0 ∩ 1)
43 ax-a1 30 . . . . . . . 8 0 = 0
44 0i1 273 . . . . . . . . . 10 (0 →1 c) = 1
4544ax-r1 35 . . . . . . . . 9 1 = (0 →1 c)
4645, 19ax-r2 36 . . . . . . . 8 1 = (0 →1 c)
4743, 462an 79 . . . . . . 7 (0 ∩ 1) = (0 ∩ (0 →1 c) )
4842, 47ax-r2 36 . . . . . 6 0 = (0 ∩ (0 →1 c) )
4940, 482or 72 . . . . 5 (d ∪ 0) = (((a ∩ (a1 c) ) ∪ (b ∩ (b1 c) )) ∪ (0 ∩ (0 →1 c) ))
5023, 49ax-r2 36 . . . 4 d = (((a ∩ (a1 c) ) ∪ (b ∩ (b1 c) )) ∪ (0 ∩ (0 →1 c) ))
51 oa3-2lema 978 . . . . 5 ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((a ∩ 0) ∪ ((a1 d) ∩ (0 →1 d))) ∩ ((b ∩ 0) ∪ ((b1 d) ∩ (0 →1 d)))))))) = ((a1 d) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 d) ∩ (b1 d))))))
52 oa3-2to2s.1 . . . . 5 ((a1 d) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 d) ∩ (b1 d)))))) ≤ d
5351, 52bltr 138 . . . 4 ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((a ∩ 0) ∪ ((a1 d) ∩ (0 →1 d))) ∩ ((b ∩ 0) ∪ ((b1 d) ∩ (0 →1 d)))))))) ≤ d
549, 15, 21, 50, 29, 36, 43, 53oa4to6 965 . . 3 (((a ∪ (a1 c) ) ∩ (b ∪ (b1 c) )) ∩ (0 ∪ (0 →1 c) )) ≤ ((a1 c) ∪ (a ∩ (b ∪ (((ab ) ∩ ((a1 c) ∪ (b1 c) )) ∩ (((a ∪ 0 ) ∩ ((a1 c) ∪ (0 →1 c) )) ∪ ((b ∪ 0 ) ∩ ((b1 c) ∪ (0 →1 c) )))))))
551, 2, 3, 54oa6to4 958 . 2 ((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((a ∩ 0) ∪ ((a1 c) ∩ (0 →1 c))) ∩ ((b ∩ 0) ∪ ((b1 c) ∩ (0 →1 c)))))))) ≤ (((ac) ∪ (bc)) ∪ (0 ∩ c))
56 oa3-2lema 978 . 2 ((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((a ∩ 0) ∪ ((a1 c) ∩ (0 →1 c))) ∩ ((b ∩ 0) ∪ ((b1 c) ∩ (0 →1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))
57 ancom 74 . . . . 5 (0 ∩ c) = (c ∩ 0)
58 an0 108 . . . . 5 (c ∩ 0) = 0
5957, 58ax-r2 36 . . . 4 (0 ∩ c) = 0
6059lor 70 . . 3 (((ac) ∪ (bc)) ∪ (0 ∩ c)) = (((ac) ∪ (bc)) ∪ 0)
61 or0 102 . . 3 (((ac) ∪ (bc)) ∪ 0) = ((ac) ∪ (bc))
6260, 61ax-r2 36 . 2 (((ac) ∪ (bc)) ∪ (0 ∩ c)) = ((ac) ∪ (bc))
6355, 56, 62le3tr2 141 1 ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ ((ac) ∪ (bc))
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  wo 6  wa 7  1wt 8  0wf 9  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