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

Theorem u4lem6 768
Description: Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)
Assertion
Ref Expression
u4lem6 (a4 (a4 (a4 b))) = (a4 b)

Proof of Theorem u4lem6
StepHypRef Expression
1 df-i4 47 . 2 (a4 (a4 (a4 b))) = (((a ∩ (a4 (a4 b))) ∪ (a ∩ (a4 (a4 b)))) ∪ ((a ∪ (a4 (a4 b))) ∩ (a4 (a4 b)) ))
2 u4lem5 764 . . . . . . . 8 (a4 (a4 b)) = ((ab ) ∪ b)
32lan 77 . . . . . . 7 (a ∩ (a4 (a4 b))) = (a ∩ ((ab ) ∪ b))
4 coman1 185 . . . . . . . . . 10 (ab ) C a
54comcom7 460 . . . . . . . . 9 (ab ) C a
6 coman2 186 . . . . . . . . . 10 (ab ) C b
76comcom7 460 . . . . . . . . 9 (ab ) C b
85, 7fh2 470 . . . . . . . 8 (a ∩ ((ab ) ∪ b)) = ((a ∩ (ab )) ∪ (ab))
9 ax-a2 31 . . . . . . . . 9 ((a ∩ (ab )) ∪ (ab)) = ((ab) ∪ (a ∩ (ab )))
10 ancom 74 . . . . . . . . . . . 12 ((aa ) ∩ b ) = (b ∩ (aa ))
11 anass 76 . . . . . . . . . . . 12 ((aa ) ∩ b ) = (a ∩ (ab ))
12 dff 101 . . . . . . . . . . . . . . 15 0 = (aa )
1312ax-r1 35 . . . . . . . . . . . . . 14 (aa ) = 0
1413lan 77 . . . . . . . . . . . . 13 (b ∩ (aa )) = (b ∩ 0)
15 an0 108 . . . . . . . . . . . . 13 (b ∩ 0) = 0
1614, 15ax-r2 36 . . . . . . . . . . . 12 (b ∩ (aa )) = 0
1710, 11, 163tr2 64 . . . . . . . . . . 11 (a ∩ (ab )) = 0
1817lor 70 . . . . . . . . . 10 ((ab) ∪ (a ∩ (ab ))) = ((ab) ∪ 0)
19 or0 102 . . . . . . . . . 10 ((ab) ∪ 0) = (ab)
2018, 19ax-r2 36 . . . . . . . . 9 ((ab) ∪ (a ∩ (ab ))) = (ab)
219, 20ax-r2 36 . . . . . . . 8 ((a ∩ (ab )) ∪ (ab)) = (ab)
228, 21ax-r2 36 . . . . . . 7 (a ∩ ((ab ) ∪ b)) = (ab)
233, 22ax-r2 36 . . . . . 6 (a ∩ (a4 (a4 b))) = (ab)
242lan 77 . . . . . . 7 (a ∩ (a4 (a4 b))) = (a ∩ ((ab ) ∪ b))
254, 7fh2 470 . . . . . . . 8 (a ∩ ((ab ) ∪ b)) = ((a ∩ (ab )) ∪ (ab))
26 anass 76 . . . . . . . . . . 11 ((aa ) ∩ b ) = (a ∩ (ab ))
2726ax-r1 35 . . . . . . . . . 10 (a ∩ (ab )) = ((aa ) ∩ b )
28 anidm 111 . . . . . . . . . . 11 (aa ) = a
2928ran 78 . . . . . . . . . 10 ((aa ) ∩ b ) = (ab )
3027, 29ax-r2 36 . . . . . . . . 9 (a ∩ (ab )) = (ab )
3130ax-r5 38 . . . . . . . 8 ((a ∩ (ab )) ∪ (ab)) = ((ab ) ∪ (ab))
3225, 31ax-r2 36 . . . . . . 7 (a ∩ ((ab ) ∪ b)) = ((ab ) ∪ (ab))
3324, 32ax-r2 36 . . . . . 6 (a ∩ (a4 (a4 b))) = ((ab ) ∪ (ab))
3423, 332or 72 . . . . 5 ((a ∩ (a4 (a4 b))) ∪ (a ∩ (a4 (a4 b)))) = ((ab) ∪ ((ab ) ∪ (ab)))
35 id 59 . . . . 5 ((ab) ∪ ((ab ) ∪ (ab))) = ((ab) ∪ ((ab ) ∪ (ab)))
3634, 35ax-r2 36 . . . 4 ((a ∩ (a4 (a4 b))) ∪ (a ∩ (a4 (a4 b)))) = ((ab) ∪ ((ab ) ∪ (ab)))
372lor 70 . . . . . . 7 (a ∪ (a4 (a4 b))) = (a ∪ ((ab ) ∪ b))
38 or12 80 . . . . . . . 8 (a ∪ ((ab ) ∪ b)) = ((ab ) ∪ (ab))
39 comor1 461 . . . . . . . . . 10 (ab) C a
40 comor2 462 . . . . . . . . . . 11 (ab) C b
4140comcom2 183 . . . . . . . . . 10 (ab) C b
4239, 41fh3r 475 . . . . . . . . 9 ((ab ) ∪ (ab)) = ((a ∪ (ab)) ∩ (b ∪ (ab)))
43 ax-a3 32 . . . . . . . . . . . . 13 ((aa ) ∪ b) = (a ∪ (ab))
4443ax-r1 35 . . . . . . . . . . . 12 (a ∪ (ab)) = ((aa ) ∪ b)
45 oridm 110 . . . . . . . . . . . . 13 (aa ) = a
4645ax-r5 38 . . . . . . . . . . . 12 ((aa ) ∪ b) = (ab)
4744, 46ax-r2 36 . . . . . . . . . . 11 (a ∪ (ab)) = (ab)
48 or12 80 . . . . . . . . . . . 12 (b ∪ (ab)) = (a ∪ (bb))
49 ax-a2 31 . . . . . . . . . . . . . . 15 (bb) = (bb )
50 df-t 41 . . . . . . . . . . . . . . . 16 1 = (bb )
5150ax-r1 35 . . . . . . . . . . . . . . 15 (bb ) = 1
5249, 51ax-r2 36 . . . . . . . . . . . . . 14 (bb) = 1
5352lor 70 . . . . . . . . . . . . 13 (a ∪ (bb)) = (a ∪ 1)
54 or1 104 . . . . . . . . . . . . 13 (a ∪ 1) = 1
5553, 54ax-r2 36 . . . . . . . . . . . 12 (a ∪ (bb)) = 1
5648, 55ax-r2 36 . . . . . . . . . . 11 (b ∪ (ab)) = 1
5747, 562an 79 . . . . . . . . . 10 ((a ∪ (ab)) ∩ (b ∪ (ab))) = ((ab) ∩ 1)
58 an1 106 . . . . . . . . . 10 ((ab) ∩ 1) = (ab)
5957, 58ax-r2 36 . . . . . . . . 9 ((a ∪ (ab)) ∩ (b ∪ (ab))) = (ab)
6042, 59ax-r2 36 . . . . . . . 8 ((ab ) ∪ (ab)) = (ab)
6138, 60ax-r2 36 . . . . . . 7 (a ∪ ((ab ) ∪ b)) = (ab)
6237, 61ax-r2 36 . . . . . 6 (a ∪ (a4 (a4 b))) = (ab)
63 u4lem5n 766 . . . . . 6 (a4 (a4 b)) = ((ab) ∩ b )
6462, 632an 79 . . . . 5 ((a ∪ (a4 (a4 b))) ∩ (a4 (a4 b)) ) = ((ab) ∩ ((ab) ∩ b ))
65 id 59 . . . . 5 ((ab) ∩ ((ab) ∩ b )) = ((ab) ∩ ((ab) ∩ b ))
6664, 65ax-r2 36 . . . 4 ((a ∪ (a4 (a4 b))) ∩ (a4 (a4 b)) ) = ((ab) ∩ ((ab) ∩ b ))
6736, 662or 72 . . 3 (((a ∩ (a4 (a4 b))) ∪ (a ∩ (a4 (a4 b)))) ∪ ((a ∪ (a4 (a4 b))) ∩ (a4 (a4 b)) )) = (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ ((ab) ∩ b )))
6839comcom7 460 . . . . . . 7 (ab) C a
6968, 40com2an 484 . . . . . 6 (ab) C (ab)
7039, 41com2an 484 . . . . . . 7 (ab) C (ab )
7139, 40com2an 484 . . . . . . 7 (ab) C (ab)
7270, 71com2or 483 . . . . . 6 (ab) C ((ab ) ∪ (ab))
7369, 72com2or 483 . . . . 5 (ab) C ((ab) ∪ ((ab ) ∪ (ab)))
7468, 40com2or 483 . . . . . 6 (ab) C (ab)
7574, 41com2an 484 . . . . 5 (ab) C ((ab) ∩ b )
7673, 75fh4 472 . . . 4 (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ ((ab) ∩ b ))) = ((((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) ∩ (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ b )))
77 lear 161 . . . . . . . . 9 (ab) ≤ b
78 leor 159 . . . . . . . . 9 b ≤ (ab)
7977, 78letr 137 . . . . . . . 8 (ab) ≤ (ab)
80 lea 160 . . . . . . . . . 10 (ab ) ≤ a
81 lea 160 . . . . . . . . . 10 (ab) ≤ a
8280, 81lel2or 170 . . . . . . . . 9 ((ab ) ∪ (ab)) ≤ a
83 leo 158 . . . . . . . . 9 a ≤ (ab)
8482, 83letr 137 . . . . . . . 8 ((ab ) ∪ (ab)) ≤ (ab)
8579, 84lel2or 170 . . . . . . 7 ((ab) ∪ ((ab ) ∪ (ab))) ≤ (ab)
8685df-le2 131 . . . . . 6 (((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) = (ab)
87 comor1 461 . . . . . . . . . 10 (ab) C a
88 comor2 462 . . . . . . . . . 10 (ab) C b
8987, 88com2an 484 . . . . . . . . 9 (ab) C (ab)
9087comcom2 183 . . . . . . . . . . 11 (ab) C a
9188comcom2 183 . . . . . . . . . . 11 (ab) C b
9290, 91com2an 484 . . . . . . . . . 10 (ab) C (ab )
9390, 88com2an 484 . . . . . . . . . 10 (ab) C (ab)
9492, 93com2or 483 . . . . . . . . 9 (ab) C ((ab ) ∪ (ab))
9589, 94com2or 483 . . . . . . . 8 (ab) C ((ab) ∪ ((ab ) ∪ (ab)))
9695, 91fh4 472 . . . . . . 7 (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ b )) = ((((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) ∩ (((ab) ∪ ((ab ) ∪ (ab))) ∪ b ))
97 or32 82 . . . . . . . . . 10 (((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) = (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab)))
98 ax-a3 32 . . . . . . . . . . . . 13 (((ab) ∪ (ab)) ∪ (ab )) = ((ab) ∪ ((ab) ∪ (ab )))
99 anor3 90 . . . . . . . . . . . . . . . . 17 (ab ) = (ab)
10099lor 70 . . . . . . . . . . . . . . . 16 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
101 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((ab) ∪ (ab) )
102101ax-r1 35 . . . . . . . . . . . . . . . 16 ((ab) ∪ (ab) ) = 1
103100, 102ax-r2 36 . . . . . . . . . . . . . . 15 ((ab) ∪ (ab )) = 1
104103lor 70 . . . . . . . . . . . . . 14 ((ab) ∪ ((ab) ∪ (ab ))) = ((ab) ∪ 1)
105 or1 104 . . . . . . . . . . . . . 14 ((ab) ∪ 1) = 1
106104, 105ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∪ ((ab) ∪ (ab ))) = 1
10798, 106ax-r2 36 . . . . . . . . . . . 12 (((ab) ∪ (ab)) ∪ (ab )) = 1
108107ax-r5 38 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab)) = (1 ∪ (ab))
109 ax-a3 32 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab)) = (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab)))
110 ax-a2 31 . . . . . . . . . . . 12 (1 ∪ (ab)) = ((ab) ∪ 1)
111 or1 104 . . . . . . . . . . . 12 ((ab) ∪ 1) = 1
112110, 111ax-r2 36 . . . . . . . . . . 11 (1 ∪ (ab)) = 1
113108, 109, 1123tr2 64 . . . . . . . . . 10 (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab))) = 1
11497, 113ax-r2 36 . . . . . . . . 9 (((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) = 1
115 or12 80 . . . . . . . . . . 11 ((ab) ∪ ((ab ) ∪ (ab))) = ((ab ) ∪ ((ab) ∪ (ab)))
116115ax-r5 38 . . . . . . . . . 10 (((ab) ∪ ((ab ) ∪ (ab))) ∪ b ) = (((ab ) ∪ ((ab) ∪ (ab))) ∪ b )
117 lear 161 . . . . . . . . . . . . 13 (ab ) ≤ b
118117df-le2 131 . . . . . . . . . . . 12 ((ab ) ∪ b ) = b
119118ax-r5 38 . . . . . . . . . . 11 (((ab ) ∪ b ) ∪ ((ab) ∪ (ab))) = (b ∪ ((ab) ∪ (ab)))
120 or32 82 . . . . . . . . . . 11 (((ab ) ∪ ((ab) ∪ (ab))) ∪ b ) = (((ab ) ∪ b ) ∪ ((ab) ∪ (ab)))
121 id 59 . . . . . . . . . . 11 (b ∪ ((ab) ∪ (ab))) = (b ∪ ((ab) ∪ (ab)))
122119, 120, 1213tr1 63 . . . . . . . . . 10 (((ab ) ∪ ((ab) ∪ (ab))) ∪ b ) = (b ∪ ((ab) ∪ (ab)))
123116, 122ax-r2 36 . . . . . . . . 9 (((ab) ∪ ((ab ) ∪ (ab))) ∪ b ) = (b ∪ ((ab) ∪ (ab)))
124114, 1232an 79 . . . . . . . 8 ((((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) ∩ (((ab) ∪ ((ab ) ∪ (ab))) ∪ b )) = (1 ∩ (b ∪ ((ab) ∪ (ab))))
125 ancom 74 . . . . . . . . 9 (1 ∩ (b ∪ ((ab) ∪ (ab)))) = ((b ∪ ((ab) ∪ (ab))) ∩ 1)
126 an1 106 . . . . . . . . 9 ((b ∪ ((ab) ∪ (ab))) ∩ 1) = (b ∪ ((ab) ∪ (ab)))
127125, 126ax-r2 36 . . . . . . . 8 (1 ∩ (b ∪ ((ab) ∪ (ab)))) = (b ∪ ((ab) ∪ (ab)))
128124, 127ax-r2 36 . . . . . . 7 ((((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) ∩ (((ab) ∪ ((ab ) ∪ (ab))) ∪ b )) = (b ∪ ((ab) ∪ (ab)))
12996, 128ax-r2 36 . . . . . 6 (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ b )) = (b ∪ ((ab) ∪ (ab)))
13086, 1292an 79 . . . . 5 ((((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) ∩ (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ b ))) = ((ab) ∩ (b ∪ ((ab) ∪ (ab))))
131 comorr2 463 . . . . . . . 8 b C (ab)
132131comcom3 454 . . . . . . 7 b C (ab)
133 comanr2 465 . . . . . . . . 9 b C (ab)
134 comanr2 465 . . . . . . . . 9 b C (ab)
135133, 134com2or 483 . . . . . . . 8 b C ((ab) ∪ (ab))
136135comcom3 454 . . . . . . 7 b C ((ab) ∪ (ab))
137132, 136fh2 470 . . . . . 6 ((ab) ∩ (b ∪ ((ab) ∪ (ab)))) = (((ab) ∩ b ) ∪ ((ab) ∩ ((ab) ∪ (ab))))
138 ax-a2 31 . . . . . . 7 (((ab) ∩ b ) ∪ ((ab) ∪ (ab))) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))
139 ancom 74 . . . . . . . . 9 ((ab) ∩ ((ab) ∪ (ab))) = (((ab) ∪ (ab)) ∩ (ab))
140 lear 161 . . . . . . . . . . . 12 (ab) ≤ b
14177, 140lel2or 170 . . . . . . . . . . 11 ((ab) ∪ (ab)) ≤ b
142141, 78letr 137 . . . . . . . . . 10 ((ab) ∪ (ab)) ≤ (ab)
143142df2le2 136 . . . . . . . . 9 (((ab) ∪ (ab)) ∩ (ab)) = ((ab) ∪ (ab))
144139, 143ax-r2 36 . . . . . . . 8 ((ab) ∩ ((ab) ∪ (ab))) = ((ab) ∪ (ab))
145144lor 70 . . . . . . 7 (((ab) ∩ b ) ∪ ((ab) ∩ ((ab) ∪ (ab)))) = (((ab) ∩ b ) ∪ ((ab) ∪ (ab)))
146 df-i4 47 . . . . . . 7 (a4 b) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))
147138, 145, 1463tr1 63 . . . . . 6 (((ab) ∩ b ) ∪ ((ab) ∩ ((ab) ∪ (ab)))) = (a4 b)
148137, 147ax-r2 36 . . . . 5 ((ab) ∩ (b ∪ ((ab) ∪ (ab)))) = (a4 b)
149130, 148ax-r2 36 . . . 4 ((((ab) ∪ ((ab ) ∪ (ab))) ∪ (ab)) ∩ (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ b ))) = (a4 b)
15076, 149ax-r2 36 . . 3 (((ab) ∪ ((ab ) ∪ (ab))) ∪ ((ab) ∩ ((ab) ∩ b ))) = (a4 b)
15167, 150ax-r2 36 . 2 (((a ∩ (a4 (a4 b))) ∪ (a ∩ (a4 (a4 b)))) ∪ ((a ∪ (a4 (a4 b))) ∩ (a4 (a4 b)) )) = (a4 b)
1521, 151ax-r2 36 1 (a4 (a4 (a4 b))) = (a4 b)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  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: (None)
  Copyright terms: Public domain W3C validator