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

Theorem mlaconj4 844
Description: For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper. (Contributed by NM, 8-Jul-2000.)
Hypotheses
Ref Expression
mlaconj4.1 ((de) ∩ ((ec ) ∪ (dc))) ≤ (dc)
mlaconj4.2 d = (ab)
mlaconj4.3 e = (ab)
Assertion
Ref Expression
mlaconj4 ((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)

Proof of Theorem mlaconj4
StepHypRef Expression
1 biao 799 . . . . 5 (ab) = ((ab) ≡ (ab))
2 bicom 96 . . . . 5 ((ab) ≡ (ab)) = ((ab) ≡ (ab))
31, 2ax-r2 36 . . . 4 (ab) = ((ab) ≡ (ab))
43bile 142 . . 3 (ab) ≤ ((ab) ≡ (ab))
5 orbile 843 . . . 4 ((ac) ∪ (bc)) ≤ (((ab) →2 c) ∩ (c1 (ab)))
6 imp3 841 . . . 4 (((ab) →2 c) ∩ (c1 (ab))) = (((ab)c ) ∪ (c ∩ (ab)))
75, 6lbtr 139 . . 3 ((ac) ∪ (bc)) ≤ (((ab)c ) ∪ (c ∩ (ab)))
84, 7le2an 169 . 2 ((ab) ∩ ((ac) ∪ (bc))) ≤ (((ab) ≡ (ab)) ∩ (((ab)c ) ∪ (c ∩ (ab))))
9 mlaconj4.2 . . . . . 6 d = (ab)
10 mlaconj4.3 . . . . . 6 e = (ab)
119, 102bi 99 . . . . 5 (de) = ((ab) ≡ (ab))
1210ax-r4 37 . . . . . . 7 e = (ab)
1312ran 78 . . . . . 6 (ec ) = ((ab)c )
14 ancom 74 . . . . . . 7 (dc) = (cd)
159lan 77 . . . . . . 7 (cd) = (c ∩ (ab))
1614, 15ax-r2 36 . . . . . 6 (dc) = (c ∩ (ab))
1713, 162or 72 . . . . 5 ((ec ) ∪ (dc)) = (((ab)c ) ∪ (c ∩ (ab)))
1811, 172an 79 . . . 4 ((de) ∩ ((ec ) ∪ (dc))) = (((ab) ≡ (ab)) ∩ (((ab)c ) ∪ (c ∩ (ab))))
1918ax-r1 35 . . 3 (((ab) ≡ (ab)) ∩ (((ab)c ) ∪ (c ∩ (ab)))) = ((de) ∩ ((ec ) ∪ (dc)))
20 lea 160 . . . . . 6 ((de) ∩ ((ec ) ∪ (dc))) ≤ (de)
21 bicom 96 . . . . . . 7 ((ab) ≡ (ab)) = ((ab) ≡ (ab))
2221, 11, 13tr1 63 . . . . . 6 (de) = (ab)
2320, 22lbtr 139 . . . . 5 ((de) ∩ ((ec ) ∪ (dc))) ≤ (ab)
24 mlaconj4.1 . . . . . 6 ((de) ∩ ((ec ) ∪ (dc))) ≤ (dc)
259rbi 98 . . . . . 6 (dc) = ((ab) ≡ c)
2624, 25lbtr 139 . . . . 5 ((de) ∩ ((ec ) ∪ (dc))) ≤ ((ab) ≡ c)
2723, 26ler2an 173 . . . 4 ((de) ∩ ((ec ) ∪ (dc))) ≤ ((ab) ∩ ((ab) ≡ c))
28 anass 76 . . . . . . . . . . 11 ((ab ) ∩ c ) = (a ∩ (bc ))
29 coman1 185 . . . . . . . . . . . 12 (a ∩ (bc )) C a
3029comcom7 460 . . . . . . . . . . 11 (a ∩ (bc )) C a
3128, 30bctr 181 . . . . . . . . . 10 ((ab ) ∩ c ) C a
32 an32 83 . . . . . . . . . . 11 ((ab ) ∩ c ) = ((ac ) ∩ b )
33 coman2 186 . . . . . . . . . . . 12 ((ac ) ∩ b ) C b
3433comcom7 460 . . . . . . . . . . 11 ((ac ) ∩ b ) C b
3532, 34bctr 181 . . . . . . . . . 10 ((ab ) ∩ c ) C b
3631, 35com2an 484 . . . . . . . . 9 ((ab ) ∩ c ) C (ab)
37 coman1 185 . . . . . . . . 9 ((ab ) ∩ c ) C (ab )
3836, 37com2or 483 . . . . . . . 8 ((ab ) ∩ c ) C ((ab) ∪ (ab ))
3931, 35com2or 483 . . . . . . . . 9 ((ab ) ∩ c ) C (ab)
40 coman2 186 . . . . . . . . . 10 ((ab ) ∩ c ) C c
4140comcom7 460 . . . . . . . . 9 ((ab ) ∩ c ) C c
4239, 41com2an 484 . . . . . . . 8 ((ab ) ∩ c ) C ((ab) ∩ c)
4338, 42fh2c 477 . . . . . . 7 (((ab) ∪ (ab )) ∩ (((ab) ∩ c) ∪ ((ab ) ∩ c ))) = ((((ab) ∪ (ab )) ∩ ((ab) ∩ c)) ∪ (((ab) ∪ (ab )) ∩ ((ab ) ∩ c )))
44 anor3 90 . . . . . . . . . . 11 (ab ) = (ab)
45 comanr1 464 . . . . . . . . . . . 12 (ab) C ((ab) ∩ c)
4645comcom3 454 . . . . . . . . . . 11 (ab) C ((ab) ∩ c)
4744, 46bctr 181 . . . . . . . . . 10 (ab ) C ((ab) ∩ c)
48 coman1 185 . . . . . . . . . . . 12 (ab ) C a
4948comcom7 460 . . . . . . . . . . 11 (ab ) C a
50 coman2 186 . . . . . . . . . . . 12 (ab ) C b
5150comcom7 460 . . . . . . . . . . 11 (ab ) C b
5249, 51com2an 484 . . . . . . . . . 10 (ab ) C (ab)
5347, 52fh2rc 480 . . . . . . . . 9 (((ab) ∪ (ab )) ∩ ((ab) ∩ c)) = (((ab) ∩ ((ab) ∩ c)) ∪ ((ab ) ∩ ((ab) ∩ c)))
54 anass 76 . . . . . . . . . . . 12 (((ab) ∩ (ab)) ∩ c) = ((ab) ∩ ((ab) ∩ c))
5554ax-r1 35 . . . . . . . . . . 11 ((ab) ∩ ((ab) ∩ c)) = (((ab) ∩ (ab)) ∩ c)
56 leao1 162 . . . . . . . . . . . . 13 (ab) ≤ (ab)
5756df2le2 136 . . . . . . . . . . . 12 ((ab) ∩ (ab)) = (ab)
5857ran 78 . . . . . . . . . . 11 (((ab) ∩ (ab)) ∩ c) = ((ab) ∩ c)
5955, 58ax-r2 36 . . . . . . . . . 10 ((ab) ∩ ((ab) ∩ c)) = ((ab) ∩ c)
60 dff 101 . . . . . . . . . . . . . 14 0 = ((ab ) ∩ (ab ) )
61 oran 87 . . . . . . . . . . . . . . . 16 (ab) = (ab )
6261lan 77 . . . . . . . . . . . . . . 15 ((ab ) ∩ (ab)) = ((ab ) ∩ (ab ) )
6362ax-r1 35 . . . . . . . . . . . . . 14 ((ab ) ∩ (ab ) ) = ((ab ) ∩ (ab))
6460, 63ax-r2 36 . . . . . . . . . . . . 13 0 = ((ab ) ∩ (ab))
6564ran 78 . . . . . . . . . . . 12 (0 ∩ c) = (((ab ) ∩ (ab)) ∩ c)
6665ax-r1 35 . . . . . . . . . . 11 (((ab ) ∩ (ab)) ∩ c) = (0 ∩ c)
67 anass 76 . . . . . . . . . . 11 (((ab ) ∩ (ab)) ∩ c) = ((ab ) ∩ ((ab) ∩ c))
68 an0r 109 . . . . . . . . . . 11 (0 ∩ c) = 0
6966, 67, 683tr2 64 . . . . . . . . . 10 ((ab ) ∩ ((ab) ∩ c)) = 0
7059, 692or 72 . . . . . . . . 9 (((ab) ∩ ((ab) ∩ c)) ∪ ((ab ) ∩ ((ab) ∩ c))) = (((ab) ∩ c) ∪ 0)
71 or0 102 . . . . . . . . 9 (((ab) ∩ c) ∪ 0) = ((ab) ∩ c)
7253, 70, 713tr 65 . . . . . . . 8 (((ab) ∪ (ab )) ∩ ((ab) ∩ c)) = ((ab) ∩ c)
73 comanr1 464 . . . . . . . . . 10 (ab ) C ((ab ) ∩ c )
7473, 52fh2rc 480 . . . . . . . . 9 (((ab) ∪ (ab )) ∩ ((ab ) ∩ c )) = (((ab) ∩ ((ab ) ∩ c )) ∪ ((ab ) ∩ ((ab ) ∩ c )))
75 an4 86 . . . . . . . . . . 11 ((ab) ∩ ((ab ) ∩ c )) = ((a ∩ (ab )) ∩ (bc ))
76 dff 101 . . . . . . . . . . . . . . 15 0 = (aa )
7776ran 78 . . . . . . . . . . . . . 14 (0 ∩ b ) = ((aa ) ∩ b )
78 an0r 109 . . . . . . . . . . . . . 14 (0 ∩ b ) = 0
79 anass 76 . . . . . . . . . . . . . 14 ((aa ) ∩ b ) = (a ∩ (ab ))
8077, 78, 793tr2 64 . . . . . . . . . . . . 13 0 = (a ∩ (ab ))
8180ran 78 . . . . . . . . . . . 12 (0 ∩ (bc )) = ((a ∩ (ab )) ∩ (bc ))
8281ax-r1 35 . . . . . . . . . . 11 ((a ∩ (ab )) ∩ (bc )) = (0 ∩ (bc ))
83 an0r 109 . . . . . . . . . . 11 (0 ∩ (bc )) = 0
8475, 82, 833tr 65 . . . . . . . . . 10 ((ab) ∩ ((ab ) ∩ c )) = 0
85 anass 76 . . . . . . . . . . . 12 (((ab ) ∩ (ab )) ∩ c ) = ((ab ) ∩ ((ab ) ∩ c ))
8685ax-r1 35 . . . . . . . . . . 11 ((ab ) ∩ ((ab ) ∩ c )) = (((ab ) ∩ (ab )) ∩ c )
87 anidm 111 . . . . . . . . . . . 12 ((ab ) ∩ (ab )) = (ab )
8887ran 78 . . . . . . . . . . 11 (((ab ) ∩ (ab )) ∩ c ) = ((ab ) ∩ c )
8986, 88ax-r2 36 . . . . . . . . . 10 ((ab ) ∩ ((ab ) ∩ c )) = ((ab ) ∩ c )
9084, 892or 72 . . . . . . . . 9 (((ab) ∩ ((ab ) ∩ c )) ∪ ((ab ) ∩ ((ab ) ∩ c ))) = (0 ∪ ((ab ) ∩ c ))
91 or0r 103 . . . . . . . . 9 (0 ∪ ((ab ) ∩ c )) = ((ab ) ∩ c )
9274, 90, 913tr 65 . . . . . . . 8 (((ab) ∪ (ab )) ∩ ((ab ) ∩ c )) = ((ab ) ∩ c )
9372, 922or 72 . . . . . . 7 ((((ab) ∪ (ab )) ∩ ((ab) ∩ c)) ∪ (((ab) ∪ (ab )) ∩ ((ab ) ∩ c ))) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))
9443, 93ax-r2 36 . . . . . 6 (((ab) ∪ (ab )) ∩ (((ab) ∩ c) ∪ ((ab ) ∩ c ))) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))
95 dfb 94 . . . . . . 7 (ab) = ((ab) ∪ (ab ))
96 dfb 94 . . . . . . . 8 ((ab) ≡ c) = (((ab) ∩ c) ∪ ((ab)c ))
9744ran 78 . . . . . . . . . 10 ((ab ) ∩ c ) = ((ab)c )
9897lor 70 . . . . . . . . 9 (((ab) ∩ c) ∪ ((ab ) ∩ c )) = (((ab) ∩ c) ∪ ((ab)c ))
9998ax-r1 35 . . . . . . . 8 (((ab) ∩ c) ∪ ((ab)c )) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))
10096, 99ax-r2 36 . . . . . . 7 ((ab) ≡ c) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))
10195, 1002an 79 . . . . . 6 ((ab) ∩ ((ab) ≡ c)) = (((ab) ∪ (ab )) ∩ (((ab) ∩ c) ∪ ((ab ) ∩ c )))
102 bi3 839 . . . . . 6 ((ab) ∩ (bc)) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))
10394, 101, 1023tr1 63 . . . . 5 ((ab) ∩ ((ab) ≡ c)) = ((ab) ∩ (bc))
104 mlaoml 833 . . . . 5 ((ab) ∩ (bc)) ≤ (ac)
105103, 104bltr 138 . . . 4 ((ab) ∩ ((ab) ≡ c)) ≤ (ac)
10627, 105letr 137 . . 3 ((de) ∩ ((ec ) ∪ (dc))) ≤ (ac)
10719, 106bltr 138 . 2 (((ab) ≡ (ab)) ∩ (((ab)c ) ∪ (c ∩ (ab)))) ≤ (ac)
1088, 107letr 137 1 ((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  tb 5  wo 6  wa 7  0wf 9  1 wi1 12  2 wi2 13
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: (None)
  Copyright terms: Public domain W3C validator