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

Theorem ud5lem1a 586
Description: Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
Assertion
Ref Expression
ud5lem1a ((a5 b) ∩ (b5 a)) = ((ab) ∪ (ab ))

Proof of Theorem ud5lem1a
StepHypRef Expression
1 df-i5 48 . . 3 (a5 b) = (((ab) ∪ (ab)) ∪ (ab ))
2 df-i5 48 . . 3 (b5 a) = (((ba) ∪ (ba)) ∪ (ba ))
31, 22an 79 . 2 ((a5 b) ∩ (b5 a)) = ((((ab) ∪ (ab)) ∪ (ab )) ∩ (((ba) ∪ (ba)) ∪ (ba )))
4 ax-a2 31 . . . 4 (((ba) ∪ (ba)) ∪ (ba )) = ((ba ) ∪ ((ba) ∪ (ba)))
54lan 77 . . 3 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (((ba) ∪ (ba)) ∪ (ba ))) = ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba ) ∪ ((ba) ∪ (ba))))
6 coman2 186 . . . . . . . . . 10 (ab) C b
76comcom2 183 . . . . . . . . 9 (ab) C b
8 coman1 185 . . . . . . . . . 10 (ab) C a
98comcom2 183 . . . . . . . . 9 (ab) C a
107, 9com2an 484 . . . . . . . 8 (ab) C (ba )
1110comcom 453 . . . . . . 7 (ba ) C (ab)
12 coman2 186 . . . . . . . . . 10 (ab) C b
1312comcom2 183 . . . . . . . . 9 (ab) C b
14 coman1 185 . . . . . . . . 9 (ab) C a
1513, 14com2an 484 . . . . . . . 8 (ab) C (ba )
1615comcom 453 . . . . . . 7 (ba ) C (ab)
1711, 16com2or 483 . . . . . 6 (ba ) C ((ab) ∪ (ab))
18 coman2 186 . . . . . . 7 (ba ) C a
19 coman1 185 . . . . . . 7 (ba ) C b
2018, 19com2an 484 . . . . . 6 (ba ) C (ab )
2117, 20com2or 483 . . . . 5 (ba ) C (((ab) ∪ (ab)) ∪ (ab ))
22 coman1 185 . . . . . . . . 9 (ba) C b
2322comcom2 183 . . . . . . . 8 (ba) C b
24 coman2 186 . . . . . . . . 9 (ba) C a
2524comcom2 183 . . . . . . . 8 (ba) C a
2623, 25com2an 484 . . . . . . 7 (ba) C (ba )
2726comcom 453 . . . . . 6 (ba ) C (ba)
28 coman1 185 . . . . . . . 8 (ba) C b
29 coman2 186 . . . . . . . . 9 (ba) C a
3029comcom2 183 . . . . . . . 8 (ba) C a
3128, 30com2an 484 . . . . . . 7 (ba) C (ba )
3231comcom 453 . . . . . 6 (ba ) C (ba)
3327, 32com2or 483 . . . . 5 (ba ) C ((ba) ∪ (ba))
3421, 33fh2 470 . . . 4 ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba ) ∪ ((ba) ∪ (ba)))) = (((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba )) ∪ ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba) ∪ (ba))))
3518comcom3 454 . . . . . . . . . . 11 (ba ) C a
3635comcom5 458 . . . . . . . . . 10 (ba ) C a
3719comcom3 454 . . . . . . . . . . 11 (ba ) C b
3837comcom5 458 . . . . . . . . . 10 (ba ) C b
3936, 38com2an 484 . . . . . . . . 9 (ba ) C (ab)
4018, 38com2an 484 . . . . . . . . 9 (ba ) C (ab)
4139, 40com2or 483 . . . . . . . 8 (ba ) C ((ab) ∪ (ab))
4241, 20fh1r 473 . . . . . . 7 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba )) = ((((ab) ∪ (ab)) ∩ (ba )) ∪ ((ab ) ∩ (ba )))
4311, 16fh1r 473 . . . . . . . . . 10 (((ab) ∪ (ab)) ∩ (ba )) = (((ab) ∩ (ba )) ∪ ((ab) ∩ (ba )))
44 anass 76 . . . . . . . . . . . . 13 ((ab) ∩ (ba )) = (a ∩ (b ∩ (ba )))
45 anass 76 . . . . . . . . . . . . . . . 16 ((bb ) ∩ a ) = (b ∩ (ba ))
4645ax-r1 35 . . . . . . . . . . . . . . 15 (b ∩ (ba )) = ((bb ) ∩ a )
4746lan 77 . . . . . . . . . . . . . 14 (a ∩ (b ∩ (ba ))) = (a ∩ ((bb ) ∩ a ))
48 ancom 74 . . . . . . . . . . . . . . . . 17 ((bb ) ∩ a ) = (a ∩ (bb ))
49 dff 101 . . . . . . . . . . . . . . . . . . . 20 0 = (bb )
5049ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (bb ) = 0
5150lan 77 . . . . . . . . . . . . . . . . . 18 (a ∩ (bb )) = (a ∩ 0)
52 an0 108 . . . . . . . . . . . . . . . . . 18 (a ∩ 0) = 0
5351, 52ax-r2 36 . . . . . . . . . . . . . . . . 17 (a ∩ (bb )) = 0
5448, 53ax-r2 36 . . . . . . . . . . . . . . . 16 ((bb ) ∩ a ) = 0
5554lan 77 . . . . . . . . . . . . . . 15 (a ∩ ((bb ) ∩ a )) = (a ∩ 0)
56 an0 108 . . . . . . . . . . . . . . 15 (a ∩ 0) = 0
5755, 56ax-r2 36 . . . . . . . . . . . . . 14 (a ∩ ((bb ) ∩ a )) = 0
5847, 57ax-r2 36 . . . . . . . . . . . . 13 (a ∩ (b ∩ (ba ))) = 0
5944, 58ax-r2 36 . . . . . . . . . . . 12 ((ab) ∩ (ba )) = 0
60 anass 76 . . . . . . . . . . . . 13 ((ab) ∩ (ba )) = (a ∩ (b ∩ (ba )))
6146lan 77 . . . . . . . . . . . . . 14 (a ∩ (b ∩ (ba ))) = (a ∩ ((bb ) ∩ a ))
6254lan 77 . . . . . . . . . . . . . . 15 (a ∩ ((bb ) ∩ a )) = (a ∩ 0)
6362, 52ax-r2 36 . . . . . . . . . . . . . 14 (a ∩ ((bb ) ∩ a )) = 0
6461, 63ax-r2 36 . . . . . . . . . . . . 13 (a ∩ (b ∩ (ba ))) = 0
6560, 64ax-r2 36 . . . . . . . . . . . 12 ((ab) ∩ (ba )) = 0
6659, 652or 72 . . . . . . . . . . 11 (((ab) ∩ (ba )) ∪ ((ab) ∩ (ba ))) = (0 ∪ 0)
67 or0 102 . . . . . . . . . . 11 (0 ∪ 0) = 0
6866, 67ax-r2 36 . . . . . . . . . 10 (((ab) ∩ (ba )) ∪ ((ab) ∩ (ba ))) = 0
6943, 68ax-r2 36 . . . . . . . . 9 (((ab) ∪ (ab)) ∩ (ba )) = 0
70 ancom 74 . . . . . . . . . . 11 (ba ) = (ab )
7170lan 77 . . . . . . . . . 10 ((ab ) ∩ (ba )) = ((ab ) ∩ (ab ))
72 anidm 111 . . . . . . . . . 10 ((ab ) ∩ (ab )) = (ab )
7371, 72ax-r2 36 . . . . . . . . 9 ((ab ) ∩ (ba )) = (ab )
7469, 732or 72 . . . . . . . 8 ((((ab) ∪ (ab)) ∩ (ba )) ∪ ((ab ) ∩ (ba ))) = (0 ∪ (ab ))
75 ax-a2 31 . . . . . . . . 9 (0 ∪ (ab )) = ((ab ) ∪ 0)
76 or0 102 . . . . . . . . 9 ((ab ) ∪ 0) = (ab )
7775, 76ax-r2 36 . . . . . . . 8 (0 ∪ (ab )) = (ab )
7874, 77ax-r2 36 . . . . . . 7 ((((ab) ∪ (ab)) ∩ (ba )) ∪ ((ab ) ∩ (ba ))) = (ab )
7942, 78ax-r2 36 . . . . . 6 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba )) = (ab )
8024, 22com2an 484 . . . . . . . . . 10 (ba) C (ab)
8125, 22com2an 484 . . . . . . . . . 10 (ba) C (ab)
8280, 81com2or 483 . . . . . . . . 9 (ba) C ((ab) ∪ (ab))
8325, 23com2an 484 . . . . . . . . 9 (ba) C (ab )
8482, 83com2or 483 . . . . . . . 8 (ba) C (((ab) ∪ (ab)) ∪ (ab ))
8523, 24com2an 484 . . . . . . . 8 (ba) C (ba)
8684, 85fh2 470 . . . . . . 7 ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba) ∪ (ba))) = (((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) ∪ ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)))
8782, 83fh1r 473 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) = ((((ab) ∪ (ab)) ∩ (ba)) ∪ ((ab ) ∩ (ba)))
88 anass 76 . . . . . . . . . . . . 13 ((ab ) ∩ (ba)) = (a ∩ (b ∩ (ba)))
89 an12 81 . . . . . . . . . . . . . . . . 17 (b ∩ (ba)) = (b ∩ (ba))
9089ax-r1 35 . . . . . . . . . . . . . . . 16 (b ∩ (ba)) = (b ∩ (ba))
91 anass 76 . . . . . . . . . . . . . . . . . 18 ((bb ) ∩ a) = (b ∩ (ba))
9291ax-r1 35 . . . . . . . . . . . . . . . . 17 (b ∩ (ba)) = ((bb ) ∩ a)
93 ancom 74 . . . . . . . . . . . . . . . . . 18 ((bb ) ∩ a) = (a ∩ (bb ))
9450lan 77 . . . . . . . . . . . . . . . . . . 19 (a ∩ (bb )) = (a ∩ 0)
9594, 56ax-r2 36 . . . . . . . . . . . . . . . . . 18 (a ∩ (bb )) = 0
9693, 95ax-r2 36 . . . . . . . . . . . . . . . . 17 ((bb ) ∩ a) = 0
9792, 96ax-r2 36 . . . . . . . . . . . . . . . 16 (b ∩ (ba)) = 0
9890, 97ax-r2 36 . . . . . . . . . . . . . . 15 (b ∩ (ba)) = 0
9998lan 77 . . . . . . . . . . . . . 14 (a ∩ (b ∩ (ba))) = (a ∩ 0)
10099, 52ax-r2 36 . . . . . . . . . . . . 13 (a ∩ (b ∩ (ba))) = 0
10188, 100ax-r2 36 . . . . . . . . . . . 12 ((ab ) ∩ (ba)) = 0
102101lor 70 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∩ (ba)) ∪ ((ab ) ∩ (ba))) = ((((ab) ∪ (ab)) ∩ (ba)) ∪ 0)
103 or0 102 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∩ (ba)) ∪ 0) = (((ab) ∪ (ab)) ∩ (ba))
104102, 103ax-r2 36 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∩ (ba)) ∪ ((ab ) ∩ (ba))) = (((ab) ∪ (ab)) ∩ (ba))
10587, 104ax-r2 36 . . . . . . . . 9 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) = (((ab) ∪ (ab)) ∩ (ba))
10628comcom3 454 . . . . . . . . . . . . . 14 (ba) C b
107106comcom5 458 . . . . . . . . . . . . 13 (ba) C b
10829, 107com2an 484 . . . . . . . . . . . 12 (ba) C (ab)
10930, 107com2an 484 . . . . . . . . . . . 12 (ba) C (ab)
110108, 109com2or 483 . . . . . . . . . . 11 (ba) C ((ab) ∪ (ab))
11130, 28com2an 484 . . . . . . . . . . 11 (ba) C (ab )
112110, 111fh1r 473 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) = ((((ab) ∪ (ab)) ∩ (ba)) ∪ ((ab ) ∩ (ba)))
113 ancom 74 . . . . . . . . . . . . 13 ((ab ) ∩ (ba)) = ((ba) ∩ (ab ))
114 anass 76 . . . . . . . . . . . . . 14 ((ba) ∩ (ab )) = (b ∩ (a ∩ (ab )))
115 anass 76 . . . . . . . . . . . . . . . . . 18 ((aa ) ∩ b ) = (a ∩ (ab ))
116115ax-r1 35 . . . . . . . . . . . . . . . . 17 (a ∩ (ab )) = ((aa ) ∩ b )
117 ancom 74 . . . . . . . . . . . . . . . . . 18 ((aa ) ∩ b ) = (b ∩ (aa ))
118 dff 101 . . . . . . . . . . . . . . . . . . . . 21 0 = (aa )
119118ax-r1 35 . . . . . . . . . . . . . . . . . . . 20 (aa ) = 0
120119lan 77 . . . . . . . . . . . . . . . . . . 19 (b ∩ (aa )) = (b ∩ 0)
121 an0 108 . . . . . . . . . . . . . . . . . . 19 (b ∩ 0) = 0
122120, 121ax-r2 36 . . . . . . . . . . . . . . . . . 18 (b ∩ (aa )) = 0
123117, 122ax-r2 36 . . . . . . . . . . . . . . . . 17 ((aa ) ∩ b ) = 0
124116, 123ax-r2 36 . . . . . . . . . . . . . . . 16 (a ∩ (ab )) = 0
125124lan 77 . . . . . . . . . . . . . . 15 (b ∩ (a ∩ (ab ))) = (b ∩ 0)
126125, 121ax-r2 36 . . . . . . . . . . . . . 14 (b ∩ (a ∩ (ab ))) = 0
127114, 126ax-r2 36 . . . . . . . . . . . . 13 ((ba) ∩ (ab )) = 0
128113, 127ax-r2 36 . . . . . . . . . . . 12 ((ab ) ∩ (ba)) = 0
129128lor 70 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∩ (ba)) ∪ ((ab ) ∩ (ba))) = ((((ab) ∪ (ab)) ∩ (ba)) ∪ 0)
130 or0 102 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∩ (ba)) ∪ 0) = (((ab) ∪ (ab)) ∩ (ba))
131129, 130ax-r2 36 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∩ (ba)) ∪ ((ab ) ∩ (ba))) = (((ab) ∪ (ab)) ∩ (ba))
132112, 131ax-r2 36 . . . . . . . . 9 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) = (((ab) ∪ (ab)) ∩ (ba))
133105, 1322or 72 . . . . . . . 8 (((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) ∪ ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba))) = ((((ab) ∪ (ab)) ∩ (ba)) ∪ (((ab) ∪ (ab)) ∩ (ba)))
1347, 8com2an 484 . . . . . . . . . . . . 13 (ab) C (ba)
135134comcom 453 . . . . . . . . . . . 12 (ba) C (ab)
136135, 109fh1r 473 . . . . . . . . . . 11 (((ab) ∪ (ab)) ∩ (ba)) = (((ab) ∩ (ba)) ∪ ((ab) ∩ (ba)))
137 anass 76 . . . . . . . . . . . . . 14 ((ab) ∩ (ba)) = (a ∩ (b ∩ (ba)))
13897lan 77 . . . . . . . . . . . . . . 15 (a ∩ (b ∩ (ba))) = (a ∩ 0)
139138, 56ax-r2 36 . . . . . . . . . . . . . 14 (a ∩ (b ∩ (ba))) = 0
140137, 139ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∩ (ba)) = 0
141 anass 76 . . . . . . . . . . . . . 14 ((ab) ∩ (ba)) = (a ∩ (b ∩ (ba)))
14297lan 77 . . . . . . . . . . . . . . 15 (a ∩ (b ∩ (ba))) = (a ∩ 0)
143142, 52ax-r2 36 . . . . . . . . . . . . . 14 (a ∩ (b ∩ (ba))) = 0
144141, 143ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∩ (ba)) = 0
145140, 1442or 72 . . . . . . . . . . . 12 (((ab) ∩ (ba)) ∪ ((ab) ∩ (ba))) = (0 ∪ 0)
146145, 67ax-r2 36 . . . . . . . . . . 11 (((ab) ∩ (ba)) ∪ ((ab) ∩ (ba))) = 0
147136, 146ax-r2 36 . . . . . . . . . 10 (((ab) ∪ (ab)) ∩ (ba)) = 0
148147lor 70 . . . . . . . . 9 ((((ab) ∪ (ab)) ∩ (ba)) ∪ (((ab) ∪ (ab)) ∩ (ba))) = ((((ab) ∪ (ab)) ∩ (ba)) ∪ 0)
14980, 81fh1r 473 . . . . . . . . . . 11 (((ab) ∪ (ab)) ∩ (ba)) = (((ab) ∩ (ba)) ∪ ((ab) ∩ (ba)))
150 ancom 74 . . . . . . . . . . . . . . 15 (ba) = (ab)
151150lan 77 . . . . . . . . . . . . . 14 ((ab) ∩ (ba)) = ((ab) ∩ (ab))
152 anidm 111 . . . . . . . . . . . . . 14 ((ab) ∩ (ab)) = (ab)
153151, 152ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∩ (ba)) = (ab)
154 ancom 74 . . . . . . . . . . . . . 14 ((ab) ∩ (ba)) = ((ba) ∩ (ab))
155 anass 76 . . . . . . . . . . . . . . 15 ((ba) ∩ (ab)) = (b ∩ (a ∩ (ab)))
156 anass 76 . . . . . . . . . . . . . . . . . . . 20 ((aa ) ∩ b) = (a ∩ (ab))
157156ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (a ∩ (ab)) = ((aa ) ∩ b)
158119ran 78 . . . . . . . . . . . . . . . . . . . 20 ((aa ) ∩ b) = (0 ∩ b)
159 ancom 74 . . . . . . . . . . . . . . . . . . . 20 (0 ∩ b) = (b ∩ 0)
160158, 159ax-r2 36 . . . . . . . . . . . . . . . . . . 19 ((aa ) ∩ b) = (b ∩ 0)
161157, 160ax-r2 36 . . . . . . . . . . . . . . . . . 18 (a ∩ (ab)) = (b ∩ 0)
162 an0 108 . . . . . . . . . . . . . . . . . 18 (b ∩ 0) = 0
163161, 162ax-r2 36 . . . . . . . . . . . . . . . . 17 (a ∩ (ab)) = 0
164163lan 77 . . . . . . . . . . . . . . . 16 (b ∩ (a ∩ (ab))) = (b ∩ 0)
165164, 162ax-r2 36 . . . . . . . . . . . . . . 15 (b ∩ (a ∩ (ab))) = 0
166155, 165ax-r2 36 . . . . . . . . . . . . . 14 ((ba) ∩ (ab)) = 0
167154, 166ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∩ (ba)) = 0
168153, 1672or 72 . . . . . . . . . . . 12 (((ab) ∩ (ba)) ∪ ((ab) ∩ (ba))) = ((ab) ∪ 0)
169 or0 102 . . . . . . . . . . . 12 ((ab) ∪ 0) = (ab)
170168, 169ax-r2 36 . . . . . . . . . . 11 (((ab) ∩ (ba)) ∪ ((ab) ∩ (ba))) = (ab)
171149, 170ax-r2 36 . . . . . . . . . 10 (((ab) ∪ (ab)) ∩ (ba)) = (ab)
172103, 171ax-r2 36 . . . . . . . . 9 ((((ab) ∪ (ab)) ∩ (ba)) ∪ 0) = (ab)
173148, 172ax-r2 36 . . . . . . . 8 ((((ab) ∪ (ab)) ∩ (ba)) ∪ (((ab) ∪ (ab)) ∩ (ba))) = (ab)
174133, 173ax-r2 36 . . . . . . 7 (((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba)) ∪ ((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba))) = (ab)
17586, 174ax-r2 36 . . . . . 6 ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba) ∪ (ba))) = (ab)
17679, 1752or 72 . . . . 5 (((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba )) ∪ ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba) ∪ (ba)))) = ((ab ) ∪ (ab))
177 ax-a2 31 . . . . 5 ((ab ) ∪ (ab)) = ((ab) ∪ (ab ))
178176, 177ax-r2 36 . . . 4 (((((ab) ∪ (ab)) ∪ (ab )) ∩ (ba )) ∪ ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba) ∪ (ba)))) = ((ab) ∪ (ab ))
17934, 178ax-r2 36 . . 3 ((((ab) ∪ (ab)) ∪ (ab )) ∩ ((ba ) ∪ ((ba) ∪ (ba)))) = ((ab) ∪ (ab ))
1805, 179ax-r2 36 . 2 ((((ab) ∪ (ab)) ∪ (ab )) ∩ (((ba) ∪ (ba)) ∪ (ba ))) = ((ab) ∪ (ab ))
1813, 180ax-r2 36 1 ((a5 b) ∩ (b5 a)) = ((ab) ∪ (ab ))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  0wf 9  5 wi5 16
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-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud5lem1  589
  Copyright terms: Public domain W3C validator