Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  e2ast2 GIF 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 ab
e2ast2.2 cd
e2ast2.3 ac
Assertion
Ref Expression
e2ast2 ((ab) ∩ (cd)) ≤ ((bd) ∪ (ac) )

Proof of Theorem e2ast2
StepHypRef Expression
1 e2ast2.3 . . . 4 ac
21leror 152 . . 3 (ab) ≤ (cb)
31lecon3 157 . . . 4 ca
43leror 152 . . 3 (cd) ≤ (ad)
52, 4le2an 169 . 2 ((ab) ∩ (cd)) ≤ ((cb) ∩ (ad))
6 e2ast2.2 . . . . . . . . . . 11 cd
76lecon3 157 . . . . . . . . . 10 dc
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 ∪ (ac )) = ((da ) ∩ (dc ))
147df-le2 131 . . . . . . . 8 (dc ) = c
1514lan 77 . . . . . . 7 ((da ) ∩ (dc )) = ((da ) ∩ c )
1613, 15ax-r2 36 . . . . . 6 (d ∪ (ac )) = ((da ) ∩ c )
1716ax-r1 35 . . . . 5 ((da ) ∩ c ) = (d ∪ (ac ))
18 anor3 90 . . . . . 6 (ac ) = (ac)
1918lor 70 . . . . 5 (d ∪ (ac )) = (d ∪ (ac) )
2017, 19ax-r2 36 . . . 4 ((da ) ∩ c ) = (d ∪ (ac) )
2120lor 70 . . 3 (b ∪ ((da ) ∩ c )) = (b ∪ (d ∪ (ac) ))
22 leao4 165 . . . . . . . . 9 (ba ) ≤ (da )
2322lecom 180 . . . . . . . 8 (ba ) C (da )
2423comcom 453 . . . . . . 7 (da ) C (ba )
259, 12com2or 483 . . . . . . . 8 c C (da )
2625comcom 453 . . . . . . 7 (da ) C c
2724, 26fh4 472 . . . . . 6 ((ba ) ∪ ((da ) ∩ c )) = (((ba ) ∪ (da )) ∩ ((ba ) ∪ c ))
28 or32 82 . . . . . . . 8 (((ba ) ∪ d) ∪ a ) = (((ba ) ∪ a ) ∪ d)
29 ax-a3 32 . . . . . . . 8 (((ba ) ∪ d) ∪ a ) = ((ba ) ∪ (da ))
30 lear 161 . . . . . . . . . 10 (ba ) ≤ a
3130df-le2 131 . . . . . . . . 9 ((ba ) ∪ a ) = a
3231ax-r5 38 . . . . . . . 8 (((ba ) ∪ a ) ∪ d) = (ad)
3328, 29, 323tr2 64 . . . . . . 7 ((ba ) ∪ (da )) = (ad)
34 e2ast2.1 . . . . . . . . . . 11 ab
3534lecon3 157 . . . . . . . . . 10 ba
3635df2le2 136 . . . . . . . . 9 (ba ) = b
3736ax-r5 38 . . . . . . . 8 ((ba ) ∪ c ) = (bc )
38 ax-a2 31 . . . . . . . 8 (bc ) = (cb)
3937, 38ax-r2 36 . . . . . . 7 ((ba ) ∪ c ) = (cb)
4033, 392an 79 . . . . . 6 (((ba ) ∪ (da )) ∩ ((ba ) ∪ c )) = ((ad) ∩ (cb))
41 ancom 74 . . . . . 6 ((ad) ∩ (cb)) = ((cb) ∩ (ad))
4227, 40, 413tr 65 . . . . 5 ((ba ) ∪ ((da ) ∩ c )) = ((cb) ∩ (ad))
4342ax-r1 35 . . . 4 ((cb) ∩ (ad)) = ((ba ) ∪ ((da ) ∩ c ))
4436ax-r5 38 . . . 4 ((ba ) ∪ ((da ) ∩ c )) = (b ∪ ((da ) ∩ c ))
4543, 44ax-r2 36 . . 3 ((cb) ∩ (ad)) = (b ∪ ((da ) ∩ c ))
46 ax-a3 32 . . 3 ((bd) ∪ (ac) ) = (b ∪ (d ∪ (ac) ))
4721, 45, 463tr1 63 . 2 ((cb) ∩ (ad)) = ((bd) ∪ (ac) )
485, 47lbtr 139 1 ((ab) ∩ (cd)) ≤ ((bd) ∪ (ac) )
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ wn 4   ∪ 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