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

Theorem oa4to6 965
 Description: Orthoarguesian law (4-variable to 6-variable proof). The first 3 hypotheses are those for 6-OA. The next 4 are variable substitutions into 4-OA. The last is the 4-OA. The proof uses OM logic only.
Hypotheses
Ref Expression
oa4to6.oa6.1 ab
oa4to6.oa6.2 cd
oa4to6.oa6.3 ef
oa4to6.4 g = (((ab ) ∪ (cd )) ∪ (ef ))
oa4to6.5 h = a
oa4to6.6 j = c
oa4to6.7 k = e
oa4to6.oa4 ((h1 g) ∩ (h ∪ (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))))))) ≤ g
Assertion
Ref Expression
oa4to6 (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Proof of Theorem oa4to6
StepHypRef Expression
1 oa4to6.oa6.1 . . . . 5 ab
21lecon3 157 . . . 4 ba
32lecon 154 . . 3 a b
4 oa4to6.oa6.2 . . . . 5 cd
54lecon3 157 . . . 4 dc
65lecon 154 . . 3 c d
7 oa4to6.oa6.3 . . . . 5 ef
87lecon3 157 . . . 4 fe
98lecon 154 . . 3 e f
10 id 59 . . 3 (((ab ) ∪ (cd )) ∪ (ef )) = (((ab ) ∪ (cd )) ∪ (ef ))
11 oa4to6.oa4 . . . 4 ((h1 g) ∩ (h ∪ (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))))))) ≤ g
12 oa4to6.5 . . . . . 6 h = a
13 oa4to6.4 . . . . . 6 g = (((ab ) ∪ (cd )) ∪ (ef ))
1412, 13ud1lem0ab 257 . . . . 5 (h1 g) = (a1 (((ab ) ∪ (cd )) ∪ (ef )))
15 oa4to6.6 . . . . . . 7 j = c
1612, 152an 79 . . . . . . . . 9 (hj) = (ac )
1715, 13ud1lem0ab 257 . . . . . . . . . 10 (j1 g) = (c1 (((ab ) ∪ (cd )) ∪ (ef )))
1814, 172an 79 . . . . . . . . 9 ((h1 g) ∩ (j1 g)) = ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef ))))
1916, 182or 72 . . . . . . . 8 ((hj) ∪ ((h1 g) ∩ (j1 g))) = ((ac ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef )))))
20 oa4to6.7 . . . . . . . . . . 11 k = e
2112, 202an 79 . . . . . . . . . 10 (hk) = (ae )
2220, 13ud1lem0ab 257 . . . . . . . . . . 11 (k1 g) = (e1 (((ab ) ∪ (cd )) ∪ (ef )))
2314, 222an 79 . . . . . . . . . 10 ((h1 g) ∩ (k1 g)) = ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))
2421, 232or 72 . . . . . . . . 9 ((hk) ∪ ((h1 g) ∩ (k1 g))) = ((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef )))))
2515, 202an 79 . . . . . . . . . 10 (jk) = (ce )
2617, 222an 79 . . . . . . . . . 10 ((j1 g) ∩ (k1 g)) = ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))
2725, 262or 72 . . . . . . . . 9 ((jk) ∪ ((j1 g) ∩ (k1 g))) = ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef )))))
2824, 272an 79 . . . . . . . 8 (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))) = (((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∩ ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))))
2919, 282or 72 . . . . . . 7 (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g))))) = (((ac ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∪ (((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∩ ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef )))))))
3015, 292an 79 . . . . . 6 (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))))) = (c ∩ (((ac ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∪ (((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∩ ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))))))
3112, 302or 72 . . . . 5 (h ∪ (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g))))))) = (a ∪ (c ∩ (((ac ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∪ (((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∩ ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef )))))))))
3214, 312an 79 . . . 4 ((h1 g) ∩ (h ∪ (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))))))) = ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (a ∪ (c ∩ (((ac ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∪ (((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∩ ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))))))))
3311, 32, 13le3tr2 141 . . 3 ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (a ∪ (c ∩ (((ac ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (c1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∪ (((ae ) ∪ ((a1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef ))))) ∩ ((ce ) ∪ ((c1 (((ab ) ∪ (cd )) ∪ (ef ))) ∩ (e1 (((ab ) ∪ (cd )) ∪ (ef )))))))))) ≤ (((ab ) ∪ (cd )) ∪ (ef ))
343, 6, 9, 10, 33oa4to6dual 964 . 2 (b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))) ≤ (((ab ) ∪ (cd )) ∪ (ef ))
3534oa6fromdual 953 1 (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
 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  d6oa  997  oa6  1036
 Copyright terms: Public domain W3C validator