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

Theorem oa6to4 958
 Description: Derivation of 4-variable proper OA law, assuming 6-variable OA law.
Hypotheses
Ref Expression
oa6to4.1 b = (a1 g)
oa6to4.2 d = (c1 g)
oa6to4.3 f = (e1 g)
oa6to4.oa6 (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))
Assertion
Ref Expression
oa6to4 ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ (((ag) ∪ (cg)) ∪ (eg))

Proof of Theorem oa6to4
StepHypRef Expression
1 oa6to4.oa6 . . 3 (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))
21oa6todual 952 . 2 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))
3 oa6to4.1 . . . 4 b = (a1 g)
43con1 66 . . 3 b = (a1 g)
5 oa6to4.2 . . . . . . . . 9 d = (c1 g)
65con1 66 . . . . . . . 8 d = (c1 g)
74, 62an 79 . . . . . . 7 (bd) = ((a1 g) ∩ (c1 g))
87lor 70 . . . . . 6 ((ac) ∪ (bd)) = ((ac) ∪ ((a1 g) ∩ (c1 g)))
9 oa6to4.3 . . . . . . . . . 10 f = (e1 g)
109con1 66 . . . . . . . . 9 f = (e1 g)
114, 102an 79 . . . . . . . 8 (bf) = ((a1 g) ∩ (e1 g))
1211lor 70 . . . . . . 7 ((ae) ∪ (bf)) = ((ae) ∪ ((a1 g) ∩ (e1 g)))
136, 102an 79 . . . . . . . 8 (df) = ((c1 g) ∩ (e1 g))
1413lor 70 . . . . . . 7 ((ce) ∪ (df)) = ((ce) ∪ ((c1 g) ∩ (e1 g)))
1512, 142an 79 . . . . . 6 (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))) = (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g))))
168, 152or 72 . . . . 5 (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))) = (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))
1716lan 77 . . . 4 (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))) = (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g))))))
1817lor 70 . . 3 (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))))) = (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))
194, 182an 79 . 2 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) = ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g))))))))
204lan 77 . . . . 5 (ab) = (a ∩ (a1 g))
21 ancom 74 . . . . 5 (a ∩ (a1 g)) = ((a1 g) ∩ a)
22 u1lemaa 600 . . . . 5 ((a1 g) ∩ a) = (ag)
2320, 21, 223tr 65 . . . 4 (ab) = (ag)
246lan 77 . . . . 5 (cd) = (c ∩ (c1 g))
25 ancom 74 . . . . 5 (c ∩ (c1 g)) = ((c1 g) ∩ c)
26 u1lemaa 600 . . . . 5 ((c1 g) ∩ c) = (cg)
2724, 25, 263tr 65 . . . 4 (cd) = (cg)
2823, 272or 72 . . 3 ((ab) ∪ (cd)) = ((ag) ∪ (cg))
2910lan 77 . . . 4 (ef) = (e ∩ (e1 g))
30 ancom 74 . . . 4 (e ∩ (e1 g)) = ((e1 g) ∩ e)
31 u1lemaa 600 . . . 4 ((e1 g) ∩ e) = (eg)
3229, 30, 313tr 65 . . 3 (ef) = (eg)
3328, 322or 72 . 2 (((ab) ∪ (cd)) ∪ (ef)) = (((ag) ∪ (cg)) ∪ (eg))
342, 19, 33le3tr2 141 1 ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ (((ag) ∪ (cg)) ∪ (eg))
 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:  oa3-2to2s  990  axoa4a  1037
 Copyright terms: Public domain W3C validator