Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  e2astlem1 GIF 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 ab
e2ast.2 cd
e2ast.3 ra
e2ast.4 ac
e2ast.5 cr
Assertion
Ref Expression
e2astlem1 (((ab) ∩ (cd)) ∩ ((ac) ∪ r)) = ((a ∪ (b ∩ (cr))) ∩ (c ∪ (d ∩ (ar))))

Proof of Theorem e2astlem1
StepHypRef Expression
1 anandir 115 . 2 (((ab) ∩ (cd)) ∩ ((ac) ∪ r)) = (((ab) ∩ ((ac) ∪ r)) ∩ ((cd) ∩ ((ac) ∪ r)))
2 leo 158 . . . . . . 7 a ≤ (ac)
32ler 149 . . . . . 6 a ≤ ((ac) ∪ r)
43lecom 180 . . . . 5 a C ((ac) ∪ r)
5 e2ast.1 . . . . . . 7 ab
65lecom 180 . . . . . 6 a C b
76comcom7 460 . . . . 5 a C b
84, 7fh2r 474 . . . 4 ((ab) ∩ ((ac) ∪ r)) = ((a ∩ ((ac) ∪ r)) ∪ (b ∩ ((ac) ∪ r)))
93df2le2 136 . . . . 5 (a ∩ ((ac) ∪ r)) = a
10 ax-a3 32 . . . . . . 7 ((ac) ∪ r) = (a ∪ (cr))
1110lan 77 . . . . . 6 (b ∩ ((ac) ∪ r)) = (b ∩ (a ∪ (cr)))
12 e2ast.4 . . . . . . . . . . 11 ac
1312lecom 180 . . . . . . . . . 10 a C c
1413comcom7 460 . . . . . . . . 9 a C c
15 e2ast.3 . . . . . . . . . . . 12 ra
1615lecom 180 . . . . . . . . . . 11 r C a
1716comcom7 460 . . . . . . . . . 10 r C a
1817comcom 453 . . . . . . . . 9 a C r
1914, 18com2or 483 . . . . . . . 8 a C (cr)
207, 19fh2 470 . . . . . . 7 (b ∩ (a ∪ (cr))) = ((ba) ∪ (b ∩ (cr)))
215lecon3 157 . . . . . . . . 9 ba
2221ortha 438 . . . . . . . 8 (ba) = 0
2322ax-r5 38 . . . . . . 7 ((ba) ∪ (b ∩ (cr))) = (0 ∪ (b ∩ (cr)))
2420, 23ax-r2 36 . . . . . 6 (b ∩ (a ∪ (cr))) = (0 ∪ (b ∩ (cr)))
25 or0r 103 . . . . . 6 (0 ∪ (b ∩ (cr))) = (b ∩ (cr))
2611, 24, 253tr 65 . . . . 5 (b ∩ ((ac) ∪ r)) = (b ∩ (cr))
279, 262or 72 . . . 4 ((a ∩ ((ac) ∪ r)) ∪ (b ∩ ((ac) ∪ r))) = (a ∪ (b ∩ (cr)))
288, 27ax-r2 36 . . 3 ((ab) ∩ ((ac) ∪ r)) = (a ∪ (b ∩ (cr)))
29 leor 159 . . . . . . 7 c ≤ (ac)
3029ler 149 . . . . . 6 c ≤ ((ac) ∪ r)
3130lecom 180 . . . . 5 c C ((ac) ∪ r)
32 e2ast.2 . . . . . . 7 cd
3332lecom 180 . . . . . 6 c C d
3433comcom7 460 . . . . 5 c C d
3531, 34fh2r 474 . . . 4 ((cd) ∩ ((ac) ∪ r)) = ((c ∩ ((ac) ∪ r)) ∪ (d ∩ ((ac) ∪ r)))
3630df2le2 136 . . . . 5 (c ∩ ((ac) ∪ r)) = c
37 or32 82 . . . . . . 7 ((ac) ∪ r) = ((ar) ∪ c)
3837lan 77 . . . . . 6 (d ∩ ((ac) ∪ r)) = (d ∩ ((ar) ∪ c))
3914comcom 453 . . . . . . . 8 c C a
40 e2ast.5 . . . . . . . . . 10 cr
4140lecom 180 . . . . . . . . 9 c C r
4241comcom7 460 . . . . . . . 8 c C r
4339, 42com2or 483 . . . . . . 7 c C (ar)
4434, 43fh2c 477 . . . . . 6 (d ∩ ((ar) ∪ c)) = ((d ∩ (ar)) ∪ (dc))
4532lecon3 157 . . . . . . . . 9 dc
4645ortha 438 . . . . . . . 8 (dc) = 0
4746lor 70 . . . . . . 7 ((d ∩ (ar)) ∪ (dc)) = ((d ∩ (ar)) ∪ 0)
48 or0 102 . . . . . . 7 ((d ∩ (ar)) ∪ 0) = (d ∩ (ar))
4947, 48ax-r2 36 . . . . . 6 ((d ∩ (ar)) ∪ (dc)) = (d ∩ (ar))
5038, 44, 493tr 65 . . . . 5 (d ∩ ((ac) ∪ r)) = (d ∩ (ar))
5136, 502or 72 . . . 4 ((c ∩ ((ac) ∪ r)) ∪ (d ∩ ((ac) ∪ r))) = (c ∪ (d ∩ (ar)))
5235, 51ax-r2 36 . . 3 ((cd) ∩ ((ac) ∪ r)) = (c ∪ (d ∩ (ar)))
5328, 522an 79 . 2 (((ab) ∩ ((ac) ∪ r)) ∩ ((cd) ∩ ((ac) ∪ r))) = ((a ∪ (b ∩ (cr))) ∩ (c ∪ (d ∩ (ar))))
541, 53ax-r2 36 1 (((ab) ∩ (cd)) ∩ ((ac) ∪ r)) = ((a ∪ (b ∩ (cr))) ∩ (c ∪ (d ∩ (ar))))
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2  ⊥ wn 4   ∪ 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