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

Theorem oa3-u2 992
Description: Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA. (Contributed by NM, 27-Dec-1998.)
Hypothesis
Ref Expression
oa3-u2.1 (((a1 c) →1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ (((a1 c) →1 c) ∩ (c1 c))) ∪ ((((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c))) ∩ ((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c)))))))) ≤ c
Assertion
Ref Expression
oa3-u2 ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) ≤ c

Proof of Theorem oa3-u2
StepHypRef Expression
1 oa3-u2lem 986 . . 3 ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))))
21ax-r1 35 . 2 ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) = ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))))))))
3 u1lem9ab 779 . . 3 (a1 c) ≤ (a1 c)
4 le1 146 . . 3 c ≤ 1
5 u1lem9ab 779 . . 3 (b1 c) ≤ (b1 c)
6 or32 82 . . . . 5 ((((a1 c) ∩ (a1 c)) ∪ (c ∩ 1)) ∪ ((b1 c) ∩ (b1 c))) = ((((a1 c) ∩ (a1 c)) ∪ ((b1 c) ∩ (b1 c))) ∪ (c ∩ 1))
7 ancom 74 . . . . . . . 8 ((a1 c) ∩ (a1 c)) = ((a1 c) ∩ (a1 c))
8 u1lem8 776 . . . . . . . 8 ((a1 c) ∩ (a1 c)) = ((ac) ∪ (ac))
97, 8ax-r2 36 . . . . . . 7 ((a1 c) ∩ (a1 c)) = ((ac) ∪ (ac))
10 ancom 74 . . . . . . . 8 ((b1 c) ∩ (b1 c)) = ((b1 c) ∩ (b1 c))
11 u1lem8 776 . . . . . . . 8 ((b1 c) ∩ (b1 c)) = ((bc) ∪ (bc))
1210, 11ax-r2 36 . . . . . . 7 ((b1 c) ∩ (b1 c)) = ((bc) ∪ (bc))
139, 122or 72 . . . . . 6 (((a1 c) ∩ (a1 c)) ∪ ((b1 c) ∩ (b1 c))) = (((ac) ∪ (ac)) ∪ ((bc) ∪ (bc)))
14 an1 106 . . . . . 6 (c ∩ 1) = c
1513, 142or 72 . . . . 5 ((((a1 c) ∩ (a1 c)) ∪ ((b1 c) ∩ (b1 c))) ∪ (c ∩ 1)) = ((((ac) ∪ (ac)) ∪ ((bc) ∪ (bc))) ∪ c)
16 lear 161 . . . . . . . 8 (ac) ≤ c
17 lear 161 . . . . . . . 8 (ac) ≤ c
1816, 17lel2or 170 . . . . . . 7 ((ac) ∪ (ac)) ≤ c
19 lear 161 . . . . . . . 8 (bc) ≤ c
20 lear 161 . . . . . . . 8 (bc) ≤ c
2119, 20lel2or 170 . . . . . . 7 ((bc) ∪ (bc)) ≤ c
2218, 21lel2or 170 . . . . . 6 (((ac) ∪ (ac)) ∪ ((bc) ∪ (bc))) ≤ c
2322df-le2 131 . . . . 5 ((((ac) ∪ (ac)) ∪ ((bc) ∪ (bc))) ∪ c) = c
246, 15, 233tr 65 . . . 4 ((((a1 c) ∩ (a1 c)) ∪ (c ∩ 1)) ∪ ((b1 c) ∩ (b1 c))) = c
2524ax-r1 35 . . 3 c = ((((a1 c) ∩ (a1 c)) ∪ (c ∩ 1)) ∪ ((b1 c) ∩ (b1 c)))
26 oa3-u2.1 . . 3 (((a1 c) →1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ (((a1 c) →1 c) ∩ (c1 c))) ∪ ((((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c))) ∩ ((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c)))))))) ≤ c
273, 4, 5, 25, 26oa4to6dual 964 . 2 ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))))) ≤ c
282, 27bltr 138 1 ((a1 c) ∩ ((a1 c) ∪ (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