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

Theorem 1oa 820
Description: Orthoarguesian-like law with 1 instead of 0 but true in all OMLs. (Contributed by NM, 1-Nov-1998.)
Assertion
Ref Expression
1oa ((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Proof of Theorem 1oa
StepHypRef Expression
1 lear 161 . . 3 ((((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ (b ∪ (ab )))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac )))) ≤ ((a ∩ (bc )) ∪ (c ∪ (ac )))
2 an12 81 . . . . 5 (a ∩ (bc )) = (b ∩ (ac ))
3 lear 161 . . . . . 6 (b ∩ (ac )) ≤ (ac )
43lerr 150 . . . . 5 (b ∩ (ac )) ≤ (c ∪ (ac ))
52, 4bltr 138 . . . 4 (a ∩ (bc )) ≤ (c ∪ (ac ))
6 leid 148 . . . 4 (c ∪ (ac )) ≤ (c ∪ (ac ))
75, 6lel2or 170 . . 3 ((a ∩ (bc )) ∪ (c ∪ (ac ))) ≤ (c ∪ (ac ))
81, 7letr 137 . 2 ((((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ (b ∪ (ab )))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac )))) ≤ (c ∪ (ac ))
9 df-i1 44 . . . 4 ((bc) →1 ((a2 b) ∩ (a2 c))) = ((bc) ∪ ((bc) ∩ ((a2 b) ∩ (a2 c))))
109lan 77 . . 3 ((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ ((bc) ∪ ((bc) ∩ ((a2 b) ∩ (a2 c)))))
11 an12 81 . . . . . 6 ((a2 b) ∩ ((bc) ∩ (a2 c))) = ((bc) ∩ ((a2 b) ∩ (a2 c)))
1211ax-r1 35 . . . . 5 ((bc) ∩ ((a2 b) ∩ (a2 c))) = ((a2 b) ∩ ((bc) ∩ (a2 c)))
13 coman1 185 . . . . 5 ((a2 b) ∩ ((bc) ∩ (a2 c))) C (a2 b)
1412, 13bctr 181 . . . 4 ((bc) ∩ ((a2 b) ∩ (a2 c))) C (a2 b)
15 coman1 185 . . . . 5 ((bc) ∩ ((a2 b) ∩ (a2 c))) C (bc)
1615comcom2 183 . . . 4 ((bc) ∩ ((a2 b) ∩ (a2 c))) C (bc)
1714, 16fh2c 477 . . 3 ((a2 b) ∩ ((bc) ∪ ((bc) ∩ ((a2 b) ∩ (a2 c))))) = (((a2 b) ∩ (bc) ) ∪ ((a2 b) ∩ ((bc) ∩ ((a2 b) ∩ (a2 c)))))
18 df-i2 45 . . . . . . 7 (a2 b) = (b ∪ (ab ))
19 anor3 90 . . . . . . . 8 (bc ) = (bc)
2019ax-r1 35 . . . . . . 7 (bc) = (bc )
2118, 202an 79 . . . . . 6 ((a2 b) ∩ (bc) ) = ((b ∪ (ab )) ∩ (bc ))
22 comid 187 . . . . . . . . . . 11 b C b
2322comcom3 454 . . . . . . . . . 10 b C b
24 comanr2 465 . . . . . . . . . 10 b C (ab )
2523, 24fh1r 473 . . . . . . . . 9 ((b ∪ (ab )) ∩ b ) = ((bb ) ∪ ((ab ) ∩ b ))
26 dff 101 . . . . . . . . . . 11 0 = (bb )
2726ax-r1 35 . . . . . . . . . 10 (bb ) = 0
28 anass 76 . . . . . . . . . . 11 ((ab ) ∩ b ) = (a ∩ (bb ))
29 anidm 111 . . . . . . . . . . . 12 (bb ) = b
3029lan 77 . . . . . . . . . . 11 (a ∩ (bb )) = (ab )
3128, 30ax-r2 36 . . . . . . . . . 10 ((ab ) ∩ b ) = (ab )
3227, 312or 72 . . . . . . . . 9 ((bb ) ∪ ((ab ) ∩ b )) = (0 ∪ (ab ))
33 ax-a2 31 . . . . . . . . . 10 (0 ∪ (ab )) = ((ab ) ∪ 0)
34 or0 102 . . . . . . . . . 10 ((ab ) ∪ 0) = (ab )
3533, 34ax-r2 36 . . . . . . . . 9 (0 ∪ (ab )) = (ab )
3625, 32, 353tr 65 . . . . . . . 8 ((b ∪ (ab )) ∩ b ) = (ab )
3736ran 78 . . . . . . 7 (((b ∪ (ab )) ∩ b ) ∩ c ) = ((ab ) ∩ c )
38 anass 76 . . . . . . 7 (((b ∪ (ab )) ∩ b ) ∩ c ) = ((b ∪ (ab )) ∩ (bc ))
39 anass 76 . . . . . . 7 ((ab ) ∩ c ) = (a ∩ (bc ))
4037, 38, 393tr2 64 . . . . . 6 ((b ∪ (ab )) ∩ (bc )) = (a ∩ (bc ))
4121, 40ax-r2 36 . . . . 5 ((a2 b) ∩ (bc) ) = (a ∩ (bc ))
42 an12 81 . . . . . 6 ((a2 b) ∩ ((bc) ∩ ((a2 b) ∩ (a2 c)))) = ((bc) ∩ ((a2 b) ∩ ((a2 b) ∩ (a2 c))))
43 anass 76 . . . . . . . . 9 (((a2 b) ∩ (a2 b)) ∩ (a2 c)) = ((a2 b) ∩ ((a2 b) ∩ (a2 c)))
4443ax-r1 35 . . . . . . . 8 ((a2 b) ∩ ((a2 b) ∩ (a2 c))) = (((a2 b) ∩ (a2 b)) ∩ (a2 c))
45 anidm 111 . . . . . . . . . 10 ((a2 b) ∩ (a2 b)) = (a2 b)
4645, 18ax-r2 36 . . . . . . . . 9 ((a2 b) ∩ (a2 b)) = (b ∪ (ab ))
47 df-i2 45 . . . . . . . . 9 (a2 c) = (c ∪ (ac ))
4846, 472an 79 . . . . . . . 8 (((a2 b) ∩ (a2 b)) ∩ (a2 c)) = ((b ∪ (ab )) ∩ (c ∪ (ac )))
4944, 48ax-r2 36 . . . . . . 7 ((a2 b) ∩ ((a2 b) ∩ (a2 c))) = ((b ∪ (ab )) ∩ (c ∪ (ac )))
5049lan 77 . . . . . 6 ((bc) ∩ ((a2 b) ∩ ((a2 b) ∩ (a2 c)))) = ((bc) ∩ ((b ∪ (ab )) ∩ (c ∪ (ac ))))
5142, 50ax-r2 36 . . . . 5 ((a2 b) ∩ ((bc) ∩ ((a2 b) ∩ (a2 c)))) = ((bc) ∩ ((b ∪ (ab )) ∩ (c ∪ (ac ))))
5241, 512or 72 . . . 4 (((a2 b) ∩ (bc) ) ∪ ((a2 b) ∩ ((bc) ∩ ((a2 b) ∩ (a2 c))))) = ((a ∩ (bc )) ∪ ((bc) ∩ ((b ∪ (ab )) ∩ (c ∪ (ac )))))
5339ax-r1 35 . . . . . . . 8 (a ∩ (bc )) = ((ab ) ∩ c )
54 lea 160 . . . . . . . . . 10 ((ab ) ∩ c ) ≤ (ab )
5554lerr 150 . . . . . . . . 9 ((ab ) ∩ c ) ≤ (b ∪ (ab ))
5655lecom 180 . . . . . . . 8 ((ab ) ∩ c ) C (b ∪ (ab ))
5753, 56bctr 181 . . . . . . 7 (a ∩ (bc )) C (b ∪ (ab ))
584lecom 180 . . . . . . . 8 (b ∩ (ac )) C (c ∪ (ac ))
592, 58bctr 181 . . . . . . 7 (a ∩ (bc )) C (c ∪ (ac ))
6057, 59fh3 471 . . . . . 6 ((a ∩ (bc )) ∪ ((b ∪ (ab )) ∩ (c ∪ (ac )))) = (((a ∩ (bc )) ∪ (b ∪ (ab ))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac ))))
6160lan 77 . . . . 5 (((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ ((b ∪ (ab )) ∩ (c ∪ (ac ))))) = (((a ∩ (bc )) ∪ (bc)) ∩ (((a ∩ (bc )) ∪ (b ∪ (ab ))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac )))))
62 coman2 186 . . . . . . . 8 (a ∩ (bc )) C (bc )
6362comcom2 183 . . . . . . 7 (a ∩ (bc )) C (bc )
64 oran 87 . . . . . . . 8 (bc) = (bc )
6564ax-r1 35 . . . . . . 7 (bc ) = (bc)
6663, 65cbtr 182 . . . . . 6 (a ∩ (bc )) C (bc)
6757, 59com2an 484 . . . . . 6 (a ∩ (bc )) C ((b ∪ (ab )) ∩ (c ∪ (ac )))
6866, 67fh3 471 . . . . 5 ((a ∩ (bc )) ∪ ((bc) ∩ ((b ∪ (ab )) ∩ (c ∪ (ac ))))) = (((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ ((b ∪ (ab )) ∩ (c ∪ (ac )))))
69 anass 76 . . . . 5 ((((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ (b ∪ (ab )))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac )))) = (((a ∩ (bc )) ∪ (bc)) ∩ (((a ∩ (bc )) ∪ (b ∪ (ab ))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac )))))
7061, 68, 693tr1 63 . . . 4 ((a ∩ (bc )) ∪ ((bc) ∩ ((b ∪ (ab )) ∩ (c ∪ (ac ))))) = ((((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ (b ∪ (ab )))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac ))))
7152, 70ax-r2 36 . . 3 (((a2 b) ∩ (bc) ) ∪ ((a2 b) ∩ ((bc) ∩ ((a2 b) ∩ (a2 c))))) = ((((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ (b ∪ (ab )))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac ))))
7210, 17, 713tr 65 . 2 ((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) = ((((a ∩ (bc )) ∪ (bc)) ∩ ((a ∩ (bc )) ∪ (b ∪ (ab )))) ∩ ((a ∩ (bc )) ∪ (c ∪ (ac ))))
738, 72, 47le3tr1 140 1 ((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
Colors of variables: term
Syntax hints:  wle 2   wn 4  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:  1oai1  821  1oaiii  823  distoa  944
  Copyright terms: Public domain W3C validator