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

Theorem ud4lem1c 579
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud4lem1c ((a4 b) ∪ (b4 a)) = (ab )

Proof of Theorem ud4lem1c
StepHypRef Expression
1 ud4lem0c 280 . . 3 (a4 b) = (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))
2 df-i4 47 . . 3 (b4 a) = (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))
31, 22or 72 . 2 ((a4 b) ∪ (b4 a)) = ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))
4 comor2 462 . . . . . . . . . . . 12 (ab ) C b
54comcom3 454 . . . . . . . . . . 11 (ab ) C b
65comcom5 458 . . . . . . . . . 10 (ab ) C b
7 comor1 461 . . . . . . . . . . . 12 (ab ) C a
87comcom3 454 . . . . . . . . . . 11 (ab ) C a
98comcom5 458 . . . . . . . . . 10 (ab ) C a
106, 9com2an 484 . . . . . . . . 9 (ab ) C (ba)
114, 9com2an 484 . . . . . . . . 9 (ab ) C (ba)
1210, 11com2or 483 . . . . . . . 8 (ab ) C ((ba) ∪ (ba))
1312comcom 453 . . . . . . 7 ((ba) ∪ (ba)) C (ab )
14 comor2 462 . . . . . . . . . . . 12 (ab ) C b
1514comcom3 454 . . . . . . . . . . 11 (ab ) C b
1615comcom5 458 . . . . . . . . . 10 (ab ) C b
17 comor1 461 . . . . . . . . . 10 (ab ) C a
1816, 17com2an 484 . . . . . . . . 9 (ab ) C (ba)
1914, 17com2an 484 . . . . . . . . 9 (ab ) C (ba)
2018, 19com2or 483 . . . . . . . 8 (ab ) C ((ba) ∪ (ba))
2120comcom 453 . . . . . . 7 ((ba) ∪ (ba)) C (ab )
2213, 21com2an 484 . . . . . 6 ((ba) ∪ (ba)) C ((ab ) ∩ (ab ))
2322comcom 453 . . . . 5 ((ab ) ∩ (ab )) C ((ba) ∪ (ba))
24 comor2 462 . . . . . . . . . 10 (ba) C a
2524comcom2 183 . . . . . . . . 9 (ba) C a
26 comor1 461 . . . . . . . . 9 (ba) C b
2725, 26com2or 483 . . . . . . . 8 (ba) C (ab )
2825comcom3 454 . . . . . . . . . 10 (ba) C a
2928comcom5 458 . . . . . . . . 9 (ba) C a
3029, 26com2or 483 . . . . . . . 8 (ba) C (ab )
3127, 30com2an 484 . . . . . . 7 (ba) C ((ab ) ∩ (ab ))
3231comcom 453 . . . . . 6 ((ab ) ∩ (ab )) C (ba)
33 comorr 184 . . . . . . . 8 a C (ab )
34 comorr 184 . . . . . . . . 9 a C (ab )
3534comcom3 454 . . . . . . . 8 a C (ab )
3633, 35com2an 484 . . . . . . 7 a C ((ab ) ∩ (ab ))
3736comcom 453 . . . . . 6 ((ab ) ∩ (ab )) C a
3832, 37com2an 484 . . . . 5 ((ab ) ∩ (ab )) C ((ba) ∩ a )
3923, 38com2or 483 . . . 4 ((ab ) ∩ (ab )) C (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))
40 coman1 185 . . . . . . . . 9 (ab ) C a
4140comcom2 183 . . . . . . . 8 (ab ) C a
42 coman2 186 . . . . . . . 8 (ab ) C b
4341, 42com2or 483 . . . . . . 7 (ab ) C (ab )
4440, 42com2or 483 . . . . . . 7 (ab ) C (ab )
4543, 44com2an 484 . . . . . 6 (ab ) C ((ab ) ∩ (ab ))
4645comcom 453 . . . . 5 ((ab ) ∩ (ab )) C (ab )
474comcom 453 . . . . . . . . 9 b C (ab )
4814comcom 453 . . . . . . . . 9 b C (ab )
4947, 48com2an 484 . . . . . . . 8 b C ((ab ) ∩ (ab ))
5049comcom 453 . . . . . . 7 ((ab ) ∩ (ab )) C b
5150comcom3 454 . . . . . 6 ((ab ) ∩ (ab )) C b
5251comcom5 458 . . . . 5 ((ab ) ∩ (ab )) C b
5346, 52com2or 483 . . . 4 ((ab ) ∩ (ab )) C ((ab ) ∪ b)
5439, 53fh4r 476 . . 3 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((((ab ) ∩ (ab )) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∩ (((ab ) ∪ b) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))))
55 coman2 186 . . . . . . . . . . . 12 (ba) C a
5655comcom2 183 . . . . . . . . . . 11 (ba) C a
57 coman1 185 . . . . . . . . . . . 12 (ba) C b
5857comcom2 183 . . . . . . . . . . 11 (ba) C b
5956, 58com2or 483 . . . . . . . . . 10 (ba) C (ab )
6059comcom 453 . . . . . . . . 9 (ab ) C (ba)
61 coman2 186 . . . . . . . . . . . 12 (ba) C a
6261comcom2 183 . . . . . . . . . . 11 (ba) C a
63 coman1 185 . . . . . . . . . . 11 (ba) C b
6462, 63com2or 483 . . . . . . . . . 10 (ba) C (ab )
6564comcom 453 . . . . . . . . 9 (ab ) C (ba)
6660, 65com2or 483 . . . . . . . 8 (ab ) C ((ba) ∪ (ba))
6727comcom 453 . . . . . . . . 9 (ab ) C (ba)
6867, 7com2an 484 . . . . . . . 8 (ab ) C ((ba) ∩ a )
6966, 68com2or 483 . . . . . . 7 (ab ) C (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))
7017comcom2 183 . . . . . . . . 9 (ab ) C a
7170, 14com2or 483 . . . . . . . 8 (ab ) C (ab )
7271comcom 453 . . . . . . 7 (ab ) C (ab )
7369, 72fh4r 476 . . . . . 6 (((ab ) ∩ (ab )) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∩ ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))))
74 ax-a2 31 . . . . . . . . . . 11 (((ab ) ∪ (ba)) ∪ (ba)) = ((ba) ∪ ((ab ) ∪ (ba)))
75 ax-a3 32 . . . . . . . . . . 11 (((ab ) ∪ (ba)) ∪ (ba)) = ((ab ) ∪ ((ba) ∪ (ba)))
76 ax-a2 31 . . . . . . . . . . . . . . 15 (ab ) = (ba )
77 df-a 40 . . . . . . . . . . . . . . 15 (ba) = (ba )
7876, 772or 72 . . . . . . . . . . . . . 14 ((ab ) ∪ (ba)) = ((ba ) ∪ (ba ) )
79 df-t 41 . . . . . . . . . . . . . . 15 1 = ((ba ) ∪ (ba ) )
8079ax-r1 35 . . . . . . . . . . . . . 14 ((ba ) ∪ (ba ) ) = 1
8178, 80ax-r2 36 . . . . . . . . . . . . 13 ((ab ) ∪ (ba)) = 1
8281lor 70 . . . . . . . . . . . 12 ((ba) ∪ ((ab ) ∪ (ba))) = ((ba) ∪ 1)
83 or1 104 . . . . . . . . . . . 12 ((ba) ∪ 1) = 1
8482, 83ax-r2 36 . . . . . . . . . . 11 ((ba) ∪ ((ab ) ∪ (ba))) = 1
8574, 75, 843tr2 64 . . . . . . . . . 10 ((ab ) ∪ ((ba) ∪ (ba))) = 1
8685ax-r5 38 . . . . . . . . 9 (((ab ) ∪ ((ba) ∪ (ba))) ∪ ((ba) ∩ a )) = (1 ∪ ((ba) ∩ a ))
87 ax-a3 32 . . . . . . . . 9 (((ab ) ∪ ((ba) ∪ (ba))) ∪ ((ba) ∩ a )) = ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))
88 ax-a2 31 . . . . . . . . . 10 (1 ∪ ((ba) ∩ a )) = (((ba) ∩ a ) ∪ 1)
89 or1 104 . . . . . . . . . 10 (((ba) ∩ a ) ∪ 1) = 1
9088, 89ax-r2 36 . . . . . . . . 9 (1 ∪ ((ba) ∩ a )) = 1
9186, 87, 903tr2 64 . . . . . . . 8 ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = 1
92 ax-a2 31 . . . . . . . . 9 ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ∪ (ab ))
93 lear 161 . . . . . . . . . . . . 13 (ba) ≤ a
94 lear 161 . . . . . . . . . . . . 13 (ba) ≤ a
9593, 94lel2or 170 . . . . . . . . . . . 12 ((ba) ∪ (ba)) ≤ a
96 leo 158 . . . . . . . . . . . 12 a ≤ (ab )
9795, 96letr 137 . . . . . . . . . . 11 ((ba) ∪ (ba)) ≤ (ab )
98 lea 160 . . . . . . . . . . . 12 ((ba) ∩ a ) ≤ (ba)
99 ax-a2 31 . . . . . . . . . . . 12 (ba) = (ab )
10098, 99lbtr 139 . . . . . . . . . . 11 ((ba) ∩ a ) ≤ (ab )
10197, 100lel2or 170 . . . . . . . . . 10 (((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ≤ (ab )
102101df-le2 131 . . . . . . . . 9 ((((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ∪ (ab )) = (ab )
10392, 102ax-r2 36 . . . . . . . 8 ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (ab )
10491, 1032an 79 . . . . . . 7 (((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∩ ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))) = (1 ∩ (ab ))
105 ancom 74 . . . . . . . 8 (1 ∩ (ab )) = ((ab ) ∩ 1)
106 an1 106 . . . . . . . 8 ((ab ) ∩ 1) = (ab )
107105, 106ax-r2 36 . . . . . . 7 (1 ∩ (ab )) = (ab )
108104, 107ax-r2 36 . . . . . 6 (((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∩ ((ab ) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))) = (ab )
10973, 108ax-r2 36 . . . . 5 (((ab ) ∩ (ab )) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (ab )
110 ax-a2 31 . . . . . 6 (((ab ) ∪ b) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = ((((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ∪ ((ab ) ∪ b))
111 or32 82 . . . . . . . 8 ((((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ∪ ((ab ) ∪ b)) = ((((ba) ∪ (ba)) ∪ ((ab ) ∪ b)) ∪ ((ba) ∩ a ))
112 or4 84 . . . . . . . . . 10 (((ba) ∪ (ba)) ∪ ((ab ) ∪ b)) = (((ba) ∪ (ab )) ∪ ((ba) ∪ b))
113112ax-r5 38 . . . . . . . . 9 ((((ba) ∪ (ba)) ∪ ((ab ) ∪ b)) ∪ ((ba) ∩ a )) = ((((ba) ∪ (ab )) ∪ ((ba) ∪ b)) ∪ ((ba) ∩ a ))
114 ax-a3 32 . . . . . . . . . 10 ((((ba) ∪ (ab )) ∪ ((ba) ∪ b)) ∪ ((ba) ∩ a )) = (((ba) ∪ (ab )) ∪ (((ba) ∪ b) ∪ ((ba) ∩ a )))
11526comcom3 454 . . . . . . . . . . . . . . . 16 (ba) C b
116115comcom5 458 . . . . . . . . . . . . . . 15 (ba) C b
117116, 25fh4 472 . . . . . . . . . . . . . 14 (b ∪ ((ba) ∩ a )) = ((b ∪ (ba)) ∩ (ba ))
118 df-t 41 . . . . . . . . . . . . . . . . . . 19 1 = (bb )
119118ax-r1 35 . . . . . . . . . . . . . . . . . 18 (bb ) = 1
120119ax-r5 38 . . . . . . . . . . . . . . . . 17 ((bb ) ∪ a) = (1 ∪ a)
121 ax-a3 32 . . . . . . . . . . . . . . . . 17 ((bb ) ∪ a) = (b ∪ (ba))
122 ax-a2 31 . . . . . . . . . . . . . . . . . 18 (1 ∪ a) = (a ∪ 1)
123 or1 104 . . . . . . . . . . . . . . . . . 18 (a ∪ 1) = 1
124122, 123ax-r2 36 . . . . . . . . . . . . . . . . 17 (1 ∪ a) = 1
125120, 121, 1243tr2 64 . . . . . . . . . . . . . . . 16 (b ∪ (ba)) = 1
126 anor2 89 . . . . . . . . . . . . . . . . . 18 (ba) = (ba )
127126con2 67 . . . . . . . . . . . . . . . . 17 (ba) = (ba )
128127ax-r1 35 . . . . . . . . . . . . . . . 16 (ba ) = (ba)
129125, 1282an 79 . . . . . . . . . . . . . . 15 ((b ∪ (ba)) ∩ (ba )) = (1 ∩ (ba) )
130 ancom 74 . . . . . . . . . . . . . . . 16 (1 ∩ (ba) ) = ((ba) ∩ 1)
131 an1 106 . . . . . . . . . . . . . . . 16 ((ba) ∩ 1) = (ba)
132130, 131ax-r2 36 . . . . . . . . . . . . . . 15 (1 ∩ (ba) ) = (ba)
133129, 132ax-r2 36 . . . . . . . . . . . . . 14 ((b ∪ (ba)) ∩ (ba )) = (ba)
134117, 133ax-r2 36 . . . . . . . . . . . . 13 (b ∪ ((ba) ∩ a )) = (ba)
135134lor 70 . . . . . . . . . . . 12 ((ba) ∪ (b ∪ ((ba) ∩ a ))) = ((ba) ∪ (ba) )
136 ax-a3 32 . . . . . . . . . . . 12 (((ba) ∪ b) ∪ ((ba) ∩ a )) = ((ba) ∪ (b ∪ ((ba) ∩ a )))
137 df-t 41 . . . . . . . . . . . 12 1 = ((ba) ∪ (ba) )
138135, 136, 1373tr1 63 . . . . . . . . . . 11 (((ba) ∪ b) ∪ ((ba) ∩ a )) = 1
139138lor 70 . . . . . . . . . 10 (((ba) ∪ (ab )) ∪ (((ba) ∪ b) ∪ ((ba) ∩ a ))) = (((ba) ∪ (ab )) ∪ 1)
140114, 139ax-r2 36 . . . . . . . . 9 ((((ba) ∪ (ab )) ∪ ((ba) ∪ b)) ∪ ((ba) ∩ a )) = (((ba) ∪ (ab )) ∪ 1)
141113, 140ax-r2 36 . . . . . . . 8 ((((ba) ∪ (ba)) ∪ ((ab ) ∪ b)) ∪ ((ba) ∩ a )) = (((ba) ∪ (ab )) ∪ 1)
142111, 141ax-r2 36 . . . . . . 7 ((((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ∪ ((ab ) ∪ b)) = (((ba) ∪ (ab )) ∪ 1)
143 or1 104 . . . . . . 7 (((ba) ∪ (ab )) ∪ 1) = 1
144142, 143ax-r2 36 . . . . . 6 ((((ba) ∪ (ba)) ∪ ((ba) ∩ a )) ∪ ((ab ) ∪ b)) = 1
145110, 144ax-r2 36 . . . . 5 (((ab ) ∪ b) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = 1
146109, 1452an 79 . . . 4 ((((ab ) ∩ (ab )) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∩ (((ab ) ∪ b) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))) = ((ab ) ∩ 1)
147146, 106ax-r2 36 . . 3 ((((ab ) ∩ (ab )) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) ∩ (((ab ) ∪ b) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a )))) = (ab )
14854, 147ax-r2 36 . 2 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∪ (((ba) ∪ (ba)) ∪ ((ba) ∩ a ))) = (ab )
1493, 148ax-r2 36 1 ((a4 b) ∪ (b4 a)) = (ab )
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  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:  ud4lem1d  580
  Copyright terms: Public domain W3C validator