QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  e2astlem1 Unicode version
Theorem e2astlem1 895
Description: Lemma towards a possible proof that E*2 on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs.
Hypotheses
Ref Expression
e2ast.1 a =< b'
e2ast.2 c =< d'
e2ast.3 r =< a'
e2ast.4 a =< c'
e2ast.5 c =< r'
Assertion
Ref Expression
e2astlem1 (((a v b) ^ (c v d)) ^ ((a v c) v r)) = ((a v (b ^ (c v r))) ^ (c v (d ^ (a v r))))
Proof of Theorem e2astlem1
StepHypRef Expression
1 anandir 115 . 2 (((a v b) ^ (c v d)) ^ ((a v c) v r)) = (((a v b) ^ ((a v c) v r)) ^ ((c v d) ^ ((a v c) v r)))
2 leo 158 . . . . . . 7 a =< (a v c)
32ler 149 . . . . . 6 a =< ((a v c) v r)
43lecom 180 . . . . 5 a C ((a v c) v r)
5 e2ast.1 . . . . . . 7 a =< b'
65lecom 180 . . . . . 6 a C b'
76comcom7 460 . . . . 5 a C b
84, 7fh2r 474 . . . 4 ((a v b) ^ ((a v c) v r)) = ((a ^ ((a v c) v r)) v (b ^ ((a v c) v r)))
93df2le2 136 . . . . 5 (a ^ ((a v c) v r)) = a
10 ax-a3 32 . . . . . . 7 ((a v c) v r) = (a v (c v r))
1110lan 77 . . . . . 6 (b ^ ((a v c) v r)) = (b ^ (a v (c v r)))
12 e2ast.4 . . . . . . . . . . 11 a =< c'
1312lecom 180 . . . . . . . . . 10 a C c'
1413comcom7 460 . . . . . . . . 9 a C c
15 e2ast.3 . . . . . . . . . . . 12 r =< a'
1615lecom 180 . . . . . . . . . . 11 r C a'
1716comcom7 460 . . . . . . . . . 10 r C a
1817comcom 453 . . . . . . . . 9 a C r
1914, 18com2or 483 . . . . . . . 8 a C (c v r)
207, 19fh2 470 . . . . . . 7 (b ^ (a v (c v r))) = ((b ^ a) v (b ^ (c v r)))
215lecon3 157 . . . . . . . . 9 b =< a'
2221ortha 438 . . . . . . . 8 (b ^ a) = 0
2322ax-r5 38 . . . . . . 7 ((b ^ a) v (b ^ (c v r))) = (0 v (b ^ (c v r)))
2420, 23ax-r2 36 . . . . . 6 (b ^ (a v (c v r))) = (0 v (b ^ (c v r)))
25 or0r 103 . . . . . 6 (0 v (b ^ (c v r))) = (b ^ (c v r))
2611, 24, 253tr 65 . . . . 5 (b ^ ((a v c) v r)) = (b ^ (c v r))
279, 262or 72 . . . 4 ((a ^ ((a v c) v r)) v (b ^ ((a v c) v r))) = (a v (b ^ (c v r)))
288, 27ax-r2 36 . . 3 ((a v b) ^ ((a v c) v r)) = (a v (b ^ (c v r)))
29 leor 159 . . . . . . 7 c =< (a v c)
3029ler 149 . . . . . 6 c =< ((a v c) v r)
3130lecom 180 . . . . 5 c C ((a v c) v r)
32 e2ast.2 . . . . . . 7 c =< d'
3332lecom 180 . . . . . 6 c C d'
3433comcom7 460 . . . . 5 c C d
3531, 34fh2r 474 . . . 4 ((c v d) ^ ((a v c) v r)) = ((c ^ ((a v c) v r)) v (d ^ ((a v c) v r)))
3630df2le2 136 . . . . 5 (c ^ ((a v c) v r)) = c
37 or32 82 . . . . . . 7 ((a v c) v r) = ((a v r) v c)
3837lan 77 . . . . . 6 (d ^ ((a v c) v r)) = (d ^ ((a v r) v c))
3914comcom 453 . . . . . . . 8 c C a
40 e2ast.5 . . . . . . . . . 10 c =< r'
4140lecom 180 . . . . . . . . 9 c C r'
4241comcom7 460 . . . . . . . 8 c C r
4339, 42com2or 483 . . . . . . 7 c C (a v r)
4434, 43fh2c 477 . . . . . 6 (d ^ ((a v r) v c)) = ((d ^ (a v r)) v (d ^ c))
4532lecon3 157 . . . . . . . . 9 d =< c'
4645ortha 438 . . . . . . . 8 (d ^ c) = 0
4746lor 70 . . . . . . 7 ((d ^ (a v r)) v (d ^ c)) = ((d ^ (a v r)) v 0)
48 or0 102 . . . . . . 7 ((d ^ (a v r)) v 0) = (d ^ (a v r))
4947, 48ax-r2 36 . . . . . 6 ((d ^ (a v r)) v (d ^ c)) = (d ^ (a v r))
5038, 44, 493tr 65 . . . . 5 (d ^ ((a v c) v r)) = (d ^ (a v r))
5136, 502or 72 . . . 4 ((c ^ ((a v c) v r)) v (d ^ ((a v c) v r))) = (c v (d ^ (a v r)))
5235, 51ax-r2 36 . . 3 ((c v d) ^ ((a v c) v r)) = (c v (d ^ (a v r)))
5328, 522an 79 . 2 (((a v b) ^ ((a v c) v r)) ^ ((c v d) ^ ((a v c) v r))) = ((a v (b ^ (c v r))) ^ (c v (d ^ (a v r))))
541, 53ax-r2 36 1 (((a v b) ^ (c v d)) ^ ((a v c) v r)) = ((a v (b ^ (c v r))) ^ (c v (d ^ (a v r))))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7  0wf 9
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator