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

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

Proof of Theorem ud3lem1a
StepHypRef Expression
1 ud3lem0c 279 . . 3 (a3 b) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
2 df-i3 46 . . 3 (b3 a) = (((ba) ∪ (ba )) ∪ (b ∩ (ba)))
31, 22an 79 . 2 ((a3 b) ∩ (b3 a)) = ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (((ba) ∪ (ba )) ∪ (b ∩ (ba))))
4 comor2 462 . . . . . . . . 9 (ab ) C b
5 comor1 461 . . . . . . . . 9 (ab ) C a
64, 5com2an 484 . . . . . . . 8 (ab ) C (ba)
75comcom2 183 . . . . . . . . 9 (ab ) C a
84, 7com2an 484 . . . . . . . 8 (ab ) C (ba )
96, 8com2or 483 . . . . . . 7 (ab ) C ((ba) ∪ (ba ))
109comcom 453 . . . . . 6 ((ba) ∪ (ba )) C (ab )
11 comor2 462 . . . . . . . . . 10 (ab) C b
1211comcom2 183 . . . . . . . . 9 (ab) C b
13 comor1 461 . . . . . . . . 9 (ab) C a
1412, 13com2an 484 . . . . . . . 8 (ab) C (ba)
1513comcom2 183 . . . . . . . . 9 (ab) C a
1612, 15com2an 484 . . . . . . . 8 (ab) C (ba )
1714, 16com2or 483 . . . . . . 7 (ab) C ((ba) ∪ (ba ))
1817comcom 453 . . . . . 6 ((ba) ∪ (ba )) C (ab)
1910, 18com2an 484 . . . . 5 ((ba) ∪ (ba )) C ((ab ) ∩ (ab))
20 comanr2 465 . . . . . . . . 9 a C (ba)
2120comcom3 454 . . . . . . . 8 a C (ba)
22 comanr2 465 . . . . . . . 8 a C (ba )
2321, 22com2or 483 . . . . . . 7 a C ((ba) ∪ (ba ))
2423comcom 453 . . . . . 6 ((ba) ∪ (ba )) C a
25 coman2 186 . . . . . . . . 9 (ab ) C b
26 coman1 185 . . . . . . . . 9 (ab ) C a
2725, 26com2an 484 . . . . . . . 8 (ab ) C (ba)
2826comcom2 183 . . . . . . . . 9 (ab ) C a
2925, 28com2an 484 . . . . . . . 8 (ab ) C (ba )
3027, 29com2or 483 . . . . . . 7 (ab ) C ((ba) ∪ (ba ))
3130comcom 453 . . . . . 6 ((ba) ∪ (ba )) C (ab )
3224, 31com2or 483 . . . . 5 ((ba) ∪ (ba )) C (a ∪ (ab ))
3319, 32com2an 484 . . . 4 ((ba) ∪ (ba )) C (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
34 comanr1 464 . . . . . . . 8 b C (ba)
3534comcom6 459 . . . . . . 7 b C (ba)
36 comanr1 464 . . . . . . . 8 b C (ba )
3736comcom6 459 . . . . . . 7 b C (ba )
3835, 37com2or 483 . . . . . 6 b C ((ba) ∪ (ba ))
3938comcom 453 . . . . 5 ((ba) ∪ (ba )) C b
40 comor1 461 . . . . . . . 8 (ba) C b
41 comor2 462 . . . . . . . 8 (ba) C a
4240, 41com2an 484 . . . . . . 7 (ba) C (ba)
4341comcom2 183 . . . . . . . 8 (ba) C a
4440, 43com2an 484 . . . . . . 7 (ba) C (ba )
4542, 44com2or 483 . . . . . 6 (ba) C ((ba) ∪ (ba ))
4645comcom 453 . . . . 5 ((ba) ∪ (ba )) C (ba)
4739, 46com2an 484 . . . 4 ((ba) ∪ (ba )) C (b ∩ (ba))
4833, 47fh2 470 . . 3 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ ((ba) ∪ (ba ))) ∪ ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (b ∩ (ba))))
49 coman2 186 . . . . . . . . . 10 (ba) C a
50 coman1 185 . . . . . . . . . 10 (ba) C b
5149, 50com2or 483 . . . . . . . . 9 (ba) C (ab )
5250comcom7 460 . . . . . . . . . 10 (ba) C b
5349, 52com2or 483 . . . . . . . . 9 (ba) C (ab)
5451, 53com2an 484 . . . . . . . 8 (ba) C ((ab ) ∩ (ab))
5549comcom2 183 . . . . . . . . 9 (ba) C a
5649, 50com2an 484 . . . . . . . . 9 (ba) C (ab )
5755, 56com2or 483 . . . . . . . 8 (ba) C (a ∪ (ab ))
5854, 57com2an 484 . . . . . . 7 (ba) C (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
5950, 55com2an 484 . . . . . . 7 (ba) C (ba )
6058, 59fh2 470 . . . . . 6 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ ((ba) ∪ (ba ))) = (((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba)) ∪ ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba )))
61 anass 76 . . . . . . . . 9 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba)) = (((ab ) ∩ (ab)) ∩ ((a ∪ (ab )) ∩ (ba)))
62 ancom 74 . . . . . . . . . . . 12 ((a ∪ (ab )) ∩ (ba)) = ((ba) ∩ (a ∪ (ab )))
63 ancom 74 . . . . . . . . . . . . . 14 (ba) = (ab )
64 ax-a2 31 . . . . . . . . . . . . . 14 (a ∪ (ab )) = ((ab ) ∪ a )
6563, 642an 79 . . . . . . . . . . . . 13 ((ba) ∩ (a ∪ (ab ))) = ((ab ) ∩ ((ab ) ∪ a ))
66 anabs 121 . . . . . . . . . . . . 13 ((ab ) ∩ ((ab ) ∪ a )) = (ab )
6765, 66ax-r2 36 . . . . . . . . . . . 12 ((ba) ∩ (a ∪ (ab ))) = (ab )
6862, 67ax-r2 36 . . . . . . . . . . 11 ((a ∪ (ab )) ∩ (ba)) = (ab )
6968lan 77 . . . . . . . . . 10 (((ab ) ∩ (ab)) ∩ ((a ∪ (ab )) ∩ (ba))) = (((ab ) ∩ (ab)) ∩ (ab ))
70 ancom 74 . . . . . . . . . . 11 (((ab ) ∩ (ab)) ∩ (ab )) = ((ab ) ∩ ((ab ) ∩ (ab)))
71 lea 160 . . . . . . . . . . . . 13 (ab ) ≤ a
72 leo 158 . . . . . . . . . . . . . 14 a ≤ (ab )
73 leo 158 . . . . . . . . . . . . . 14 a ≤ (ab)
7472, 73ler2an 173 . . . . . . . . . . . . 13 a ≤ ((ab ) ∩ (ab))
7571, 74letr 137 . . . . . . . . . . . 12 (ab ) ≤ ((ab ) ∩ (ab))
7675df2le2 136 . . . . . . . . . . 11 ((ab ) ∩ ((ab ) ∩ (ab))) = (ab )
7770, 76ax-r2 36 . . . . . . . . . 10 (((ab ) ∩ (ab)) ∩ (ab )) = (ab )
7869, 77ax-r2 36 . . . . . . . . 9 (((ab ) ∩ (ab)) ∩ ((a ∪ (ab )) ∩ (ba))) = (ab )
7961, 78ax-r2 36 . . . . . . . 8 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba)) = (ab )
80 an32 83 . . . . . . . . 9 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba )) = ((((ab ) ∩ (ab)) ∩ (ba )) ∩ (a ∪ (ab )))
81 anass 76 . . . . . . . . . . . 12 (((ab ) ∩ (ab)) ∩ (ba )) = ((ab ) ∩ ((ab) ∩ (ba )))
82 ax-a2 31 . . . . . . . . . . . . . . . 16 (ab) = (ba)
83 oran 87 . . . . . . . . . . . . . . . . . 18 (ba) = (ba )
8483ax-r1 35 . . . . . . . . . . . . . . . . 17 (ba ) = (ba)
8584con3 68 . . . . . . . . . . . . . . . 16 (ba ) = (ba)
8682, 852an 79 . . . . . . . . . . . . . . 15 ((ab) ∩ (ba )) = ((ba) ∩ (ba) )
87 dff 101 . . . . . . . . . . . . . . . 16 0 = ((ba) ∩ (ba) )
8887ax-r1 35 . . . . . . . . . . . . . . 15 ((ba) ∩ (ba) ) = 0
8986, 88ax-r2 36 . . . . . . . . . . . . . 14 ((ab) ∩ (ba )) = 0
9089lan 77 . . . . . . . . . . . . 13 ((ab ) ∩ ((ab) ∩ (ba ))) = ((ab ) ∩ 0)
91 an0 108 . . . . . . . . . . . . 13 ((ab ) ∩ 0) = 0
9290, 91ax-r2 36 . . . . . . . . . . . 12 ((ab ) ∩ ((ab) ∩ (ba ))) = 0
9381, 92ax-r2 36 . . . . . . . . . . 11 (((ab ) ∩ (ab)) ∩ (ba )) = 0
9493ran 78 . . . . . . . . . 10 ((((ab ) ∩ (ab)) ∩ (ba )) ∩ (a ∪ (ab ))) = (0 ∩ (a ∪ (ab )))
95 an0r 109 . . . . . . . . . 10 (0 ∩ (a ∪ (ab ))) = 0
9694, 95ax-r2 36 . . . . . . . . 9 ((((ab ) ∩ (ab)) ∩ (ba )) ∩ (a ∪ (ab ))) = 0
9780, 96ax-r2 36 . . . . . . . 8 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba )) = 0
9879, 972or 72 . . . . . . 7 (((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba)) ∪ ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba ))) = ((ab ) ∪ 0)
99 or0 102 . . . . . . 7 ((ab ) ∪ 0) = (ab )
10098, 99ax-r2 36 . . . . . 6 (((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba)) ∪ ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (ba ))) = (ab )
10160, 100ax-r2 36 . . . . 5 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ ((ba) ∪ (ba ))) = (ab )
102 anass 76 . . . . . 6 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (b ∩ (ba))) = (((ab ) ∩ (ab)) ∩ ((a ∪ (ab )) ∩ (b ∩ (ba))))
103 anass 76 . . . . . . . . . 10 (((a ∪ (ab )) ∩ b) ∩ (ba)) = ((a ∪ (ab )) ∩ (b ∩ (ba)))
104103ax-r1 35 . . . . . . . . 9 ((a ∪ (ab )) ∩ (b ∩ (ba))) = (((a ∪ (ab )) ∩ b) ∩ (ba))
10564ran 78 . . . . . . . . . . . 12 ((a ∪ (ab )) ∩ b) = (((ab ) ∪ a ) ∩ b)
10625comcom7 460 . . . . . . . . . . . . . 14 (ab ) C b
107106, 28fh2r 474 . . . . . . . . . . . . 13 (((ab ) ∪ a ) ∩ b) = (((ab ) ∩ b) ∪ (ab))
108 anass 76 . . . . . . . . . . . . . . . 16 ((ab ) ∩ b) = (a ∩ (bb))
109 ancom 74 . . . . . . . . . . . . . . . . . . 19 (bb) = (bb )
110 dff 101 . . . . . . . . . . . . . . . . . . . 20 0 = (bb )
111110ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (bb ) = 0
112109, 111ax-r2 36 . . . . . . . . . . . . . . . . . 18 (bb) = 0
113112lan 77 . . . . . . . . . . . . . . . . 17 (a ∩ (bb)) = (a ∩ 0)
114 an0 108 . . . . . . . . . . . . . . . . 17 (a ∩ 0) = 0
115113, 114ax-r2 36 . . . . . . . . . . . . . . . 16 (a ∩ (bb)) = 0
116108, 115ax-r2 36 . . . . . . . . . . . . . . 15 ((ab ) ∩ b) = 0
117 ancom 74 . . . . . . . . . . . . . . 15 (ab) = (ba )
118116, 1172or 72 . . . . . . . . . . . . . 14 (((ab ) ∩ b) ∪ (ab)) = (0 ∪ (ba ))
119 or0r 103 . . . . . . . . . . . . . 14 (0 ∪ (ba )) = (ba )
120118, 119ax-r2 36 . . . . . . . . . . . . 13 (((ab ) ∩ b) ∪ (ab)) = (ba )
121107, 120ax-r2 36 . . . . . . . . . . . 12 (((ab ) ∪ a ) ∩ b) = (ba )
122105, 121ax-r2 36 . . . . . . . . . . 11 ((a ∪ (ab )) ∩ b) = (ba )
123122ran 78 . . . . . . . . . 10 (((a ∪ (ab )) ∩ b) ∩ (ba)) = ((ba ) ∩ (ba))
124 anor1 88 . . . . . . . . . . . . . 14 (ba ) = (ba)
125124ax-r1 35 . . . . . . . . . . . . 13 (ba) = (ba )
126125con3 68 . . . . . . . . . . . 12 (ba) = (ba )
127126lan 77 . . . . . . . . . . 11 ((ba ) ∩ (ba)) = ((ba ) ∩ (ba ) )
128 dff 101 . . . . . . . . . . . 12 0 = ((ba ) ∩ (ba ) )
129128ax-r1 35 . . . . . . . . . . 11 ((ba ) ∩ (ba ) ) = 0
130127, 129ax-r2 36 . . . . . . . . . 10 ((ba ) ∩ (ba)) = 0
131123, 130ax-r2 36 . . . . . . . . 9 (((a ∪ (ab )) ∩ b) ∩ (ba)) = 0
132104, 131ax-r2 36 . . . . . . . 8 ((a ∪ (ab )) ∩ (b ∩ (ba))) = 0
133132lan 77 . . . . . . 7 (((ab ) ∩ (ab)) ∩ ((a ∪ (ab )) ∩ (b ∩ (ba)))) = (((ab ) ∩ (ab)) ∩ 0)
134 an0 108 . . . . . . 7 (((ab ) ∩ (ab)) ∩ 0) = 0
135133, 134ax-r2 36 . . . . . 6 (((ab ) ∩ (ab)) ∩ ((a ∪ (ab )) ∩ (b ∩ (ba)))) = 0
136102, 135ax-r2 36 . . . . 5 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (b ∩ (ba))) = 0
137101, 1362or 72 . . . 4 (((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ ((ba) ∪ (ba ))) ∪ ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (b ∩ (ba)))) = ((ab ) ∪ 0)
138137, 99ax-r2 36 . . 3 (((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ ((ba) ∪ (ba ))) ∪ ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (b ∩ (ba)))) = (ab )
13948, 138ax-r2 36 . 2 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∩ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (ab )
1403, 139ax-r2 36 1 ((a3 b) ∩ (b3 a)) = (ab )
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