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

Theorem oa3-u1 991
Description: Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA.
Hypothesis
Ref Expression
oa3-u1.1 ((c1 c) ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ ((c1 c) ∩ ((a1 c) →1 c))) ∪ (((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c)))))))) ≤ c
Assertion
Ref Expression
oa3-u1 (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))) ≤ c

Proof of Theorem oa3-u1
StepHypRef Expression
1 oa3-u1lem 985 . . 3 (1 ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ (1 ∩ (a1 c))) ∪ (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) = (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))
21ax-r1 35 . 2 (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))) = (1 ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ (1 ∩ (a1 c))) ∪ (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))))
3 le1 146 . . . 4 c ≤ 1
4 u1lem9ab 779 . . . 4 (a1 c) ≤ (a1 c)
5 u1lem9ab 779 . . . 4 (b1 c) ≤ (b1 c)
6 ax-a2 31 . . . . . . 7 (c ∪ ((bc) ∪ (bc))) = (((bc) ∪ (bc)) ∪ c)
7 lear 161 . . . . . . . . 9 (bc) ≤ c
8 lear 161 . . . . . . . . 9 (bc) ≤ c
97, 8lel2or 170 . . . . . . . 8 ((bc) ∪ (bc)) ≤ c
109df-le2 131 . . . . . . 7 (((bc) ∪ (bc)) ∪ c) = c
116, 10ax-r2 36 . . . . . 6 (c ∪ ((bc) ∪ (bc))) = c
1211ax-r1 35 . . . . 5 c = (c ∪ ((bc) ∪ (bc)))
13 an1 106 . . . . . . . . 9 (c ∩ 1) = c
14 ancom 74 . . . . . . . . . 10 ((a1 c) ∩ (a1 c)) = ((a1 c) ∩ (a1 c))
15 u1lem8 776 . . . . . . . . . 10 ((a1 c) ∩ (a1 c)) = ((ac) ∪ (ac))
1614, 15ax-r2 36 . . . . . . . . 9 ((a1 c) ∩ (a1 c)) = ((ac) ∪ (ac))
1713, 162or 72 . . . . . . . 8 ((c ∩ 1) ∪ ((a1 c) ∩ (a1 c))) = (c ∪ ((ac) ∪ (ac)))
18 ax-a2 31 . . . . . . . 8 (c ∪ ((ac) ∪ (ac))) = (((ac) ∪ (ac)) ∪ c)
19 lear 161 . . . . . . . . . 10 (ac) ≤ c
20 lear 161 . . . . . . . . . 10 (ac) ≤ c
2119, 20lel2or 170 . . . . . . . . 9 ((ac) ∪ (ac)) ≤ c
2221df-le2 131 . . . . . . . 8 (((ac) ∪ (ac)) ∪ c) = c
2317, 18, 223tr 65 . . . . . . 7 ((c ∩ 1) ∪ ((a1 c) ∩ (a1 c))) = c
24 ancom 74 . . . . . . . 8 ((b1 c) ∩ (b1 c)) = ((b1 c) ∩ (b1 c))
25 u1lem8 776 . . . . . . . 8 ((b1 c) ∩ (b1 c)) = ((bc) ∪ (bc))
2624, 25ax-r2 36 . . . . . . 7 ((b1 c) ∩ (b1 c)) = ((bc) ∪ (bc))
2723, 262or 72 . . . . . 6 (((c ∩ 1) ∪ ((a1 c) ∩ (a1 c))) ∪ ((b1 c) ∩ (b1 c))) = (c ∪ ((bc) ∪ (bc)))
2827ax-r1 35 . . . . 5 (c ∪ ((bc) ∪ (bc))) = (((c ∩ 1) ∪ ((a1 c) ∩ (a1 c))) ∪ ((b1 c) ∩ (b1 c)))
2912, 28ax-r2 36 . . . 4 c = (((c ∩ 1) ∪ ((a1 c) ∩ (a1 c))) ∪ ((b1 c) ∩ (b1 c)))
30 oa3-u1.1 . . . 4 ((c1 c) ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ ((c1 c) ∩ ((a1 c) →1 c))) ∪ (((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c)))))))) ≤ c
313, 4, 5, 29, 30oa4to6dual 964 . . 3 (1 ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ (1 ∩ (a1 c))) ∪ (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) ≤ c
32 leid 148 . . 3 cc
3331, 32letr 137 . 2 (1 ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ (1 ∩ (a1 c))) ∪ (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) ≤ c
342, 33bltr 138 1 (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))) ≤ c
Colors of variables: term
Syntax hints:  wle 2   wn 4  wo 6  wa 7  1wt 8  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