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

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

Proof of Theorem ud3lem1c
StepHypRef Expression
1 ud3lem0c 279 . . 3 (a3 b) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
2 df-i3 46 . . 3 (b3 a) = (((ba) ∪ (ba )) ∪ (b ∩ (ba)))
31, 22or 72 . 2 ((a3 b) ∪ (b3 a)) = ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba))))
4 coman2 186 . . . . . . . . 9 (ba) C a
5 coman1 185 . . . . . . . . 9 (ba) C b
64, 5com2or 483 . . . . . . . 8 (ba) C (ab )
75comcom7 460 . . . . . . . . 9 (ba) C b
84, 7com2or 483 . . . . . . . 8 (ba) C (ab)
96, 8com2an 484 . . . . . . 7 (ba) C ((ab ) ∩ (ab))
109comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C (ba)
11 coman2 186 . . . . . . . . . 10 (ba ) C a
1211comcom7 460 . . . . . . . . 9 (ba ) C a
13 coman1 185 . . . . . . . . 9 (ba ) C b
1412, 13com2or 483 . . . . . . . 8 (ba ) C (ab )
1513comcom7 460 . . . . . . . . 9 (ba ) C b
1612, 15com2or 483 . . . . . . . 8 (ba ) C (ab)
1714, 16com2an 484 . . . . . . 7 (ba ) C ((ab ) ∩ (ab))
1817comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C (ba )
1910, 18com2or 483 . . . . 5 ((ab ) ∩ (ab)) C ((ba) ∪ (ba ))
20 comorr2 463 . . . . . . . . 9 b C (ab )
2120comcom6 459 . . . . . . . 8 b C (ab )
22 comorr2 463 . . . . . . . 8 b C (ab)
2321, 22com2an 484 . . . . . . 7 b C ((ab ) ∩ (ab))
2423comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C b
25 comor2 462 . . . . . . . . 9 (ba) C a
26 comor1 461 . . . . . . . . 9 (ba) C b
2725, 26com2or 483 . . . . . . . 8 (ba) C (ab )
2826comcom7 460 . . . . . . . . 9 (ba) C b
2925, 28com2or 483 . . . . . . . 8 (ba) C (ab)
3027, 29com2an 484 . . . . . . 7 (ba) C ((ab ) ∩ (ab))
3130comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C (ba)
3224, 31com2an 484 . . . . 5 ((ab ) ∩ (ab)) C (b ∩ (ba))
3319, 32com2or 483 . . . 4 ((ab ) ∩ (ab)) C (((ba) ∪ (ba )) ∪ (b ∩ (ba)))
34 comorr 184 . . . . . . . 8 a C (ab )
3534comcom3 454 . . . . . . 7 a C (ab )
36 comorr 184 . . . . . . . 8 a C (ab)
3736comcom3 454 . . . . . . 7 a C (ab)
3835, 37com2an 484 . . . . . 6 a C ((ab ) ∩ (ab))
3938comcom 453 . . . . 5 ((ab ) ∩ (ab)) C a
40 coman1 185 . . . . . . . 8 (ab ) C a
41 coman2 186 . . . . . . . 8 (ab ) C b
4240, 41com2or 483 . . . . . . 7 (ab ) C (ab )
4341comcom7 460 . . . . . . . 8 (ab ) C b
4440, 43com2or 483 . . . . . . 7 (ab ) C (ab)
4542, 44com2an 484 . . . . . 6 (ab ) C ((ab ) ∩ (ab))
4645comcom 453 . . . . 5 ((ab ) ∩ (ab)) C (ab )
4739, 46com2or 483 . . . 4 ((ab ) ∩ (ab)) C (a ∪ (ab ))
4833, 47fh4r 476 . . 3 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = ((((ab ) ∩ (ab)) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) ∩ ((a ∪ (ab )) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))))
49 comor2 462 . . . . . . . . . 10 (ab ) C b
50 comor1 461 . . . . . . . . . 10 (ab ) C a
5149, 50com2an 484 . . . . . . . . 9 (ab ) C (ba)
5250comcom2 183 . . . . . . . . . 10 (ab ) C a
5349, 52com2an 484 . . . . . . . . 9 (ab ) C (ba )
5451, 53com2or 483 . . . . . . . 8 (ab ) C ((ba) ∪ (ba ))
5549comcom7 460 . . . . . . . . 9 (ab ) C b
5649, 50com2or 483 . . . . . . . . 9 (ab ) C (ba)
5755, 56com2an 484 . . . . . . . 8 (ab ) C (b ∩ (ba))
5854, 57com2or 483 . . . . . . 7 (ab ) C (((ba) ∪ (ba )) ∪ (b ∩ (ba)))
5950, 55com2or 483 . . . . . . 7 (ab ) C (ab)
6058, 59fh4r 476 . . . . . 6 (((ab ) ∩ (ab)) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (((ab ) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) ∩ ((ab) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))))
61 ax-a2 31 . . . . . . . . 9 ((ab ) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = ((((ba) ∪ (ba )) ∪ (b ∩ (ba))) ∪ (ab ))
62 lea 160 . . . . . . . . . . . . 13 (ba) ≤ b
63 lea 160 . . . . . . . . . . . . 13 (ba ) ≤ b
6462, 63lel2or 170 . . . . . . . . . . . 12 ((ba) ∪ (ba )) ≤ b
65 leor 159 . . . . . . . . . . . 12 b ≤ (ab )
6664, 65letr 137 . . . . . . . . . . 11 ((ba) ∪ (ba )) ≤ (ab )
67 lear 161 . . . . . . . . . . . 12 (b ∩ (ba)) ≤ (ba)
68 ax-a2 31 . . . . . . . . . . . 12 (ba) = (ab )
6967, 68lbtr 139 . . . . . . . . . . 11 (b ∩ (ba)) ≤ (ab )
7066, 69lel2or 170 . . . . . . . . . 10 (((ba) ∪ (ba )) ∪ (b ∩ (ba))) ≤ (ab )
7170df-le2 131 . . . . . . . . 9 ((((ba) ∪ (ba )) ∪ (b ∩ (ba))) ∪ (ab )) = (ab )
7261, 71ax-r2 36 . . . . . . . 8 ((ab ) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (ab )
73 or12 80 . . . . . . . . 9 ((ab) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (((ba) ∪ (ba )) ∪ ((ab) ∪ (b ∩ (ba))))
74 ax-a3 32 . . . . . . . . . . 11 ((((ba) ∪ (ba )) ∪ (ab)) ∪ (b ∩ (ba))) = (((ba) ∪ (ba )) ∪ ((ab) ∪ (b ∩ (ba))))
7574ax-r1 35 . . . . . . . . . 10 (((ba) ∪ (ba )) ∪ ((ab) ∪ (b ∩ (ba)))) = ((((ba) ∪ (ba )) ∪ (ab)) ∪ (b ∩ (ba)))
76 ax-a3 32 . . . . . . . . . . . . 13 (((ba) ∪ (ba )) ∪ (ab)) = ((ba) ∪ ((ba ) ∪ (ab)))
77 ancom 74 . . . . . . . . . . . . . . . . 17 (ba ) = (ab )
78 oran 87 . . . . . . . . . . . . . . . . 17 (ab) = (ab )
7977, 782or 72 . . . . . . . . . . . . . . . 16 ((ba ) ∪ (ab)) = ((ab ) ∪ (ab ) )
80 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((ab ) ∪ (ab ) )
8180ax-r1 35 . . . . . . . . . . . . . . . 16 ((ab ) ∪ (ab ) ) = 1
8279, 81ax-r2 36 . . . . . . . . . . . . . . 15 ((ba ) ∪ (ab)) = 1
8382lor 70 . . . . . . . . . . . . . 14 ((ba) ∪ ((ba ) ∪ (ab))) = ((ba) ∪ 1)
84 or1 104 . . . . . . . . . . . . . 14 ((ba) ∪ 1) = 1
8583, 84ax-r2 36 . . . . . . . . . . . . 13 ((ba) ∪ ((ba ) ∪ (ab))) = 1
8676, 85ax-r2 36 . . . . . . . . . . . 12 (((ba) ∪ (ba )) ∪ (ab)) = 1
8786ax-r5 38 . . . . . . . . . . 11 ((((ba) ∪ (ba )) ∪ (ab)) ∪ (b ∩ (ba))) = (1 ∪ (b ∩ (ba)))
88 or1r 105 . . . . . . . . . . 11 (1 ∪ (b ∩ (ba))) = 1
8987, 88ax-r2 36 . . . . . . . . . 10 ((((ba) ∪ (ba )) ∪ (ab)) ∪ (b ∩ (ba))) = 1
9075, 89ax-r2 36 . . . . . . . . 9 (((ba) ∪ (ba )) ∪ ((ab) ∪ (b ∩ (ba)))) = 1
9173, 90ax-r2 36 . . . . . . . 8 ((ab) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = 1
9272, 912an 79 . . . . . . 7 (((ab ) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) ∩ ((ab) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba))))) = ((ab ) ∩ 1)
93 an1 106 . . . . . . 7 ((ab ) ∩ 1) = (ab )
9492, 93ax-r2 36 . . . . . 6 (((ab ) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) ∩ ((ab) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba))))) = (ab )
9560, 94ax-r2 36 . . . . 5 (((ab ) ∩ (ab)) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (ab )
96 or12 80 . . . . . 6 ((a ∪ (ab )) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (((ba) ∪ (ba )) ∪ ((a ∪ (ab )) ∪ (b ∩ (ba))))
97 ax-a2 31 . . . . . . . . . 10 (a ∪ (ab )) = ((ab ) ∪ a )
98 ancom 74 . . . . . . . . . 10 (b ∩ (ba)) = ((ba) ∩ b)
9997, 982or 72 . . . . . . . . 9 ((a ∪ (ab )) ∪ (b ∩ (ba))) = (((ab ) ∪ a ) ∪ ((ba) ∩ b))
100 ax-a3 32 . . . . . . . . . 10 (((ab ) ∪ a ) ∪ ((ba) ∩ b)) = ((ab ) ∪ (a ∪ ((ba) ∩ b)))
10125comcom2 183 . . . . . . . . . . . . . 14 (ba) C a
102101, 28fh4 472 . . . . . . . . . . . . 13 (a ∪ ((ba) ∩ b)) = ((a ∪ (ba)) ∩ (ab))
103 ax-a2 31 . . . . . . . . . . . . . . . 16 (a ∪ (ba)) = ((ba) ∪ a )
104 ax-a3 32 . . . . . . . . . . . . . . . . 17 ((ba) ∪ a ) = (b ∪ (aa ))
105 df-t 41 . . . . . . . . . . . . . . . . . . . 20 1 = (aa )
106105ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (aa ) = 1
107106lor 70 . . . . . . . . . . . . . . . . . 18 (b ∪ (aa )) = (b ∪ 1)
108 or1 104 . . . . . . . . . . . . . . . . . 18 (b ∪ 1) = 1
109107, 108ax-r2 36 . . . . . . . . . . . . . . . . 17 (b ∪ (aa )) = 1
110104, 109ax-r2 36 . . . . . . . . . . . . . . . 16 ((ba) ∪ a ) = 1
111103, 110ax-r2 36 . . . . . . . . . . . . . . 15 (a ∪ (ba)) = 1
112111ran 78 . . . . . . . . . . . . . 14 ((a ∪ (ba)) ∩ (ab)) = (1 ∩ (ab))
113 an1r 107 . . . . . . . . . . . . . 14 (1 ∩ (ab)) = (ab)
114112, 113ax-r2 36 . . . . . . . . . . . . 13 ((a ∪ (ba)) ∩ (ab)) = (ab)
115102, 114ax-r2 36 . . . . . . . . . . . 12 (a ∪ ((ba) ∩ b)) = (ab)
116115lor 70 . . . . . . . . . . 11 ((ab ) ∪ (a ∪ ((ba) ∩ b))) = ((ab ) ∪ (ab))
117 ax-a2 31 . . . . . . . . . . . 12 ((ab ) ∪ (ab)) = ((ab) ∪ (ab ))
118 anor1 88 . . . . . . . . . . . . . 14 (ab ) = (ab)
119118lor 70 . . . . . . . . . . . . 13 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
120 df-t 41 . . . . . . . . . . . . . 14 1 = ((ab) ∪ (ab) )
121120ax-r1 35 . . . . . . . . . . . . 13 ((ab) ∪ (ab) ) = 1
122119, 121ax-r2 36 . . . . . . . . . . . 12 ((ab) ∪ (ab )) = 1
123117, 122ax-r2 36 . . . . . . . . . . 11 ((ab ) ∪ (ab)) = 1
124116, 123ax-r2 36 . . . . . . . . . 10 ((ab ) ∪ (a ∪ ((ba) ∩ b))) = 1
125100, 124ax-r2 36 . . . . . . . . 9 (((ab ) ∪ a ) ∪ ((ba) ∩ b)) = 1
12699, 125ax-r2 36 . . . . . . . 8 ((a ∪ (ab )) ∪ (b ∩ (ba))) = 1
127126lor 70 . . . . . . 7 (((ba) ∪ (ba )) ∪ ((a ∪ (ab )) ∪ (b ∩ (ba)))) = (((ba) ∪ (ba )) ∪ 1)
128 or1 104 . . . . . . 7 (((ba) ∪ (ba )) ∪ 1) = 1
129127, 128ax-r2 36 . . . . . 6 (((ba) ∪ (ba )) ∪ ((a ∪ (ab )) ∪ (b ∩ (ba)))) = 1
13096, 129ax-r2 36 . . . . 5 ((a ∪ (ab )) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = 1
13195, 1302an 79 . . . 4 ((((ab ) ∩ (ab)) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) ∩ ((a ∪ (ab )) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba))))) = ((ab ) ∩ 1)
132131, 93ax-r2 36 . . 3 ((((ab ) ∩ (ab)) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) ∩ ((a ∪ (ab )) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba))))) = (ab )
13348, 132ax-r2 36 . 2 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ (((ba) ∪ (ba )) ∪ (b ∩ (ba)))) = (ab )
1343, 133ax-r2 36 1 ((a3 b) ∪ (b3 a)) = (ab )
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  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:  ud3lem1d  569
  Copyright terms: Public domain W3C validator