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

Theorem ud4lem1a 577
Description: Lemma for unified disjunction. (Contributed by NM, 24-Nov-1997.)
Assertion
Ref Expression
ud4lem1a ((a4 b) ∩ (b4 a)) = ((ab) ∪ (ab ))

Proof of Theorem ud4lem1a
StepHypRef Expression
1 df-i4 47 . . 3 (a4 b) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))
2 df-i4 47 . . 3 (b4 a) = (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))
31, 22an 79 . 2 ((a4 b) ∩ (b4 a)) = ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))
4 coman2 186 . . . . . . . . . 10 (ab) C b
54comcom 453 . . . . . . . . 9 b C (ab)
6 coman2 186 . . . . . . . . . 10 (ab) C b
76comcom 453 . . . . . . . . 9 b C (ab)
85, 7com2or 483 . . . . . . . 8 b C ((ab) ∪ (ab))
98comcom 453 . . . . . . 7 ((ab) ∪ (ab)) C b
10 coman1 185 . . . . . . . . . 10 (ab) C a
1110comcom 453 . . . . . . . . 9 a C (ab)
12 coman1 185 . . . . . . . . . . . 12 (ab) C a
1312comcom 453 . . . . . . . . . . 11 a C (ab)
1413comcom2 183 . . . . . . . . . 10 a C (ab)
1514comcom5 458 . . . . . . . . 9 a C (ab)
1611, 15com2or 483 . . . . . . . 8 a C ((ab) ∪ (ab))
1716comcom 453 . . . . . . 7 ((ab) ∪ (ab)) C a
189, 17com2an 484 . . . . . 6 ((ab) ∪ (ab)) C (ba)
195comcom3 454 . . . . . . . . 9 b C (ab)
207comcom3 454 . . . . . . . . 9 b C (ab)
2119, 20com2or 483 . . . . . . . 8 b C ((ab) ∪ (ab))
2221comcom 453 . . . . . . 7 ((ab) ∪ (ab)) C b
2322, 17com2an 484 . . . . . 6 ((ab) ∪ (ab)) C (ba)
2418, 23com2or 483 . . . . 5 ((ab) ∪ (ab)) C ((ba) ∪ (ba))
2522, 17com2or 483 . . . . . 6 ((ab) ∪ (ab)) C (ba)
2611comcom3 454 . . . . . . . 8 a C (ab)
2726, 13com2or 483 . . . . . . 7 a C ((ab) ∪ (ab))
2827comcom 453 . . . . . 6 ((ab) ∪ (ab)) C a
2925, 28com2an 484 . . . . 5 ((ab) ∪ (ab)) C ((ba) ∩ a )
3024, 29com2or 483 . . . 4 ((ab) ∪ (ab)) C (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))
3128, 9com2or 483 . . . . 5 ((ab) ∪ (ab)) C (ab)
329comcom2 183 . . . . 5 ((ab) ∪ (ab)) C b
3331, 32com2an 484 . . . 4 ((ab) ∪ (ab)) C ((ab) ∩ b )
3430, 33fh2r 474 . . 3 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((((ab) ∪ (ab)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∪ (((ab) ∩ b ) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))))
35 ancom 74 . . . . . . . . 9 (ba) = (ab)
36 ancom 74 . . . . . . . . 9 (ba) = (ab )
3735, 362or 72 . . . . . . . 8 ((ba) ∪ (ba)) = ((ab) ∪ (ab ))
38 ax-a2 31 . . . . . . . . 9 (ba) = (ab )
3938ran 78 . . . . . . . 8 ((ba) ∩ a ) = ((ab ) ∩ a )
4037, 392or 72 . . . . . . 7 (((ba) ∪ (ba)) ∪ ((ba) ∩ a )) = (((ab) ∪ (ab )) ∪ ((ab ) ∩ a ))
4140lan 77 . . . . . 6 (((ab) ∪ (ab)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (((ab) ∪ (ab)) ∩ (((ab) ∪ (ab )) ∪ ((ab ) ∩ a )))
4217, 9com2an 484 . . . . . . . . 9 ((ab) ∪ (ab)) C (ab)
4317, 22com2an 484 . . . . . . . . 9 ((ab) ∪ (ab)) C (ab )
4442, 43com2or 483 . . . . . . . 8 ((ab) ∪ (ab)) C ((ab) ∪ (ab ))
4517, 32com2or 483 . . . . . . . . 9 ((ab) ∪ (ab)) C (ab )
4645, 28com2an 484 . . . . . . . 8 ((ab) ∪ (ab)) C ((ab ) ∩ a )
4744, 46fh1 469 . . . . . . 7 (((ab) ∪ (ab)) ∩ (((ab) ∪ (ab )) ∪ ((ab ) ∩ a ))) = ((((ab) ∪ (ab)) ∩ ((ab) ∪ (ab ))) ∪ (((ab) ∪ (ab)) ∩ ((ab ) ∩ a )))
48 an4 86 . . . . . . . . . . 11 ((ab) ∩ (ab )) = ((aa) ∩ (bb ))
49 dff 101 . . . . . . . . . . . . . 14 0 = (bb )
5049ax-r1 35 . . . . . . . . . . . . 13 (bb ) = 0
5150lan 77 . . . . . . . . . . . 12 ((aa) ∩ (bb )) = ((aa) ∩ 0)
52 an0 108 . . . . . . . . . . . 12 ((aa) ∩ 0) = 0
5351, 52ax-r2 36 . . . . . . . . . . 11 ((aa) ∩ (bb )) = 0
5448, 53ax-r2 36 . . . . . . . . . 10 ((ab) ∩ (ab )) = 0
5554lor 70 . . . . . . . . 9 ((ab) ∪ ((ab) ∩ (ab ))) = ((ab) ∪ 0)
5610comcom2 183 . . . . . . . . . . 11 (ab) C a
5756, 4com2an 484 . . . . . . . . . 10 (ab) C (ab)
584comcom2 183 . . . . . . . . . . 11 (ab) C b
5910, 58com2an 484 . . . . . . . . . 10 (ab) C (ab )
6057, 59fh3 471 . . . . . . . . 9 ((ab) ∪ ((ab) ∩ (ab ))) = (((ab) ∪ (ab)) ∩ ((ab) ∪ (ab )))
61 or0 102 . . . . . . . . 9 ((ab) ∪ 0) = (ab)
6255, 60, 613tr2 64 . . . . . . . 8 (((ab) ∪ (ab)) ∩ ((ab) ∪ (ab ))) = (ab)
6310, 58com2or 483 . . . . . . . . . . 11 (ab) C (ab )
6463, 56com2an 484 . . . . . . . . . 10 (ab) C ((ab ) ∩ a )
6564, 57fh2r 474 . . . . . . . . 9 (((ab) ∪ (ab)) ∩ ((ab ) ∩ a )) = (((ab) ∩ ((ab ) ∩ a )) ∪ ((ab) ∩ ((ab ) ∩ a )))
66 an12 81 . . . . . . . . . . . 12 ((ab) ∩ ((ab ) ∩ a )) = ((ab ) ∩ ((ab) ∩ a ))
67 an32 83 . . . . . . . . . . . . . . 15 ((ab) ∩ a ) = ((aa ) ∩ b)
68 ancom 74 . . . . . . . . . . . . . . . 16 ((aa ) ∩ b) = (b ∩ (aa ))
69 dff 101 . . . . . . . . . . . . . . . . . . 19 0 = (aa )
7069ax-r1 35 . . . . . . . . . . . . . . . . . 18 (aa ) = 0
7170lan 77 . . . . . . . . . . . . . . . . 17 (b ∩ (aa )) = (b ∩ 0)
72 an0 108 . . . . . . . . . . . . . . . . 17 (b ∩ 0) = 0
7371, 72ax-r2 36 . . . . . . . . . . . . . . . 16 (b ∩ (aa )) = 0
7468, 73ax-r2 36 . . . . . . . . . . . . . . 15 ((aa ) ∩ b) = 0
7567, 74ax-r2 36 . . . . . . . . . . . . . 14 ((ab) ∩ a ) = 0
7675lan 77 . . . . . . . . . . . . 13 ((ab ) ∩ ((ab) ∩ a )) = ((ab ) ∩ 0)
77 an0 108 . . . . . . . . . . . . 13 ((ab ) ∩ 0) = 0
7876, 77ax-r2 36 . . . . . . . . . . . 12 ((ab ) ∩ ((ab) ∩ a )) = 0
7966, 78ax-r2 36 . . . . . . . . . . 11 ((ab) ∩ ((ab ) ∩ a )) = 0
80 ancom 74 . . . . . . . . . . . 12 (((ab) ∩ (ab )) ∩ a ) = (a ∩ ((ab) ∩ (ab )))
81 anass 76 . . . . . . . . . . . 12 (((ab) ∩ (ab )) ∩ a ) = ((ab) ∩ ((ab ) ∩ a ))
82 anor2 89 . . . . . . . . . . . . . . . . . 18 (ab) = (ab )
8382ax-r1 35 . . . . . . . . . . . . . . . . 17 (ab ) = (ab)
8483con3 68 . . . . . . . . . . . . . . . 16 (ab ) = (ab)
8584lan 77 . . . . . . . . . . . . . . 15 ((ab) ∩ (ab )) = ((ab) ∩ (ab) )
86 dff 101 . . . . . . . . . . . . . . . 16 0 = ((ab) ∩ (ab) )
8786ax-r1 35 . . . . . . . . . . . . . . 15 ((ab) ∩ (ab) ) = 0
8885, 87ax-r2 36 . . . . . . . . . . . . . 14 ((ab) ∩ (ab )) = 0
8988lan 77 . . . . . . . . . . . . 13 (a ∩ ((ab) ∩ (ab ))) = (a ∩ 0)
90 an0 108 . . . . . . . . . . . . 13 (a ∩ 0) = 0
9189, 90ax-r2 36 . . . . . . . . . . . 12 (a ∩ ((ab) ∩ (ab ))) = 0
9280, 81, 913tr2 64 . . . . . . . . . . 11 ((ab) ∩ ((ab ) ∩ a )) = 0
9379, 922or 72 . . . . . . . . . 10 (((ab) ∩ ((ab ) ∩ a )) ∪ ((ab) ∩ ((ab ) ∩ a ))) = (0 ∪ 0)
94 or0 102 . . . . . . . . . 10 (0 ∪ 0) = 0
9593, 94ax-r2 36 . . . . . . . . 9 (((ab) ∩ ((ab ) ∩ a )) ∪ ((ab) ∩ ((ab ) ∩ a ))) = 0
9665, 95ax-r2 36 . . . . . . . 8 (((ab) ∪ (ab)) ∩ ((ab ) ∩ a )) = 0
9762, 962or 72 . . . . . . 7 ((((ab) ∪ (ab)) ∩ ((ab) ∪ (ab ))) ∪ (((ab) ∪ (ab)) ∩ ((ab ) ∩ a ))) = ((ab) ∪ 0)
9847, 97ax-r2 36 . . . . . 6 (((ab) ∪ (ab)) ∩ (((ab) ∪ (ab )) ∪ ((ab ) ∩ a ))) = ((ab) ∪ 0)
9941, 98ax-r2 36 . . . . 5 (((ab) ∪ (ab)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((ab) ∪ 0)
10099, 61ax-r2 36 . . . 4 (((ab) ∪ (ab)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (ab)
101 coman2 186 . . . . . . . . . . . 12 (ba) C a
102101comcom 453 . . . . . . . . . . 11 a C (ba)
103 coman2 186 . . . . . . . . . . . 12 (ba) C a
104103comcom 453 . . . . . . . . . . 11 a C (ba)
105102, 104com2or 483 . . . . . . . . . 10 a C ((ba) ∪ (ba))
106105comcom3 454 . . . . . . . . 9 a C ((ba) ∪ (ba))
107106comcom 453 . . . . . . . 8 ((ba) ∪ (ba)) C a
108 coman1 185 . . . . . . . . . . 11 (ba) C b
109108comcom 453 . . . . . . . . . 10 b C (ba)
110 coman1 185 . . . . . . . . . . . . 13 (ba) C b
111110comcom 453 . . . . . . . . . . . 12 b C (ba)
112111comcom2 183 . . . . . . . . . . 11 b C (ba)
113112comcom5 458 . . . . . . . . . 10 b C (ba)
114109, 113com2or 483 . . . . . . . . 9 b C ((ba) ∪ (ba))
115114comcom 453 . . . . . . . 8 ((ba) ∪ (ba)) C b
116107, 115com2or 483 . . . . . . 7 ((ba) ∪ (ba)) C (ab)
117109comcom3 454 . . . . . . . . 9 b C (ba)
118117, 111com2or 483 . . . . . . . 8 b C ((ba) ∪ (ba))
119118comcom 453 . . . . . . 7 ((ba) ∪ (ba)) C b
120116, 119com2an 484 . . . . . 6 ((ba) ∪ (ba)) C ((ab) ∩ b )
121105comcom 453 . . . . . . . 8 ((ba) ∪ (ba)) C a
122119, 121com2or 483 . . . . . . 7 ((ba) ∪ (ba)) C (ba)
123102comcom3 454 . . . . . . . . 9 a C (ba)
124104comcom3 454 . . . . . . . . 9 a C (ba)
125123, 124com2or 483 . . . . . . . 8 a C ((ba) ∪ (ba))
126125comcom 453 . . . . . . 7 ((ba) ∪ (ba)) C a
127122, 126com2an 484 . . . . . 6 ((ba) ∪ (ba)) C ((ba) ∩ a )
128120, 127fh2 470 . . . . 5 (((ab) ∩ b ) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((((ab) ∩ b ) ∩ ((ba) ∪ (ba))) ∪ (((ab) ∩ b ) ∩ ((ba) ∩ a )))
129 lea 160 . . . . . . . . . . . . 13 (ba) ≤ b
130129lecon 154 . . . . . . . . . . . 12 b ≤ (ba)
131130lelan 167 . . . . . . . . . . 11 ((ab) ∩ b ) ≤ ((ab) ∩ (ba) )
132131lecon 154 . . . . . . . . . 10 ((ab) ∩ (ba) ) ≤ ((ab) ∩ b )
133132lelan 167 . . . . . . . . 9 (((ab) ∩ b ) ∩ ((ab) ∩ (ba) ) ) ≤ (((ab) ∩ b ) ∩ ((ab) ∩ b ) )
134 ax-a2 31 . . . . . . . . . . 11 ((ba) ∪ (ba)) = ((ba) ∪ (ba))
135 oran 87 . . . . . . . . . . . 12 ((ba) ∪ (ba)) = ((ba) ∩ (ba) )
136 anor1 88 . . . . . . . . . . . . . . . 16 (ab ) = (ab)
13736, 136ax-r2 36 . . . . . . . . . . . . . . 15 (ba) = (ab)
138137con2 67 . . . . . . . . . . . . . 14 (ba) = (ab)
139138ran 78 . . . . . . . . . . . . 13 ((ba) ∩ (ba) ) = ((ab) ∩ (ba) )
140139ax-r4 37 . . . . . . . . . . . 12 ((ba) ∩ (ba) ) = ((ab) ∩ (ba) )
141135, 140ax-r2 36 . . . . . . . . . . 11 ((ba) ∪ (ba)) = ((ab) ∩ (ba) )
142134, 141ax-r2 36 . . . . . . . . . 10 ((ba) ∪ (ba)) = ((ab) ∩ (ba) )
143142lan 77 . . . . . . . . 9 (((ab) ∩ b ) ∩ ((ba) ∪ (ba))) = (((ab) ∩ b ) ∩ ((ab) ∩ (ba) ) )
144 dff 101 . . . . . . . . 9 0 = (((ab) ∩ b ) ∩ ((ab) ∩ b ) )
145133, 143, 144le3tr1 140 . . . . . . . 8 (((ab) ∩ b ) ∩ ((ba) ∪ (ba))) ≤ 0
146 le0 147 . . . . . . . 8 0 ≤ (((ab) ∩ b ) ∩ ((ba) ∪ (ba)))
147145, 146lebi 145 . . . . . . 7 (((ab) ∩ b ) ∩ ((ba) ∪ (ba))) = 0
148 an4 86 . . . . . . . 8 (((ab) ∩ b ) ∩ ((ba) ∩ a )) = (((ab) ∩ (ba)) ∩ (ba ))
149 ancom 74 . . . . . . . . . 10 (((ab) ∩ (ba)) ∩ (ba )) = ((ba ) ∩ ((ab) ∩ (ba)))
150 ancom 74 . . . . . . . . . . . 12 ((ab) ∩ (ba)) = ((ba) ∩ (ab))
151150lan 77 . . . . . . . . . . 11 ((ba ) ∩ ((ab) ∩ (ba))) = ((ba ) ∩ ((ba) ∩ (ab)))
152 leo 158 . . . . . . . . . . . . 13 b ≤ (ba)
153 leo 158 . . . . . . . . . . . . 13 a ≤ (ab)
154152, 153le2an 169 . . . . . . . . . . . 12 (ba ) ≤ ((ba) ∩ (ab))
155154df2le2 136 . . . . . . . . . . 11 ((ba ) ∩ ((ba) ∩ (ab))) = (ba )
156151, 155ax-r2 36 . . . . . . . . . 10 ((ba ) ∩ ((ab) ∩ (ba))) = (ba )
157149, 156ax-r2 36 . . . . . . . . 9 (((ab) ∩ (ba)) ∩ (ba )) = (ba )
158 ancom 74 . . . . . . . . 9 (ba ) = (ab )
159157, 158ax-r2 36 . . . . . . . 8 (((ab) ∩ (ba)) ∩ (ba )) = (ab )
160148, 159ax-r2 36 . . . . . . 7 (((ab) ∩ b ) ∩ ((ba) ∩ a )) = (ab )
161147, 1602or 72 . . . . . 6 ((((ab) ∩ b ) ∩ ((ba) ∪ (ba))) ∪ (((ab) ∩ b ) ∩ ((ba) ∩ a ))) = (0 ∪ (ab ))
162 ax-a2 31 . . . . . . 7 (0 ∪ (ab )) = ((ab ) ∪ 0)
163 or0 102 . . . . . . 7 ((ab ) ∪ 0) = (ab )
164162, 163ax-r2 36 . . . . . 6 (0 ∪ (ab )) = (ab )
165161, 164ax-r2 36 . . . . 5 ((((ab) ∩ b ) ∩ ((ba) ∪ (ba))) ∪ (((ab) ∩ b ) ∩ ((ba) ∩ a ))) = (ab )
166128, 165ax-r2 36 . . . 4 (((ab) ∩ b ) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (ab )
167100, 1662or 72 . . 3 ((((ab) ∪ (ab)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∪ (((ab) ∩ b ) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))) = ((ab) ∪ (ab ))
16834, 167ax-r2 36 . 2 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((ab) ∪ (ab ))
1693, 168ax-r2 36 1 ((a4 b) ∩ (b4 a)) = ((ab) ∪ (ab ))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  0wf 9  4 wi4 15
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-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud4lem1  581  u4lembi  724
  Copyright terms: Public domain W3C validator