QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4to6 Unicode 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 a =< b'
oa4to6.oa6.2 c =< d'
oa4to6.oa6.3 e =< f'
oa4to6.4 g = (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
oa4to6.5 h = a'
oa4to6.6 j = c'
oa4to6.7 k = e'
oa4to6.oa4 ((h ->1 g) ^ (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))))) =< g
Assertion
Ref Expression
oa4to6 (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Proof of Theorem oa4to6
StepHypRef Expression
1 oa4to6.oa6.1 . . . . 5 a =< b'
21lecon3 157 . . . 4 b =< a'
32lecon 154 . . 3 a'' =< b'
4 oa4to6.oa6.2 . . . . 5 c =< d'
54lecon3 157 . . . 4 d =< c'
65lecon 154 . . 3 c'' =< d'
7 oa4to6.oa6.3 . . . . 5 e =< f'
87lecon3 157 . . . 4 f =< e'
98lecon 154 . . 3 e'' =< f'
10 id 59 . . 3 (((a' ^ b') v (c' ^ d')) v (e' ^ f')) = (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
11 oa4to6.oa4 . . . 4 ((h ->1 g) ^ (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))))) =< g
12 oa4to6.5 . . . . . 6 h = a'
13 oa4to6.4 . . . . . 6 g = (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
1412, 13ud1lem0ab 257 . . . . 5 (h ->1 g) = (a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))
15 oa4to6.6 . . . . . . 7 j = c'
1612, 152an 79 . . . . . . . . 9 (h ^ j) = (a' ^ c')
1715, 13ud1lem0ab 257 . . . . . . . . . 10 (j ->1 g) = (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))
1814, 172an 79 . . . . . . . . 9 ((h ->1 g) ^ (j ->1 g)) = ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))
1916, 182or 72 . . . . . . . 8 ((h ^ j) v ((h ->1 g) ^ (j ->1 g))) = ((a' ^ c') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))))
20 oa4to6.7 . . . . . . . . . . 11 k = e'
2112, 202an 79 . . . . . . . . . 10 (h ^ k) = (a' ^ e')
2220, 13ud1lem0ab 257 . . . . . . . . . . 11 (k ->1 g) = (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))
2314, 222an 79 . . . . . . . . . 10 ((h ->1 g) ^ (k ->1 g)) = ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))
2421, 232or 72 . . . . . . . . 9 ((h ^ k) v ((h ->1 g) ^ (k ->1 g))) = ((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))))
2515, 202an 79 . . . . . . . . . 10 (j ^ k) = (c' ^ e')
2617, 222an 79 . . . . . . . . . 10 ((j ->1 g) ^ (k ->1 g)) = ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))
2725, 262or 72 . . . . . . . . 9 ((j ^ k) v ((j ->1 g) ^ (k ->1 g))) = ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))))
2824, 272an 79 . . . . . . . 8 (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))) = (((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) ^ ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))))
2919, 282or 72 . . . . . . 7 (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g))))) = (((a' ^ c') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) v (((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) ^ ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))))))
3015, 292an 79 . . . . . 6 (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))) = (c' ^ (((a' ^ c') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) v (((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) ^ ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))))))
3112, 302or 72 . . . . 5 (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g))))))) = (a' v (c' ^ (((a' ^ c') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) v (((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) ^ ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))))))))
3214, 312an 79 . . . 4 ((h ->1 g) ^ (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))))) = ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (a' v (c' ^ (((a' ^ c') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) v (((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) ^ ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))))))))
3311, 32, 13le3tr2 141 . . 3 ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (a' v (c' ^ (((a' ^ c') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) v (((a' ^ e') v ((a' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))))) ^ ((c' ^ e') v ((c' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))) ^ (e' ->1 (((a' ^ b') v (c' ^ d')) v (e' ^ f')))))))))) =< (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
343, 6, 9, 10, 33oa4to6dual 964 . 2 (b' ^ (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))) =< (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
3534oa6fromdual 953 1 (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v 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