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

Theorem wdid0id5 1111
 Description: Show that quantum identity follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
Hypothesis
Ref Expression
wdid0id5.1 (a0 b) = 1
Assertion
Ref Expression
wdid0id5 (ab) = 1

Proof of Theorem wdid0id5
StepHypRef Expression
1 dfb 94 . 2 (ab) = ((ab) ∪ (ab ))
2 df-id0 49 . . . . 5 (a0 b) = ((ab) ∩ (ba))
32ax-r1 35 . . . 4 ((ab) ∩ (ba)) = (a0 b)
4 wdid0id5.1 . . . 4 (a0 b) = 1
53, 4ax-r2 36 . . 3 ((ab) ∩ (ba)) = 1
6 wa4 194 . . . . . . . . 9 (((ab ) ∪ (aa )) ≡ (aa )) = 1
76wleoa 376 . . . . . . . 8 (((ab ) ∩ (aa )) ≡ (ab )) = 1
87wr1 197 . . . . . . 7 ((ab ) ≡ ((ab ) ∩ (aa ))) = 1
9 wancom 203 . . . . . . 7 (((ab ) ∩ (aa )) ≡ ((aa ) ∩ (ab ))) = 1
108, 9wr2 371 . . . . . 6 ((ab ) ≡ ((aa ) ∩ (ab ))) = 1
11 wa2 192 . . . . . 6 ((ba) ≡ (ab )) = 1
12 wddi3 1109 . . . . . 6 ((a ∪ (ab )) ≡ ((aa ) ∩ (ab ))) = 1
1310, 11, 12w3tr1 374 . . . . 5 ((ba) ≡ (a ∪ (ab ))) = 1
14 wa4 194 . . . . . . . 8 (((ba ) ∪ (bb )) ≡ (bb )) = 1
1514wleoa 376 . . . . . . 7 (((ba ) ∩ (bb )) ≡ (ba )) = 1
1615wr1 197 . . . . . 6 ((ba ) ≡ ((ba ) ∩ (bb ))) = 1
17 wa2 192 . . . . . 6 ((ab) ≡ (ba )) = 1
18 wddi3 1109 . . . . . 6 ((b ∪ (ab )) ≡ ((ba ) ∩ (bb ))) = 1
1916, 17, 18w3tr1 374 . . . . 5 ((ab) ≡ (b ∪ (ab ))) = 1
2013, 19w2an 373 . . . 4 (((ba) ∩ (ab)) ≡ ((a ∪ (ab )) ∩ (b ∪ (ab )))) = 1
21 wancom 203 . . . 4 (((ab) ∩ (ba)) ≡ ((ba) ∩ (ab))) = 1
22 wddi4 1110 . . . 4 (((ab) ∪ (ab )) ≡ ((a ∪ (ab )) ∩ (b ∪ (ab )))) = 1
2320, 21, 22w3tr1 374 . . 3 (((ab) ∩ (ba)) ≡ ((ab) ∪ (ab ))) = 1
245, 23wwbmp 205 . 2 ((ab) ∪ (ab )) = 1
251, 24ax-r2 36 1 (ab) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8   ≡0 wid0 17 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-wom 361  ax-wdol 1104 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-id0 49  df-le 129  df-le1 130  df-le2 131  df-cmtr 134 This theorem is referenced by:  wdka4o  1116
 Copyright terms: Public domain W3C validator