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

Theorem oa4gto4u 976
 Description: A "universal" 4-OA derived from the Godowski/Greechie form. The hypotheses are the Godowski/Greechie form of the proper 4-OA and substitutions into it.
Hypotheses
Ref Expression
oa4gto4u.1 ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))) ≤ (f1 d)
oa4gto4u.2 f = (a1 d)
oa4gto4u3 e = (b1 d)
oa4gto4u.4 g = (c1 d)
Assertion
Ref Expression
oa4gto4u ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Proof of Theorem oa4gto4u
StepHypRef Expression
1 oa4gto4u.2 . . . 4 f = (a1 d)
21ud1lem0b 256 . . . . . 6 (f1 d) = ((a1 d) →1 d)
3 u1lem12 781 . . . . . 6 ((a1 d) →1 d) = (a1 d)
42, 3ax-r2 36 . . . . 5 (f1 d) = (a1 d)
5 oa4gto4u3 . . . . . . . 8 e = (b1 d)
65ud1lem0b 256 . . . . . . 7 (e1 d) = ((b1 d) →1 d)
7 u1lem12 781 . . . . . . 7 ((b1 d) →1 d) = (b1 d)
86, 7ax-r2 36 . . . . . 6 (e1 d) = (b1 d)
9 ancom 74 . . . . . . . . 9 (ef) = (fe)
101, 52an 79 . . . . . . . . 9 (fe) = ((a1 d) ∩ (b1 d))
119, 10ax-r2 36 . . . . . . . 8 (ef) = ((a1 d) ∩ (b1 d))
12 ancom 74 . . . . . . . . 9 ((e1 d) ∩ (f1 d)) = ((f1 d) ∩ (e1 d))
134, 82an 79 . . . . . . . . 9 ((f1 d) ∩ (e1 d)) = ((a1 d) ∩ (b1 d))
1412, 13ax-r2 36 . . . . . . . 8 ((e1 d) ∩ (f1 d)) = ((a1 d) ∩ (b1 d))
1511, 142or 72 . . . . . . 7 ((ef) ∪ ((e1 d) ∩ (f1 d))) = (((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d)))
16 ancom 74 . . . . . . . 8 (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))) = (((fg) ∪ ((f1 d) ∩ (g1 d))) ∩ ((eg) ∪ ((e1 d) ∩ (g1 d))))
17 oa4gto4u.4 . . . . . . . . . . 11 g = (c1 d)
181, 172an 79 . . . . . . . . . 10 (fg) = ((a1 d) ∩ (c1 d))
1917ud1lem0b 256 . . . . . . . . . . . 12 (g1 d) = ((c1 d) →1 d)
20 u1lem12 781 . . . . . . . . . . . 12 ((c1 d) →1 d) = (c1 d)
2119, 20ax-r2 36 . . . . . . . . . . 11 (g1 d) = (c1 d)
224, 212an 79 . . . . . . . . . 10 ((f1 d) ∩ (g1 d)) = ((a1 d) ∩ (c1 d))
2318, 222or 72 . . . . . . . . 9 ((fg) ∪ ((f1 d) ∩ (g1 d))) = (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))
245, 172an 79 . . . . . . . . . 10 (eg) = ((b1 d) ∩ (c1 d))
258, 212an 79 . . . . . . . . . 10 ((e1 d) ∩ (g1 d)) = ((b1 d) ∩ (c1 d))
2624, 252or 72 . . . . . . . . 9 ((eg) ∪ ((e1 d) ∩ (g1 d))) = (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))
2723, 262an 79 . . . . . . . 8 (((fg) ∪ ((f1 d) ∩ (g1 d))) ∩ ((eg) ∪ ((e1 d) ∩ (g1 d)))) = ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))
2816, 27ax-r2 36 . . . . . . 7 (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))) = ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))
2915, 282or 72 . . . . . 6 (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d))))) = ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))
308, 292an 79 . . . . 5 ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))) = ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))
314, 302or 72 . . . 4 ((f1 d) ∪ ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d))))))) = ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))
321, 312an 79 . . 3 (f ∩ ((f1 d) ∪ ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) = ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))))
3332ax-r1 35 . 2 ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) = (f ∩ ((f1 d) ∪ ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d))))))))
34 oa4gto4u.1 . . 3 ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))) ≤ (f1 d)
3534oaur 930 . 2 (f ∩ ((f1 d) ∪ ((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ d
3633, 35bltr 138 1 ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ 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:  d6oa  997  axoa4  1034
 Copyright terms: Public domain W3C validator