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

Theorem comanblem1 870
Description: Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
Assertion
Ref Expression
comanblem1 ((ac) ∩ (bc)) = (((ac) ∪ ((ab) ∩ c)) ∩ (b1 c))

Proof of Theorem comanblem1
StepHypRef Expression
1 an4 86 . 2 (((a1 c) ∩ (c1 a)) ∩ ((b1 c) ∩ (c1 b))) = (((a1 c) ∩ (b1 c)) ∩ ((c1 a) ∩ (c1 b)))
2 u1lembi 720 . . 3 ((a1 c) ∩ (c1 a)) = (ac)
3 u1lembi 720 . . 3 ((b1 c) ∩ (c1 b)) = (bc)
42, 32an 79 . 2 (((a1 c) ∩ (c1 a)) ∩ ((b1 c) ∩ (c1 b))) = ((ac) ∩ (bc))
5 an32 83 . . 3 (((a1 c) ∩ (b1 c)) ∩ ((c1 a) ∩ (c1 b))) = (((a1 c) ∩ ((c1 a) ∩ (c1 b))) ∩ (b1 c))
6 df-i1 44 . . . . . . . 8 (c1 a) = (c ∪ (ca))
7 df-i1 44 . . . . . . . 8 (c1 b) = (c ∪ (cb))
86, 72an 79 . . . . . . 7 ((c1 a) ∩ (c1 b)) = ((c ∪ (ca)) ∩ (c ∪ (cb)))
9 comanr1 464 . . . . . . . . . 10 c C (ca)
109comcom3 454 . . . . . . . . 9 c C (ca)
11 comanr1 464 . . . . . . . . . 10 c C (cb)
1211comcom3 454 . . . . . . . . 9 c C (cb)
1310, 12fh3 471 . . . . . . . 8 (c ∪ ((ca) ∩ (cb))) = ((c ∪ (ca)) ∩ (c ∪ (cb)))
1413ax-r1 35 . . . . . . 7 ((c ∪ (ca)) ∩ (c ∪ (cb))) = (c ∪ ((ca) ∩ (cb)))
158, 14ax-r2 36 . . . . . 6 ((c1 a) ∩ (c1 b)) = (c ∪ ((ca) ∩ (cb)))
1615lan 77 . . . . 5 ((a1 c) ∩ ((c1 a) ∩ (c1 b))) = ((a1 c) ∩ (c ∪ ((ca) ∩ (cb))))
17 df-i1 44 . . . . . 6 (a1 c) = (a ∪ (ac))
1817ran 78 . . . . 5 ((a1 c) ∩ (c ∪ ((ca) ∩ (cb)))) = ((a ∪ (ac)) ∩ (c ∪ ((ca) ∩ (cb))))
19 lea 160 . . . . . . . . 9 ((ca) ∩ (cb)) ≤ (ca)
20 ancom 74 . . . . . . . . . 10 (ca) = (ac)
21 leor 159 . . . . . . . . . 10 (ac) ≤ (a ∪ (ac))
2220, 21bltr 138 . . . . . . . . 9 (ca) ≤ (a ∪ (ac))
2319, 22letr 137 . . . . . . . 8 ((ca) ∩ (cb)) ≤ (a ∪ (ac))
2423lecom 180 . . . . . . 7 ((ca) ∩ (cb)) C (a ∪ (ac))
2510, 12com2an 484 . . . . . . . 8 c C ((ca) ∩ (cb))
2625comcom 453 . . . . . . 7 ((ca) ∩ (cb)) C c
2724, 26fh2c 477 . . . . . 6 ((a ∪ (ac)) ∩ (c ∪ ((ca) ∩ (cb)))) = (((a ∪ (ac)) ∩ c ) ∪ ((a ∪ (ac)) ∩ ((ca) ∩ (cb))))
28 coman2 186 . . . . . . . . . 10 (ac) C c
2928comcom2 183 . . . . . . . . 9 (ac) C c
30 coman1 185 . . . . . . . . . 10 (ac) C a
3130comcom2 183 . . . . . . . . 9 (ac) C a
3229, 31fh2rc 480 . . . . . . . 8 ((a ∪ (ac)) ∩ c ) = ((ac ) ∪ ((ac) ∩ c ))
33 anass 76 . . . . . . . . . 10 ((ac) ∩ c ) = (a ∩ (cc ))
34 dff 101 . . . . . . . . . . . 12 0 = (cc )
3534lan 77 . . . . . . . . . . 11 (a ∩ 0) = (a ∩ (cc ))
3635ax-r1 35 . . . . . . . . . 10 (a ∩ (cc )) = (a ∩ 0)
37 an0 108 . . . . . . . . . 10 (a ∩ 0) = 0
3833, 36, 373tr 65 . . . . . . . . 9 ((ac) ∩ c ) = 0
3938lor 70 . . . . . . . 8 ((ac ) ∪ ((ac) ∩ c )) = ((ac ) ∪ 0)
40 or0 102 . . . . . . . . 9 ((ac ) ∪ 0) = (ac )
41 anor3 90 . . . . . . . . 9 (ac ) = (ac)
4240, 41ax-r2 36 . . . . . . . 8 ((ac ) ∪ 0) = (ac)
4332, 39, 423tr 65 . . . . . . 7 ((a ∪ (ac)) ∩ c ) = (ac)
44 ancom 74 . . . . . . . . . 10 (ac) = (ca)
45 comanr1 464 . . . . . . . . . 10 (ca) C ((ca) ∩ (cb))
4644, 45bctr 181 . . . . . . . . 9 (ac) C ((ca) ∩ (cb))
4746, 31fh2rc 480 . . . . . . . 8 ((a ∪ (ac)) ∩ ((ca) ∩ (cb))) = ((a ∩ ((ca) ∩ (cb))) ∪ ((ac) ∩ ((ca) ∩ (cb))))
48 anandi 114 . . . . . . . . . . . 12 (c ∩ (ab)) = ((ca) ∩ (cb))
4948ax-r1 35 . . . . . . . . . . 11 ((ca) ∩ (cb)) = (c ∩ (ab))
50 ancom 74 . . . . . . . . . . 11 (c ∩ (ab)) = ((ab) ∩ c)
5149, 50ax-r2 36 . . . . . . . . . 10 ((ca) ∩ (cb)) = ((ab) ∩ c)
5251lan 77 . . . . . . . . 9 (a ∩ ((ca) ∩ (cb))) = (a ∩ ((ab) ∩ c))
5351lan 77 . . . . . . . . . 10 ((ac) ∩ ((ca) ∩ (cb))) = ((ac) ∩ ((ab) ∩ c))
54 ancom 74 . . . . . . . . . 10 ((ac) ∩ ((ab) ∩ c)) = (((ab) ∩ c) ∩ (ac))
55 lea 160 . . . . . . . . . . . 12 (ab) ≤ a
5655leran 153 . . . . . . . . . . 11 ((ab) ∩ c) ≤ (ac)
5756df2le2 136 . . . . . . . . . 10 (((ab) ∩ c) ∩ (ac)) = ((ab) ∩ c)
5853, 54, 573tr 65 . . . . . . . . 9 ((ac) ∩ ((ca) ∩ (cb))) = ((ab) ∩ c)
5952, 582or 72 . . . . . . . 8 ((a ∩ ((ca) ∩ (cb))) ∪ ((ac) ∩ ((ca) ∩ (cb)))) = ((a ∩ ((ab) ∩ c)) ∪ ((ab) ∩ c))
60 lear 161 . . . . . . . . 9 (a ∩ ((ab) ∩ c)) ≤ ((ab) ∩ c)
6160df-le2 131 . . . . . . . 8 ((a ∩ ((ab) ∩ c)) ∪ ((ab) ∩ c)) = ((ab) ∩ c)
6247, 59, 613tr 65 . . . . . . 7 ((a ∪ (ac)) ∩ ((ca) ∩ (cb))) = ((ab) ∩ c)
6343, 622or 72 . . . . . 6 (((a ∪ (ac)) ∩ c ) ∪ ((a ∪ (ac)) ∩ ((ca) ∩ (cb)))) = ((ac) ∪ ((ab) ∩ c))
6427, 63ax-r2 36 . . . . 5 ((a ∪ (ac)) ∩ (c ∪ ((ca) ∩ (cb)))) = ((ac) ∪ ((ab) ∩ c))
6516, 18, 643tr 65 . . . 4 ((a1 c) ∩ ((c1 a) ∩ (c1 b))) = ((ac) ∪ ((ab) ∩ c))
6665ran 78 . . 3 (((a1 c) ∩ ((c1 a) ∩ (c1 b))) ∩ (b1 c)) = (((ac) ∪ ((ab) ∩ c)) ∩ (b1 c))
675, 66ax-r2 36 . 2 (((a1 c) ∩ (b1 c)) ∩ ((c1 a) ∩ (c1 b))) = (((ac) ∪ ((ab) ∩ c)) ∩ (b1 c))
681, 4, 673tr2 64 1 ((ac) ∩ (bc)) = (((ac) ∪ ((ab) ∩ c)) ∩ (b1 c))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  tb 5  wo 6  wa 7  0wf 9  1 wi1 12
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  comanb  872
  Copyright terms: Public domain W3C validator