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

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

Proof of Theorem u4lem5
StepHypRef Expression
1 df-i4 47 . 2 (a4 (a4 b)) = (((a ∩ (a4 b)) ∪ (a ∩ (a4 b))) ∪ ((a ∪ (a4 b)) ∩ (a4 b) ))
2 ancom 74 . . . . . . 7 (a ∩ (a4 b)) = ((a4 b) ∩ a)
3 u4lemaa 603 . . . . . . 7 ((a4 b) ∩ a) = (ab)
42, 3ax-r2 36 . . . . . 6 (a ∩ (a4 b)) = (ab)
5 ancom 74 . . . . . . 7 (a ∩ (a4 b)) = ((a4 b) ∩ a )
6 u4lemana 608 . . . . . . 7 ((a4 b) ∩ a ) = ((ab) ∪ (ab ))
75, 6ax-r2 36 . . . . . 6 (a ∩ (a4 b)) = ((ab) ∪ (ab ))
84, 72or 72 . . . . 5 ((a ∩ (a4 b)) ∪ (a ∩ (a4 b))) = ((ab) ∪ ((ab) ∪ (ab )))
9 ax-a3 32 . . . . . 6 (((ab) ∪ (ab)) ∪ (ab )) = ((ab) ∪ ((ab) ∪ (ab )))
109ax-r1 35 . . . . 5 ((ab) ∪ ((ab) ∪ (ab ))) = (((ab) ∪ (ab)) ∪ (ab ))
118, 10ax-r2 36 . . . 4 ((a ∩ (a4 b)) ∪ (a ∩ (a4 b))) = (((ab) ∪ (ab)) ∪ (ab ))
12 ax-a2 31 . . . . . . 7 (a ∪ (a4 b)) = ((a4 b) ∪ a )
13 u4lemona 628 . . . . . . 7 ((a4 b) ∪ a ) = (ab)
1412, 13ax-r2 36 . . . . . 6 (a ∪ (a4 b)) = (ab)
15 ud4lem0c 280 . . . . . 6 (a4 b) = (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))
1614, 152an 79 . . . . 5 ((a ∪ (a4 b)) ∩ (a4 b) ) = ((ab) ∩ (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)))
17 ancom 74 . . . . . 6 ((ab) ∩ (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))) = ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ab))
18 anass 76 . . . . . . 7 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ab)) = (((ab ) ∩ (ab )) ∩ (((ab ) ∪ b) ∩ (ab)))
19 comor1 461 . . . . . . . . . . . . 13 (ab) C a
2019comcom7 460 . . . . . . . . . . . 12 (ab) C a
21 comor2 462 . . . . . . . . . . . . 13 (ab) C b
2221comcom2 183 . . . . . . . . . . . 12 (ab) C b
2320, 22com2an 484 . . . . . . . . . . 11 (ab) C (ab )
2423, 21fh1r 473 . . . . . . . . . 10 (((ab ) ∪ b) ∩ (ab)) = (((ab ) ∩ (ab)) ∪ (b ∩ (ab)))
25 ax-a2 31 . . . . . . . . . . 11 (((ab ) ∩ (ab)) ∪ (b ∩ (ab))) = ((b ∩ (ab)) ∪ ((ab ) ∩ (ab)))
26 leor 159 . . . . . . . . . . . . . 14 b ≤ (ab)
2726df2le2 136 . . . . . . . . . . . . 13 (b ∩ (ab)) = b
28 oran2 92 . . . . . . . . . . . . . . 15 (ab) = (ab )
2928lan 77 . . . . . . . . . . . . . 14 ((ab ) ∩ (ab)) = ((ab ) ∩ (ab ) )
30 dff 101 . . . . . . . . . . . . . . 15 0 = ((ab ) ∩ (ab ) )
3130ax-r1 35 . . . . . . . . . . . . . 14 ((ab ) ∩ (ab ) ) = 0
3229, 31ax-r2 36 . . . . . . . . . . . . 13 ((ab ) ∩ (ab)) = 0
3327, 322or 72 . . . . . . . . . . . 12 ((b ∩ (ab)) ∪ ((ab ) ∩ (ab))) = (b ∪ 0)
34 or0 102 . . . . . . . . . . . 12 (b ∪ 0) = b
3533, 34ax-r2 36 . . . . . . . . . . 11 ((b ∩ (ab)) ∪ ((ab ) ∩ (ab))) = b
3625, 35ax-r2 36 . . . . . . . . . 10 (((ab ) ∩ (ab)) ∪ (b ∩ (ab))) = b
3724, 36ax-r2 36 . . . . . . . . 9 (((ab ) ∪ b) ∩ (ab)) = b
3837lan 77 . . . . . . . 8 (((ab ) ∩ (ab )) ∩ (((ab ) ∪ b) ∩ (ab))) = (((ab ) ∩ (ab )) ∩ b)
39 ancom 74 . . . . . . . 8 (((ab ) ∩ (ab )) ∩ b) = (b ∩ ((ab ) ∩ (ab )))
4038, 39ax-r2 36 . . . . . . 7 (((ab ) ∩ (ab )) ∩ (((ab ) ∪ b) ∩ (ab))) = (b ∩ ((ab ) ∩ (ab )))
4118, 40ax-r2 36 . . . . . 6 ((((ab ) ∩ (ab )) ∩ ((ab ) ∪ b)) ∩ (ab)) = (b ∩ ((ab ) ∩ (ab )))
4217, 41ax-r2 36 . . . . 5 ((ab) ∩ (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))) = (b ∩ ((ab ) ∩ (ab )))
4316, 42ax-r2 36 . . . 4 ((a ∪ (a4 b)) ∩ (a4 b) ) = (b ∩ ((ab ) ∩ (ab )))
4411, 432or 72 . . 3 (((a ∩ (a4 b)) ∪ (a ∩ (a4 b))) ∪ ((a ∪ (a4 b)) ∩ (a4 b) )) = ((((ab) ∪ (ab)) ∪ (ab )) ∪ (b ∩ ((ab ) ∩ (ab ))))
45 comanr2 465 . . . . . . 7 b C (ab)
46 comanr2 465 . . . . . . 7 b C (ab)
4745, 46com2or 483 . . . . . 6 b C ((ab) ∪ (ab))
48 comanr2 465 . . . . . . 7 b C (ab )
4948comcom6 459 . . . . . 6 b C (ab )
5047, 49com2or 483 . . . . 5 b C (((ab) ∪ (ab)) ∪ (ab ))
51 comorr2 463 . . . . . . 7 b C (ab )
52 comorr2 463 . . . . . . 7 b C (ab )
5351, 52com2an 484 . . . . . 6 b C ((ab ) ∩ (ab ))
5453comcom6 459 . . . . 5 b C ((ab ) ∩ (ab ))
5550, 54fh4 472 . . . 4 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (b ∩ ((ab ) ∩ (ab )))) = (((((ab) ∪ (ab)) ∪ (ab )) ∪ b) ∩ ((((ab) ∪ (ab)) ∪ (ab )) ∪ ((ab ) ∩ (ab ))))
56 or32 82 . . . . . . 7 ((((ab) ∪ (ab)) ∪ (ab )) ∪ b) = ((((ab) ∪ (ab)) ∪ b) ∪ (ab ))
57 lear 161 . . . . . . . . . 10 (ab) ≤ b
58 lear 161 . . . . . . . . . 10 (ab) ≤ b
5957, 58lel2or 170 . . . . . . . . 9 ((ab) ∪ (ab)) ≤ b
6059df-le2 131 . . . . . . . 8 (((ab) ∪ (ab)) ∪ b) = b
6160ax-r5 38 . . . . . . 7 ((((ab) ∪ (ab)) ∪ b) ∪ (ab )) = (b ∪ (ab ))
6256, 61ax-r2 36 . . . . . 6 ((((ab) ∪ (ab)) ∪ (ab )) ∪ b) = (b ∪ (ab ))
63 comor1 461 . . . . . . . . . . . 12 (ab ) C a
6463comcom7 460 . . . . . . . . . . 11 (ab ) C a
65 comor2 462 . . . . . . . . . . . 12 (ab ) C b
6665comcom7 460 . . . . . . . . . . 11 (ab ) C b
6764, 66com2an 484 . . . . . . . . . 10 (ab ) C (ab)
6863, 66com2an 484 . . . . . . . . . 10 (ab ) C (ab)
6967, 68com2or 483 . . . . . . . . 9 (ab ) C ((ab) ∪ (ab))
7063, 65com2an 484 . . . . . . . . 9 (ab ) C (ab )
7169, 70com2or 483 . . . . . . . 8 (ab ) C (((ab) ∪ (ab)) ∪ (ab ))
7264, 65com2or 483 . . . . . . . 8 (ab ) C (ab )
7371, 72fh4 472 . . . . . . 7 ((((ab) ∪ (ab)) ∪ (ab )) ∪ ((ab ) ∩ (ab ))) = (((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) ∩ ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )))
74 or32 82 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) = ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab ))
75 ax-a3 32 . . . . . . . . . . 11 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) = (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab )))
76 or4 84 . . . . . . . . . . . 12 (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab ))) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))
77 ax-a2 31 . . . . . . . . . . . . 13 (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab ))) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))
78 oran3 93 . . . . . . . . . . . . . . . . 17 (ab ) = (ab)
7978lor 70 . . . . . . . . . . . . . . . 16 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
80 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((ab) ∪ (ab) )
8180ax-r1 35 . . . . . . . . . . . . . . . 16 ((ab) ∪ (ab) ) = 1
8279, 81ax-r2 36 . . . . . . . . . . . . . . 15 ((ab) ∪ (ab )) = 1
8382lor 70 . . . . . . . . . . . . . 14 (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab ))) = (((ab) ∪ (ab )) ∪ 1)
84 or1 104 . . . . . . . . . . . . . 14 (((ab) ∪ (ab )) ∪ 1) = 1
8583, 84ax-r2 36 . . . . . . . . . . . . 13 (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab ))) = 1
8677, 85ax-r2 36 . . . . . . . . . . . 12 (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab ))) = 1
8776, 86ax-r2 36 . . . . . . . . . . 11 (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab ))) = 1
8875, 87ax-r2 36 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) = 1
8974, 88ax-r2 36 . . . . . . . . 9 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) = 1
90 ax-a3 32 . . . . . . . . . 10 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) = (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab )))
91 or4 84 . . . . . . . . . . 11 (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab ))) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))
92 oran1 91 . . . . . . . . . . . . . . 15 (ab ) = (ab)
9392lor 70 . . . . . . . . . . . . . 14 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
94 df-t 41 . . . . . . . . . . . . . . 15 1 = ((ab) ∪ (ab) )
9594ax-r1 35 . . . . . . . . . . . . . 14 ((ab) ∪ (ab) ) = 1
9693, 95ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∪ (ab )) = 1
9796lor 70 . . . . . . . . . . . 12 (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab ))) = (((ab) ∪ (ab )) ∪ 1)
98 or1 104 . . . . . . . . . . . 12 (((ab) ∪ (ab )) ∪ 1) = 1
9997, 98ax-r2 36 . . . . . . . . . . 11 (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab ))) = 1
10091, 99ax-r2 36 . . . . . . . . . 10 (((ab) ∪ (ab)) ∪ ((ab ) ∪ (ab ))) = 1
10190, 100ax-r2 36 . . . . . . . . 9 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) = 1
10289, 1012an 79 . . . . . . . 8 (((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) ∩ ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab ))) = (1 ∩ 1)
103 an1 106 . . . . . . . 8 (1 ∩ 1) = 1
104102, 103ax-r2 36 . . . . . . 7 (((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab )) ∩ ((((ab) ∪ (ab)) ∪ (ab )) ∪ (ab ))) = 1
10573, 104ax-r2 36 . . . . . 6 ((((ab) ∪ (ab)) ∪ (ab )) ∪ ((ab ) ∩ (ab ))) = 1
10662, 1052an 79 . . . . 5 (((((ab) ∪ (ab)) ∪ (ab )) ∪ b) ∩ ((((ab) ∪ (ab)) ∪ (ab )) ∪ ((ab ) ∩ (ab )))) = ((b ∪ (ab )) ∩ 1)
107 an1 106 . . . . . 6 ((b ∪ (ab )) ∩ 1) = (b ∪ (ab ))
108 ax-a2 31 . . . . . 6 (b ∪ (ab )) = ((ab ) ∪ b)
109107, 108ax-r2 36 . . . . 5 ((b ∪ (ab )) ∩ 1) = ((ab ) ∪ b)
110106, 109ax-r2 36 . . . 4 (((((ab) ∪ (ab)) ∪ (ab )) ∪ b) ∩ ((((ab) ∪ (ab)) ∪ (ab )) ∪ ((ab ) ∩ (ab )))) = ((ab ) ∪ b)
11155, 110ax-r2 36 . . 3 ((((ab) ∪ (ab)) ∪ (ab )) ∪ (b ∩ ((ab ) ∩ (ab )))) = ((ab ) ∪ b)
11244, 111ax-r2 36 . 2 (((a ∩ (a4 b)) ∪ (a ∩ (a4 b))) ∪ ((a ∪ (a4 b)) ∩ (a4 b) )) = ((ab ) ∪ b)
1131, 112ax-r2 36 1 (a4 (a4 b)) = ((ab ) ∪ 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:  u4lem5n  766  u4lem6  768
  Copyright terms: Public domain W3C validator