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

Theorem oa4uto4g 975
Description: Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 974. (Contributed by NM, 28-Dec-1998.)
Hypotheses
Ref Expression
oa4uto4g.1 ((b1 d) ∩ ((b 1 d) ∪ ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))))))) ≤ d
oa4uto4g.4 h = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))
Assertion
Ref Expression
oa4uto4g ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)) ≤ (b1 d)

Proof of Theorem oa4uto4g
StepHypRef Expression
1 ancom 74 . . . . . . . 8 (ab) = (ba)
2 ancom 74 . . . . . . . 8 ((a1 d) ∩ (b1 d)) = ((b1 d) ∩ (a1 d))
31, 22or 72 . . . . . . 7 ((ab) ∪ ((a1 d) ∩ (b1 d))) = ((ba) ∪ ((b1 d) ∩ (a1 d)))
43ax-r5 38 . . . . . 6 (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h) = (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h)
54lan 77 . . . . 5 ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)) = ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h))
65lor 70 . . . 4 ((b1 d) ∪ ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h))) = ((b1 d) ∪ ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h)))
76lan 77 . . 3 (b ∩ ((b1 d) ∪ ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)))) = (b ∩ ((b1 d) ∪ ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h))))
8 u1lem9a 777 . . . . . 6 (b1 d)b
98lecon1 155 . . . . 5 b ≤ (b1 d)
10 u1lem9a 777 . . . . . . . . . . 11 (a1 d)a
1110lecon1 155 . . . . . . . . . 10 a ≤ (a1 d)
129, 11le2an 169 . . . . . . . . 9 (ba) ≤ ((b1 d) ∩ (a1 d))
1312leror 152 . . . . . . . 8 ((ba) ∪ ((b1 d) ∩ (a1 d))) ≤ (((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d)))
14 oa4uto4g.4 . . . . . . . . 9 h = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))
15 u1lem9a 777 . . . . . . . . . . . . 13 (c1 d)c
1615lecon1 155 . . . . . . . . . . . 12 c ≤ (c1 d)
1711, 16le2an 169 . . . . . . . . . . 11 (ac) ≤ ((a1 d) ∩ (c1 d))
1817leror 152 . . . . . . . . . 10 ((ac) ∪ ((a1 d) ∩ (c1 d))) ≤ (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))
199, 16le2an 169 . . . . . . . . . . 11 (bc) ≤ ((b1 d) ∩ (c1 d))
2019leror 152 . . . . . . . . . 10 ((bc) ∪ ((b1 d) ∩ (c1 d))) ≤ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))
2118, 20le2an 169 . . . . . . . . 9 (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))) ≤ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))
2214, 21bltr 138 . . . . . . . 8 h ≤ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))
2313, 22le2or 168 . . . . . . 7 (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h) ≤ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))
2423lelan 167 . . . . . 6 ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h)) ≤ ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))
2524lelor 166 . . . . 5 ((b1 d) ∪ ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h))) ≤ ((b1 d) ∪ ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))
269, 25le2an 169 . . . 4 (b ∩ ((b1 d) ∪ ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h)))) ≤ ((b1 d) ∩ ((b1 d) ∪ ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))))
27 ax-a1 30 . . . . . . . 8 b = b
2827ud1lem0b 256 . . . . . . 7 (b1 d) = (b 1 d)
29 ax-a1 30 . . . . . . . . 9 a = a
3029ud1lem0b 256 . . . . . . . 8 (a1 d) = (a 1 d)
3128, 302an 79 . . . . . . . . . 10 ((b1 d) ∩ (a1 d)) = ((b 1 d) ∩ (a 1 d))
3231lor 70 . . . . . . . . 9 (((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) = (((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d)))
33 ancom 74 . . . . . . . . . 10 ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))) = ((((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))))
34 ax-a1 30 . . . . . . . . . . . . . 14 c = c
3534ud1lem0b 256 . . . . . . . . . . . . 13 (c1 d) = (c 1 d)
3628, 352an 79 . . . . . . . . . . . 12 ((b1 d) ∩ (c1 d)) = ((b 1 d) ∩ (c 1 d))
3736lor 70 . . . . . . . . . . 11 (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))) = (((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d)))
3830, 352an 79 . . . . . . . . . . . 12 ((a1 d) ∩ (c1 d)) = ((a 1 d) ∩ (c 1 d))
3938lor 70 . . . . . . . . . . 11 (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) = (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))
4037, 392an 79 . . . . . . . . . 10 ((((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))) = ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d))))
4133, 40ax-r2 36 . . . . . . . . 9 ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))) = ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d))))
4232, 412or 72 . . . . . . . 8 ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))) = ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))))
4330, 422an 79 . . . . . . 7 ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))) = ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d))))))
4428, 432or 72 . . . . . 6 ((b1 d) ∪ ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))) = ((b 1 d) ∪ ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))))))
4544lan 77 . . . . 5 ((b1 d) ∩ ((b1 d) ∪ ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) = ((b1 d) ∩ ((b 1 d) ∪ ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d))))))))
46 oa4uto4g.1 . . . . 5 ((b1 d) ∩ ((b 1 d) ∪ ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))))))) ≤ d
4745, 46bltr 138 . . . 4 ((b1 d) ∩ ((b1 d) ∪ ((a1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (a1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d
4826, 47letr 137 . . 3 (b ∩ ((b1 d) ∪ ((a1 d) ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ h)))) ≤ d
497, 48bltr 138 . 2 (b ∩ ((b1 d) ∪ ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)))) ≤ d
5049oau 929 1 ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)) ≤ (b1 d)
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  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:  4oa  1039
  Copyright terms: Public domain W3C validator