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

Theorem ud4lem1b 578
Description: Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
Assertion
Ref Expression
ud4lem1b ((a4 b) ∩ (b4 a)) = (ab )

Proof of Theorem ud4lem1b
StepHypRef Expression
1 ud4lem0c 280 . . 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 . . . . . . . . . . 11 (ba) C a
54comcom2 183 . . . . . . . . . 10 (ba) C a
6 coman1 185 . . . . . . . . . . 11 (ba) C b
76comcom2 183 . . . . . . . . . 10 (ba) C b
85, 7com2or 483 . . . . . . . . 9 (ba) C (ab )
98comcom 453 . . . . . . . 8 (ab ) C (ba)
10 coman2 186 . . . . . . . . . . 11 (ba) C a
1110comcom2 183 . . . . . . . . . 10 (ba) C a
12 coman1 185 . . . . . . . . . 10 (ba) C b
1311, 12com2or 483 . . . . . . . . 9 (ba) C (ab )
1413comcom 453 . . . . . . . 8 (ab ) C (ba)
159, 14com2or 483 . . . . . . 7 (ab ) C ((ba) ∪ (ba))
1615comcom 453 . . . . . 6 ((ba) ∪ (ba)) C (ab )
174, 7com2or 483 . . . . . . . . 9 (ba) C (ab )
1817comcom 453 . . . . . . . 8 (ab ) C (ba)
19 comor2 462 . . . . . . . . 9 (ab ) C b
20 comor1 461 . . . . . . . . 9 (ab ) C a
2119, 20com2an 484 . . . . . . . 8 (ab ) C (ba)
2218, 21com2or 483 . . . . . . 7 (ab ) C ((ba) ∪ (ba))
2322comcom 453 . . . . . 6 ((ba) ∪ (ba)) C (ab )
2416, 23com2an 484 . . . . 5 ((ba) ∪ (ba)) C ((ab ) ∩ (ab ))
25 coman2 186 . . . . . . . . . . 11 (ab ) C b
2625comcom3 454 . . . . . . . . . 10 (ab ) C b
2726comcom5 458 . . . . . . . . 9 (ab ) C b
28 coman1 185 . . . . . . . . 9 (ab ) C a
2927, 28com2an 484 . . . . . . . 8 (ab ) C (ba)
3025, 28com2an 484 . . . . . . . 8 (ab ) C (ba)
3129, 30com2or 483 . . . . . . 7 (ab ) C ((ba) ∪ (ba))
3231comcom 453 . . . . . 6 ((ba) ∪ (ba)) C (ab )
336comcom 453 . . . . . . . 8 b C (ba)
3412comcom 453 . . . . . . . . . 10 b C (ba)
3534comcom2 183 . . . . . . . . 9 b C (ba)
3635comcom5 458 . . . . . . . 8 b C (ba)
3733, 36com2or 483 . . . . . . 7 b C ((ba) ∪ (ba))
3837comcom 453 . . . . . 6 ((ba) ∪ (ba)) C b
3932, 38com2or 483 . . . . 5 ((ba) ∪ (ba)) C ((ab ) ∪ b)
4024, 39com2an 484 . . . 4 ((ba) ∪ (ba)) C (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))
41 comor1 461 . . . . . . . . . 10 (ba) C b
4241comcom3 454 . . . . . . . . 9 (ba) C b
4342comcom5 458 . . . . . . . 8 (ba) C b
44 comor2 462 . . . . . . . 8 (ba) C a
4543, 44com2an 484 . . . . . . 7 (ba) C (ba)
4641, 44com2an 484 . . . . . . 7 (ba) C (ba)
4745, 46com2or 483 . . . . . 6 (ba) C ((ba) ∪ (ba))
4847comcom 453 . . . . 5 ((ba) ∪ (ba)) C (ba)
494comcom 453 . . . . . . . 8 a C (ba)
5010comcom 453 . . . . . . . 8 a C (ba)
5149, 50com2or 483 . . . . . . 7 a C ((ba) ∪ (ba))
5251comcom 453 . . . . . 6 ((ba) ∪ (ba)) C a
5352comcom2 183 . . . . 5 ((ba) ∪ (ba)) C a
5448, 53com2an 484 . . . 4 ((ba) ∪ (ba)) C ((ba) ∩ a )
5540, 54fh2 470 . . 3 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∪ (ba))) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∩ a )))
568, 17com2an 484 . . . . . . . 8 (ba) C ((ab ) ∩ (ab ))
574, 7com2an 484 . . . . . . . . 9 (ba) C (ab )
5857, 6com2or 483 . . . . . . . 8 (ba) C ((ab ) ∪ b)
5956, 58com2an 484 . . . . . . 7 (ba) C (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))
607, 4com2an 484 . . . . . . 7 (ba) C (ba)
6159, 60fh2 470 . . . . . 6 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∪ (ba))) = (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)))
62 an32 83 . . . . . . . . . 10 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) = ((((ab ) ∩ (ab )) ∩ (ba)) ∩ ((ab ) ∪ b))
63 an32 83 . . . . . . . . . . . . 13 (((ab ) ∩ (ab )) ∩ (ba)) = (((ab ) ∩ (ba)) ∩ (ab ))
64 ax-a2 31 . . . . . . . . . . . . . . . . 17 (ab ) = (ba )
65 df-a 40 . . . . . . . . . . . . . . . . 17 (ba) = (ba )
6664, 652an 79 . . . . . . . . . . . . . . . 16 ((ab ) ∩ (ba)) = ((ba ) ∩ (ba ) )
67 dff 101 . . . . . . . . . . . . . . . . 17 0 = ((ba ) ∩ (ba ) )
6867ax-r1 35 . . . . . . . . . . . . . . . 16 ((ba ) ∩ (ba ) ) = 0
6966, 68ax-r2 36 . . . . . . . . . . . . . . 15 ((ab ) ∩ (ba)) = 0
7069ran 78 . . . . . . . . . . . . . 14 (((ab ) ∩ (ba)) ∩ (ab )) = (0 ∩ (ab ))
71 ancom 74 . . . . . . . . . . . . . . 15 (0 ∩ (ab )) = ((ab ) ∩ 0)
72 an0 108 . . . . . . . . . . . . . . 15 ((ab ) ∩ 0) = 0
7371, 72ax-r2 36 . . . . . . . . . . . . . 14 (0 ∩ (ab )) = 0
7470, 73ax-r2 36 . . . . . . . . . . . . 13 (((ab ) ∩ (ba)) ∩ (ab )) = 0
7563, 74ax-r2 36 . . . . . . . . . . . 12 (((ab ) ∩ (ab )) ∩ (ba)) = 0
7675ran 78 . . . . . . . . . . 11 ((((ab ) ∩ (ab )) ∩ (ba)) ∩ ((ab ) ∪ b)) = (0 ∩ ((ab ) ∪ b))
77 ancom 74 . . . . . . . . . . . 12 (0 ∩ ((ab ) ∪ b)) = (((ab ) ∪ b) ∩ 0)
78 an0 108 . . . . . . . . . . . 12 (((ab ) ∪ b) ∩ 0) = 0
7977, 78ax-r2 36 . . . . . . . . . . 11 (0 ∩ ((ab ) ∪ b)) = 0
8076, 79ax-r2 36 . . . . . . . . . 10 ((((ab ) ∩ (ab )) ∩ (ba)) ∩ ((ab ) ∪ b)) = 0
8162, 80ax-r2 36 . . . . . . . . 9 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) = 0
82 lea 160 . . . . . . . . . . . . . 14 (ba) ≤ b
83 leor 159 . . . . . . . . . . . . . 14 b ≤ (ab )
8482, 83letr 137 . . . . . . . . . . . . 13 (ba) ≤ (ab )
85 lear 161 . . . . . . . . . . . . . 14 (ba) ≤ a
86 leo 158 . . . . . . . . . . . . . 14 a ≤ (ab )
8785, 86letr 137 . . . . . . . . . . . . 13 (ba) ≤ (ab )
8884, 87ler2an 173 . . . . . . . . . . . 12 (ba) ≤ ((ab ) ∩ (ab ))
89 ancom 74 . . . . . . . . . . . . 13 (ba) = (ab )
90 leo 158 . . . . . . . . . . . . 13 (ab ) ≤ ((ab ) ∪ b)
9189, 90bltr 138 . . . . . . . . . . . 12 (ba) ≤ ((ab ) ∪ b)
9288, 91ler2an 173 . . . . . . . . . . 11 (ba) ≤ (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))
9392df2le2 136 . . . . . . . . . 10 ((ba) ∩ (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))) = (ba)
94 ancom 74 . . . . . . . . . 10 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) = ((ba) ∩ (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)))
95 ancom 74 . . . . . . . . . 10 (ab ) = (ba)
9693, 94, 953tr1 63 . . . . . . . . 9 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) = (ab )
9781, 962or 72 . . . . . . . 8 (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba))) = (0 ∪ (ab ))
98 ax-a2 31 . . . . . . . 8 (0 ∪ (ab )) = ((ab ) ∪ 0)
9997, 98ax-r2 36 . . . . . . 7 (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba))) = ((ab ) ∪ 0)
100 or0 102 . . . . . . 7 ((ab ) ∪ 0) = (ab )
10199, 100ax-r2 36 . . . . . 6 (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ba))) = (ab )
10261, 101ax-r2 36 . . . . 5 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∪ (ba))) = (ab )
103 anass 76 . . . . . 6 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∩ a )) = (((ab ) ∩ (ab )) ∩ (((ab ) ∪ b) ∩ ((ba) ∩ a )))
10425, 28com2or 483 . . . . . . . . . . 11 (ab ) C (ba)
10528comcom2 183 . . . . . . . . . . 11 (ab ) C a
106104, 105com2an 484 . . . . . . . . . 10 (ab ) C ((ba) ∩ a )
107106, 27fh2r 474 . . . . . . . . 9 (((ab ) ∪ b) ∩ ((ba) ∩ a )) = (((ab ) ∩ ((ba) ∩ a )) ∪ (b ∩ ((ba) ∩ a )))
108 an12 81 . . . . . . . . . . . 12 ((ab ) ∩ ((ba) ∩ a )) = ((ba) ∩ ((ab ) ∩ a ))
109 an32 83 . . . . . . . . . . . . . . 15 ((ab ) ∩ a ) = ((aa ) ∩ b )
110 ancom 74 . . . . . . . . . . . . . . . 16 ((aa ) ∩ b ) = (b ∩ (aa ))
111 dff 101 . . . . . . . . . . . . . . . . . . 19 0 = (aa )
112111ax-r1 35 . . . . . . . . . . . . . . . . . 18 (aa ) = 0
113112lan 77 . . . . . . . . . . . . . . . . 17 (b ∩ (aa )) = (b ∩ 0)
114 an0 108 . . . . . . . . . . . . . . . . 17 (b ∩ 0) = 0
115113, 114ax-r2 36 . . . . . . . . . . . . . . . 16 (b ∩ (aa )) = 0
116110, 115ax-r2 36 . . . . . . . . . . . . . . 15 ((aa ) ∩ b ) = 0
117109, 116ax-r2 36 . . . . . . . . . . . . . 14 ((ab ) ∩ a ) = 0
118117lan 77 . . . . . . . . . . . . 13 ((ba) ∩ ((ab ) ∩ a )) = ((ba) ∩ 0)
119 an0 108 . . . . . . . . . . . . 13 ((ba) ∩ 0) = 0
120118, 119ax-r2 36 . . . . . . . . . . . 12 ((ba) ∩ ((ab ) ∩ a )) = 0
121108, 120ax-r2 36 . . . . . . . . . . 11 ((ab ) ∩ ((ba) ∩ a )) = 0
122 anor1 88 . . . . . . . . . . . . 13 (ba ) = (ba)
123122lan 77 . . . . . . . . . . . 12 ((ba) ∩ (ba )) = ((ba) ∩ (ba) )
124 an12 81 . . . . . . . . . . . 12 (b ∩ ((ba) ∩ a )) = ((ba) ∩ (ba ))
125 dff 101 . . . . . . . . . . . 12 0 = ((ba) ∩ (ba) )
126123, 124, 1253tr1 63 . . . . . . . . . . 11 (b ∩ ((ba) ∩ a )) = 0
127121, 1262or 72 . . . . . . . . . 10 (((ab ) ∩ ((ba) ∩ a )) ∪ (b ∩ ((ba) ∩ a ))) = (0 ∪ 0)
128 or0 102 . . . . . . . . . 10 (0 ∪ 0) = 0
129127, 128ax-r2 36 . . . . . . . . 9 (((ab ) ∩ ((ba) ∩ a )) ∪ (b ∩ ((ba) ∩ a ))) = 0
130107, 129ax-r2 36 . . . . . . . 8 (((ab ) ∪ b) ∩ ((ba) ∩ a )) = 0
131130lan 77 . . . . . . 7 (((ab ) ∩ (ab )) ∩ (((ab ) ∪ b) ∩ ((ba) ∩ a ))) = (((ab ) ∩ (ab )) ∩ 0)
132 an0 108 . . . . . . 7 (((ab ) ∩ (ab )) ∩ 0) = 0
133131, 132ax-r2 36 . . . . . 6 (((ab ) ∩ (ab )) ∩ (((ab ) ∪ b) ∩ ((ba) ∩ a ))) = 0
134103, 133ax-r2 36 . . . . 5 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∩ a )) = 0
135102, 1342or 72 . . . 4 (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∪ (ba))) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∩ a ))) = ((ab ) ∪ 0)
136135, 100ax-r2 36 . . 3 (((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∪ (ba))) ∪ ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ ((ba) ∩ a ))) = (ab )
13755, 136ax-r2 36 . 2 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (ab )
1383, 137ax-r2 36 1 ((a4 b) ∩ (b4 a)) = (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
  Copyright terms: Public domain W3C validator