QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  mlaconjo GIF version

Theorem mlaconjo 886
Description: OML proof of Mladen's conjecture. (Contributed by NM, 10-Mar-2002.)
Assertion
Ref Expression
mlaconjo ((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)

Proof of Theorem mlaconjo
StepHypRef Expression
1 dfb 94 . . . 4 (ab) = ((ab) ∪ (ab ))
21bile 142 . . 3 (ab) ≤ ((ab) ∪ (ab ))
3 mlaconjolem 885 . . 3 ((ac) ∪ (bc)) ≤ ((c ∩ (ab)) ∪ (c ∩ (ab )))
42, 3le2an 169 . 2 ((ab) ∩ ((ac) ∪ (bc))) ≤ (((ab) ∪ (ab )) ∩ ((c ∩ (ab)) ∪ (c ∩ (ab ))))
5 lea 160 . . . . 5 (ab) ≤ a
6 lea 160 . . . . 5 (c ∩ (ab)) ≤ c
75, 6le2an 169 . . . 4 ((ab) ∩ (c ∩ (ab))) ≤ (ac)
8 lea 160 . . . . 5 (ab ) ≤ a
9 lea 160 . . . . 5 (c ∩ (ab )) ≤ c
108, 9le2an 169 . . . 4 ((ab ) ∩ (c ∩ (ab ))) ≤ (ac )
117, 10le2or 168 . . 3 (((ab) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab )))) ≤ ((ac) ∪ (ac ))
12 leao1 162 . . . . . . . 8 (ab) ≤ (ab)
13 oran 87 . . . . . . . 8 (ab) = (ab )
1412, 13lbtr 139 . . . . . . 7 (ab) ≤ (ab )
1514lecom 180 . . . . . 6 (ab) C (ab )
1615comcom7 460 . . . . 5 (ab) C (ab )
17 leor 159 . . . . . . . 8 (ab) ≤ (c ∪ (ab))
18 df-a 40 . . . . . . . . . 10 (ab) = (ab )
1918lor 70 . . . . . . . . 9 (c ∪ (ab)) = (c ∪ (ab ) )
20 oran1 91 . . . . . . . . 9 (c ∪ (ab ) ) = (c ∩ (ab ))
2119, 20ax-r2 36 . . . . . . . 8 (c ∪ (ab)) = (c ∩ (ab ))
2217, 21lbtr 139 . . . . . . 7 (ab) ≤ (c ∩ (ab ))
2322lecom 180 . . . . . 6 (ab) C (c ∩ (ab ))
2423comcom7 460 . . . . 5 (ab) C (c ∩ (ab ))
25 lear 161 . . . . . . . 8 (c ∩ (ab)) ≤ (ab)
2625, 13lbtr 139 . . . . . . 7 (c ∩ (ab)) ≤ (ab )
2726lecom 180 . . . . . 6 (c ∩ (ab)) C (ab )
2827comcom7 460 . . . . 5 (c ∩ (ab)) C (ab )
29 leao1 162 . . . . . . . 8 (c ∩ (ab)) ≤ (c ∪ (ab ) )
3029, 20lbtr 139 . . . . . . 7 (c ∩ (ab)) ≤ (c ∩ (ab ))
3130lecom 180 . . . . . 6 (c ∩ (ab)) C (c ∩ (ab ))
3231comcom7 460 . . . . 5 (c ∩ (ab)) C (c ∩ (ab ))
3316, 24, 28, 32mh 879 . . . 4 (((ab) ∪ (ab )) ∩ ((c ∩ (ab)) ∪ (c ∩ (ab )))) = ((((ab) ∩ (c ∩ (ab))) ∪ ((ab) ∩ (c ∩ (ab )))) ∪ (((ab ) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab )))))
34 an12 81 . . . . . . . 8 ((ab) ∩ (c ∩ (ab ))) = (c ∩ ((ab) ∩ (ab )))
35 oran3 93 . . . . . . . . . . 11 (ab ) = (ab)
3635lan 77 . . . . . . . . . 10 ((ab) ∩ (ab )) = ((ab) ∩ (ab) )
37 dff 101 . . . . . . . . . . 11 0 = ((ab) ∩ (ab) )
3837ax-r1 35 . . . . . . . . . 10 ((ab) ∩ (ab) ) = 0
3936, 38ax-r2 36 . . . . . . . . 9 ((ab) ∩ (ab )) = 0
4039lan 77 . . . . . . . 8 (c ∩ ((ab) ∩ (ab ))) = (c ∩ 0)
41 an0 108 . . . . . . . 8 (c ∩ 0) = 0
4234, 40, 413tr 65 . . . . . . 7 ((ab) ∩ (c ∩ (ab ))) = 0
4342lor 70 . . . . . 6 (((ab) ∩ (c ∩ (ab))) ∪ ((ab) ∩ (c ∩ (ab )))) = (((ab) ∩ (c ∩ (ab))) ∪ 0)
44 or0 102 . . . . . 6 (((ab) ∩ (c ∩ (ab))) ∪ 0) = ((ab) ∩ (c ∩ (ab)))
4543, 44ax-r2 36 . . . . 5 (((ab) ∩ (c ∩ (ab))) ∪ ((ab) ∩ (c ∩ (ab )))) = ((ab) ∩ (c ∩ (ab)))
46 an12 81 . . . . . . . 8 ((ab ) ∩ (c ∩ (ab))) = (c ∩ ((ab ) ∩ (ab)))
4713lan 77 . . . . . . . . . 10 ((ab ) ∩ (ab)) = ((ab ) ∩ (ab ) )
48 dff 101 . . . . . . . . . . 11 0 = ((ab ) ∩ (ab ) )
4948ax-r1 35 . . . . . . . . . 10 ((ab ) ∩ (ab ) ) = 0
5047, 49ax-r2 36 . . . . . . . . 9 ((ab ) ∩ (ab)) = 0
5150lan 77 . . . . . . . 8 (c ∩ ((ab ) ∩ (ab))) = (c ∩ 0)
52 an0 108 . . . . . . . 8 (c ∩ 0) = 0
5346, 51, 523tr 65 . . . . . . 7 ((ab ) ∩ (c ∩ (ab))) = 0
5453ax-r5 38 . . . . . 6 (((ab ) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab )))) = (0 ∪ ((ab ) ∩ (c ∩ (ab ))))
55 or0r 103 . . . . . 6 (0 ∪ ((ab ) ∩ (c ∩ (ab )))) = ((ab ) ∩ (c ∩ (ab )))
5654, 55ax-r2 36 . . . . 5 (((ab ) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab )))) = ((ab ) ∩ (c ∩ (ab )))
5745, 562or 72 . . . 4 ((((ab) ∩ (c ∩ (ab))) ∪ ((ab) ∩ (c ∩ (ab )))) ∪ (((ab ) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab ))))) = (((ab) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab ))))
5833, 57ax-r2 36 . . 3 (((ab) ∪ (ab )) ∩ ((c ∩ (ab)) ∪ (c ∩ (ab )))) = (((ab) ∩ (c ∩ (ab))) ∪ ((ab ) ∩ (c ∩ (ab ))))
59 dfb 94 . . 3 (ac) = ((ac) ∪ (ac ))
6011, 58, 59le3tr1 140 . 2 (((ab) ∪ (ab )) ∩ ((c ∩ (ab)) ∪ (c ∩ (ab )))) ≤ (ac)
614, 60letr 137 1 ((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)
Colors of variables: term
Syntax hints:  wle 2   wn 4  tb 5  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-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  distid  887
  Copyright terms: Public domain W3C validator