QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3to4lem6 Unicode version
Theorem oa3to4lem6 950
Description: Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only.
Hypotheses
Ref Expression
oa3to4lem6.oa4.1 a =< b'
oa3to4lem6.oa4.2 c =< d'
oa3to4lem6.3 g = ((a' ^ b') v (c' ^ d'))
oa3to4lem6.4 e = a'
oa3to4lem6.5 f = c'
oa3to4lem6.oa3 (e ^ ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))))) =< ((e ^ g) v (f ^ g))
Assertion
Ref Expression
oa3to4lem6 ((a v b) ^ (c v d)) =< (a v (b ^ (d v ((a v c) ^ (b v d)))))
Proof of Theorem oa3to4lem6
StepHypRef Expression
1 oa3to4lem6.oa4.1 . . . . . 6 a =< b'
21lecon3 157 . . . . 5 b =< a'
32lecon 154 . . . 4 a'' =< b'
4 oa3to4lem6.oa4.2 . . . . . 6 c =< d'
54lecon3 157 . . . . 5 d =< c'
65lecon 154 . . . 4 c'' =< d'
7 id 59 . . . 4 ((a' ^ b') v (c' ^ d')) = ((a' ^ b') v (c' ^ d'))
8 oa3to4lem6.oa3 . . . . 5 (e ^ ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))))) =< ((e ^ g) v (f ^ g))
9 oa3to4lem6.4 . . . . . 6 e = a'
10 oa3to4lem6.3 . . . . . . . 8 g = ((a' ^ b') v (c' ^ d'))
119, 10ud1lem0ab 257 . . . . . . 7 (e ->1 g) = (a' ->1 ((a' ^ b') v (c' ^ d')))
12 oa3to4lem6.5 . . . . . . . . 9 f = c'
1312, 10ud1lem0ab 257 . . . . . . . 8 (f ->1 g) = (c' ->1 ((a' ^ b') v (c' ^ d')))
149, 122an 79 . . . . . . . . 9 (e ^ f) = (a' ^ c')
1511, 132an 79 . . . . . . . . 9 ((e ->1 g) ^ (f ->1 g)) = ((a' ->1 ((a' ^ b') v (c' ^ d'))) ^ (c' ->1 ((a' ^ b') v (c' ^ d'))))
1614, 152or 72 . . . . . . . 8 ((e ^ f) v ((e ->1 g) ^ (f ->1 g))) = ((a' ^ c') v ((a' ->1 ((a' ^ b') v (c' ^ d'))) ^ (c' ->1 ((a' ^ b') v (c' ^ d')))))
1713, 162an 79 . . . . . . 7 ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))) = ((c' ->1 ((a' ^ b') v (c' ^ d'))) ^ ((a' ^ c') v ((a' ->1 ((a' ^ b') v (c' ^ d'))) ^ (c' ->1 ((a' ^ b') v (c' ^ d'))))))
1811, 172or 72 . . . . . 6 ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g))))) = ((a' ->1 ((a' ^ b') v (c' ^ d'))) v ((c' ->1 ((a' ^ b') v (c' ^ d'))) ^ ((a' ^ c') v ((a' ->1 ((a' ^ b') v (c' ^ d'))) ^ (c' ->1 ((a' ^ b') v (c' ^ d')))))))
199, 182an 79 . . . . 5 (e ^ ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))))) = (a' ^ ((a' ->1 ((a' ^ b') v (c' ^ d'))) v ((c' ->1 ((a' ^ b') v (c' ^ d'))) ^ ((a' ^ c') v ((a' ->1 ((a' ^ b') v (c' ^ d'))) ^ (c' ->1 ((a' ^ b') v (c' ^ d'))))))))
209, 102an 79 . . . . . 6 (e ^ g) = (a' ^ ((a' ^ b') v (c' ^ d')))
2112, 102an 79 . . . . . 6 (f ^ g) = (c' ^ ((a' ^ b') v (c' ^ d')))
2220, 212or 72 . . . . 5 ((e ^ g) v (f ^ g)) = ((a' ^ ((a' ^ b') v (c' ^ d'))) v (c' ^ ((a' ^ b') v (c' ^ d'))))
238, 19, 22le3tr2 141 . . . 4 (a' ^ ((a' ->1 ((a' ^ b') v (c' ^ d'))) v ((c' ->1 ((a' ^ b') v (c' ^ d'))) ^ ((a' ^ c') v ((a' ->1 ((a' ^ b') v (c' ^ d'))) ^ (c' ->1 ((a' ^ b') v (c' ^ d')))))))) =< ((a' ^ ((a' ^ b') v (c' ^ d'))) v (c' ^ ((a' ^ b') v (c' ^ d'))))
243, 6, 7, 23oa3to4lem4 948 . . 3 (a' ^ (b' v (d' ^ ((a' ^ c') v (b' ^ d'))))) =< ((a' ^ b') v (c' ^ d'))
25 anor3 90 . . . . . . . . . . 11 (a' ^ c') = (a v c)'
26 anor3 90 . . . . . . . . . . 11 (b' ^ d') = (b v d)'
2725, 262or 72 . . . . . . . . . 10 ((a' ^ c') v (b' ^ d')) = ((a v c)' v (b v d)')
28 oran3 93 . . . . . . . . . 10 ((a v c)' v (b v d)') = ((a v c) ^ (b v d))'
2927, 28ax-r2 36 . . . . . . . . 9 ((a' ^ c') v (b' ^ d')) = ((a v c) ^ (b v d))'
3029lan 77 . . . . . . . 8 (d' ^ ((a' ^ c') v (b' ^ d'))) = (d' ^ ((a v c) ^ (b v d))')
31 anor3 90 . . . . . . . 8 (d' ^ ((a v c) ^ (b v d))') = (d v ((a v c) ^ (b v d)))'
3230, 31ax-r2 36 . . . . . . 7 (d' ^ ((a' ^ c') v (b' ^ d'))) = (d v ((a v c) ^ (b v d)))'
3332lor 70 . . . . . 6 (b' v (d' ^ ((a' ^ c') v (b' ^ d')))) = (b' v (d v ((a v c) ^ (b v d)))')
34 oran3 93 . . . . . 6 (b' v (d v ((a v c) ^ (b v d)))') = (b ^ (d v ((a v c) ^ (b v d))))'
3533, 34ax-r2 36 . . . . 5 (b' v (d' ^ ((a' ^ c') v (b' ^ d')))) = (b ^ (d v ((a v c) ^ (b v d))))'
3635lan 77 . . . 4 (a' ^ (b' v (d' ^ ((a' ^ c') v (b' ^ d'))))) = (a' ^ (b ^ (d v ((a v c) ^ (b v d))))')
37 anor3 90 . . . 4 (a' ^ (b ^ (d v ((a v c) ^ (b v d))))') = (a v (b ^ (d v ((a v c) ^ (b v d)))))'
3836, 37ax-r2 36 . . 3 (a' ^ (b' v (d' ^ ((a' ^ c') v (b' ^ d'))))) = (a v (b ^ (d v ((a v c) ^ (b v d)))))'
39 anor3 90 . . . . 5 (a' ^ b') = (a v b)'
40 anor3 90 . . . . 5 (c' ^ d') = (c v d)'
4139, 402or 72 . . . 4 ((a' ^ b') v (c' ^ d')) = ((a v b)' v (c v d)')
42 oran3 93 . . . 4 ((a v b)' v (c v d)') = ((a v b) ^ (c v d))'
4341, 42ax-r2 36 . . 3 ((a' ^ b') v (c' ^ d')) = ((a v b) ^ (c v d))'
4424, 38, 43le3tr2 141 . 2 (a v (b ^ (d v ((a v c) ^ (b v d)))))' =< ((a v b) ^ (c v d))'
4544lecon1 155 1 ((a v b) ^ (c v d)) =< (a v (b ^ (d v ((a v c) ^ (b v d)))))
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:  oa3to4  951
  Copyright terms: Public domain W3C validator