QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  e2ast2 Unicode version
Theorem e2ast2 894
Description: Show that the E*2 derivative on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs.
Hypotheses
Ref Expression
e2ast2.1 a =< b'
e2ast2.2 c =< d'
e2ast2.3 a =< c'
Assertion
Ref Expression
e2ast2 ((a v b) ^ (c v d)) =< ((b v d) v (a v c)')
Proof of Theorem e2ast2
StepHypRef Expression
1 e2ast2.3 . . . 4 a =< c'
21leror 152 . . 3 (a v b) =< (c' v b)
31lecon3 157 . . . 4 c =< a'
43leror 152 . . 3 (c v d) =< (a' v d)
52, 4le2an 169 . 2 ((a v b) ^ (c v d)) =< ((c' v b) ^ (a' v d))
6 e2ast2.2 . . . . . . . . . . 11 c =< d'
76lecon3 157 . . . . . . . . . 10 d =< c'
87lecom 180 . . . . . . . . 9 d C c'
98comcom 453 . . . . . . . 8 c' C d
101lecom 180 . . . . . . . . . 10 a C c'
1110comcom 453 . . . . . . . . 9 c' C a
1211comcom2 183 . . . . . . . 8 c' C a'
139, 12fh4c 478 . . . . . . 7 (d v (a' ^ c')) = ((d v a') ^ (d v c'))
147df-le2 131 . . . . . . . 8 (d v c') = c'
1514lan 77 . . . . . . 7 ((d v a') ^ (d v c')) = ((d v a') ^ c')
1613, 15ax-r2 36 . . . . . 6 (d v (a' ^ c')) = ((d v a') ^ c')
1716ax-r1 35 . . . . 5 ((d v a') ^ c') = (d v (a' ^ c'))
18 anor3 90 . . . . . 6 (a' ^ c') = (a v c)'
1918lor 70 . . . . 5 (d v (a' ^ c')) = (d v (a v c)')
2017, 19ax-r2 36 . . . 4 ((d v a') ^ c') = (d v (a v c)')
2120lor 70 . . 3 (b v ((d v a') ^ c')) = (b v (d v (a v c)'))
22 leao4 165 . . . . . . . . 9 (b ^ a') =< (d v a')
2322lecom 180 . . . . . . . 8 (b ^ a') C (d v a')
2423comcom 453 . . . . . . 7 (d v a') C (b ^ a')
259, 12com2or 483 . . . . . . . 8 c' C (d v a')
2625comcom 453 . . . . . . 7 (d v a') C c'
2724, 26fh4 472 . . . . . 6 ((b ^ a') v ((d v a') ^ c')) = (((b ^ a') v (d v a')) ^ ((b ^ a') v c'))
28 or32 82 . . . . . . . 8 (((b ^ a') v d) v a') = (((b ^ a') v a') v d)
29 ax-a3 32 . . . . . . . 8 (((b ^ a') v d) v a') = ((b ^ a') v (d v a'))
30 lear 161 . . . . . . . . . 10 (b ^ a') =< a'
3130df-le2 131 . . . . . . . . 9 ((b ^ a') v a') = a'
3231ax-r5 38 . . . . . . . 8 (((b ^ a') v a') v d) = (a' v d)
3328, 29, 323tr2 64 . . . . . . 7 ((b ^ a') v (d v a')) = (a' v d)
34 e2ast2.1 . . . . . . . . . . 11 a =< b'
3534lecon3 157 . . . . . . . . . 10 b =< a'
3635df2le2 136 . . . . . . . . 9 (b ^ a') = b
3736ax-r5 38 . . . . . . . 8 ((b ^ a') v c') = (b v c')
38 ax-a2 31 . . . . . . . 8 (b v c') = (c' v b)
3937, 38ax-r2 36 . . . . . . 7 ((b ^ a') v c') = (c' v b)
4033, 392an 79 . . . . . 6 (((b ^ a') v (d v a')) ^ ((b ^ a') v c')) = ((a' v d) ^ (c' v b))
41 ancom 74 . . . . . 6 ((a' v d) ^ (c' v b)) = ((c' v b) ^ (a' v d))
4227, 40, 413tr 65 . . . . 5 ((b ^ a') v ((d v a') ^ c')) = ((c' v b) ^ (a' v d))
4342ax-r1 35 . . . 4 ((c' v b) ^ (a' v d)) = ((b ^ a') v ((d v a') ^ c'))
4436ax-r5 38 . . . 4 ((b ^ a') v ((d v a') ^ c')) = (b v ((d v a') ^ c'))
4543, 44ax-r2 36 . . 3 ((c' v b) ^ (a' v d)) = (b v ((d v a') ^ c'))
46 ax-a3 32 . . 3 ((b v d) v (a v c)') = (b v (d v (a v c)'))
4721, 45, 463tr1 63 . 2 ((c' v b) ^ (a' v d)) = ((b v d) v (a v c)')
485, 47lbtr 139 1 ((a v b) ^ (c v d)) =< ((b v d) v (a v c)')
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7
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