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

Theorem ud3lem1b 567
Description: Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
Assertion
Ref Expression
ud3lem1b ((a3 b) ∩ (b3 a) ) = 0

Proof of Theorem ud3lem1b
StepHypRef Expression
1 ud3lem0c 279 . . 3 (a3 b) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
2 ud3lem0c 279 . . 3 (b3 a) = (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))
31, 22an 79 . 2 ((a3 b) ∩ (b3 a) ) = ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba ))))
4 an32 83 . . 3 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) = ((((ab ) ∩ (ab)) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) ∩ (a ∪ (ab )))
5 an32 83 . . . . . 6 (((ab ) ∩ (ab)) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) = (((ab ) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) ∩ (ab))
6 an12 81 . . . . . . . . 9 ((ab ) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) = (((ba ) ∩ (ba)) ∩ ((ab ) ∩ (b ∪ (ba ))))
7 comor2 462 . . . . . . . . . . . . 13 (ab ) C b
87comcom7 460 . . . . . . . . . . . . . 14 (ab ) C b
9 comor1 461 . . . . . . . . . . . . . . 15 (ab ) C a
109comcom2 183 . . . . . . . . . . . . . 14 (ab ) C a
118, 10com2an 484 . . . . . . . . . . . . 13 (ab ) C (ba )
127, 11fh1 469 . . . . . . . . . . . 12 ((ab ) ∩ (b ∪ (ba ))) = (((ab ) ∩ b ) ∪ ((ab ) ∩ (ba )))
13 ancom 74 . . . . . . . . . . . . . . . 16 ((ab ) ∩ b ) = (b ∩ (ab ))
14 ax-a2 31 . . . . . . . . . . . . . . . . 17 (ab ) = (ba)
1514lan 77 . . . . . . . . . . . . . . . 16 (b ∩ (ab )) = (b ∩ (ba))
1613, 15ax-r2 36 . . . . . . . . . . . . . . 15 ((ab ) ∩ b ) = (b ∩ (ba))
17 anabs 121 . . . . . . . . . . . . . . 15 (b ∩ (ba)) = b
1816, 17ax-r2 36 . . . . . . . . . . . . . 14 ((ab ) ∩ b ) = b
19 anor1 88 . . . . . . . . . . . . . . . 16 (ba ) = (ba)
2014, 192an 79 . . . . . . . . . . . . . . 15 ((ab ) ∩ (ba )) = ((ba) ∩ (ba) )
21 dff 101 . . . . . . . . . . . . . . . 16 0 = ((ba) ∩ (ba) )
2221ax-r1 35 . . . . . . . . . . . . . . 15 ((ba) ∩ (ba) ) = 0
2320, 22ax-r2 36 . . . . . . . . . . . . . 14 ((ab ) ∩ (ba )) = 0
2418, 232or 72 . . . . . . . . . . . . 13 (((ab ) ∩ b ) ∪ ((ab ) ∩ (ba ))) = (b ∪ 0)
25 or0 102 . . . . . . . . . . . . 13 (b ∪ 0) = b
2624, 25ax-r2 36 . . . . . . . . . . . 12 (((ab ) ∩ b ) ∪ ((ab ) ∩ (ba ))) = b
2712, 26ax-r2 36 . . . . . . . . . . 11 ((ab ) ∩ (b ∪ (ba ))) = b
2827lan 77 . . . . . . . . . 10 (((ba ) ∩ (ba)) ∩ ((ab ) ∩ (b ∪ (ba )))) = (((ba ) ∩ (ba)) ∩ b )
29 ancom 74 . . . . . . . . . . 11 (((ba ) ∩ (ba)) ∩ b ) = (b ∩ ((ba ) ∩ (ba)))
30 anass 76 . . . . . . . . . . . 12 ((b ∩ (ba )) ∩ (ba)) = (b ∩ ((ba ) ∩ (ba)))
3130ax-r1 35 . . . . . . . . . . 11 (b ∩ ((ba ) ∩ (ba))) = ((b ∩ (ba )) ∩ (ba))
3229, 31ax-r2 36 . . . . . . . . . 10 (((ba ) ∩ (ba)) ∩ b ) = ((b ∩ (ba )) ∩ (ba))
3328, 32ax-r2 36 . . . . . . . . 9 (((ba ) ∩ (ba)) ∩ ((ab ) ∩ (b ∪ (ba )))) = ((b ∩ (ba )) ∩ (ba))
346, 33ax-r2 36 . . . . . . . 8 ((ab ) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) = ((b ∩ (ba )) ∩ (ba))
3534ran 78 . . . . . . 7 (((ab ) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) ∩ (ab)) = (((b ∩ (ba )) ∩ (ba)) ∩ (ab))
36 ax-a2 31 . . . . . . . . 9 (ab) = (ba)
3736lan 77 . . . . . . . 8 (((b ∩ (ba )) ∩ (ba)) ∩ (ab)) = (((b ∩ (ba )) ∩ (ba)) ∩ (ba))
38 anass 76 . . . . . . . . 9 (((b ∩ (ba )) ∩ (ba)) ∩ (ba)) = ((b ∩ (ba )) ∩ ((ba) ∩ (ba)))
39 anidm 111 . . . . . . . . . . 11 ((ba) ∩ (ba)) = (ba)
4039lan 77 . . . . . . . . . 10 ((b ∩ (ba )) ∩ ((ba) ∩ (ba))) = ((b ∩ (ba )) ∩ (ba))
41 an32 83 . . . . . . . . . 10 ((b ∩ (ba )) ∩ (ba)) = ((b ∩ (ba)) ∩ (ba ))
4240, 41ax-r2 36 . . . . . . . . 9 ((b ∩ (ba )) ∩ ((ba) ∩ (ba))) = ((b ∩ (ba)) ∩ (ba ))
4338, 42ax-r2 36 . . . . . . . 8 (((b ∩ (ba )) ∩ (ba)) ∩ (ba)) = ((b ∩ (ba)) ∩ (ba ))
4437, 43ax-r2 36 . . . . . . 7 (((b ∩ (ba )) ∩ (ba)) ∩ (ab)) = ((b ∩ (ba)) ∩ (ba ))
4535, 44ax-r2 36 . . . . . 6 (((ab ) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) ∩ (ab)) = ((b ∩ (ba)) ∩ (ba ))
465, 45ax-r2 36 . . . . 5 (((ab ) ∩ (ab)) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) = ((b ∩ (ba)) ∩ (ba ))
4746ran 78 . . . 4 ((((ab ) ∩ (ab)) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) ∩ (a ∪ (ab ))) = (((b ∩ (ba)) ∩ (ba )) ∩ (a ∪ (ab )))
48 anass 76 . . . . 5 (((b ∩ (ba)) ∩ (ba )) ∩ (a ∪ (ab ))) = ((b ∩ (ba)) ∩ ((ba ) ∩ (a ∪ (ab ))))
49 ax-a2 31 . . . . . . . . 9 (ba ) = (ab)
5049ran 78 . . . . . . . 8 ((ba ) ∩ (a ∪ (ab ))) = ((ab) ∩ (a ∪ (ab )))
51 ancom 74 . . . . . . . . 9 ((ab) ∩ (a ∪ (ab ))) = ((a ∪ (ab )) ∩ (ab))
52 comor1 461 . . . . . . . . . . 11 (ab) C a
5352comcom7 460 . . . . . . . . . . . 12 (ab) C a
54 comor2 462 . . . . . . . . . . . . 13 (ab) C b
5554comcom2 183 . . . . . . . . . . . 12 (ab) C b
5653, 55com2an 484 . . . . . . . . . . 11 (ab) C (ab )
5752, 56fh1r 473 . . . . . . . . . 10 ((a ∪ (ab )) ∩ (ab)) = ((a ∩ (ab)) ∪ ((ab ) ∩ (ab)))
58 anabs 121 . . . . . . . . . . . 12 (a ∩ (ab)) = a
59 ancom 74 . . . . . . . . . . . . 13 ((ab ) ∩ (ab)) = ((ab) ∩ (ab ))
60 anor1 88 . . . . . . . . . . . . . . 15 (ab ) = (ab)
6160lan 77 . . . . . . . . . . . . . 14 ((ab) ∩ (ab )) = ((ab) ∩ (ab) )
62 dff 101 . . . . . . . . . . . . . . 15 0 = ((ab) ∩ (ab) )
6362ax-r1 35 . . . . . . . . . . . . . 14 ((ab) ∩ (ab) ) = 0
6461, 63ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∩ (ab )) = 0
6559, 64ax-r2 36 . . . . . . . . . . . 12 ((ab ) ∩ (ab)) = 0
6658, 652or 72 . . . . . . . . . . 11 ((a ∩ (ab)) ∪ ((ab ) ∩ (ab))) = (a ∪ 0)
67 or0 102 . . . . . . . . . . 11 (a ∪ 0) = a
6866, 67ax-r2 36 . . . . . . . . . 10 ((a ∩ (ab)) ∪ ((ab ) ∩ (ab))) = a
6957, 68ax-r2 36 . . . . . . . . 9 ((a ∪ (ab )) ∩ (ab)) = a
7051, 69ax-r2 36 . . . . . . . 8 ((ab) ∩ (a ∪ (ab ))) = a
7150, 70ax-r2 36 . . . . . . 7 ((ba ) ∩ (a ∪ (ab ))) = a
7271lan 77 . . . . . 6 ((b ∩ (ba)) ∩ ((ba ) ∩ (a ∪ (ab )))) = ((b ∩ (ba)) ∩ a )
73 an32 83 . . . . . . 7 ((b ∩ (ba)) ∩ a ) = ((ba ) ∩ (ba))
74 oran 87 . . . . . . . . 9 (ba) = (ba )
7574lan 77 . . . . . . . 8 ((ba ) ∩ (ba)) = ((ba ) ∩ (ba ) )
76 dff 101 . . . . . . . . 9 0 = ((ba ) ∩ (ba ) )
7776ax-r1 35 . . . . . . . 8 ((ba ) ∩ (ba ) ) = 0
7875, 77ax-r2 36 . . . . . . 7 ((ba ) ∩ (ba)) = 0
7973, 78ax-r2 36 . . . . . 6 ((b ∩ (ba)) ∩ a ) = 0
8072, 79ax-r2 36 . . . . 5 ((b ∩ (ba)) ∩ ((ba ) ∩ (a ∪ (ab )))) = 0
8148, 80ax-r2 36 . . . 4 (((b ∩ (ba)) ∩ (ba )) ∩ (a ∪ (ab ))) = 0
8247, 81ax-r2 36 . . 3 ((((ab ) ∩ (ab)) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) ∩ (a ∪ (ab ))) = 0
834, 82ax-r2 36 . 2 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (((ba ) ∩ (ba)) ∩ (b ∪ (ba )))) = 0
843, 83ax-r2 36 1 ((a3 b) ∩ (b3 a) ) = 0
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  0wf 9  3 wi3 14
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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud3lem1  570
  Copyright terms: Public domain W3C validator