![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > u1lemc4 | GIF version |
Description: Lemma for Sasaki implication study. (Contributed by NM, 24-Dec-1997.) |
Ref | Expression |
---|---|
ulemc3.1 | a C b |
Ref | Expression |
---|---|
u1lemc4 | (a →1 b) = (a⊥ ∪ b) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-i1 44 | . 2 (a →1 b) = (a⊥ ∪ (a ∩ b)) | |
2 | comid 187 | . . . . 5 a C a | |
3 | 2 | comcom2 183 | . . . 4 a C a⊥ |
4 | ulemc3.1 | . . . 4 a C b | |
5 | 3, 4 | fh4 472 | . . 3 (a⊥ ∪ (a ∩ b)) = ((a⊥ ∪ a) ∩ (a⊥ ∪ b)) |
6 | ancom 74 | . . . 4 ((a⊥ ∪ a) ∩ (a⊥ ∪ b)) = ((a⊥ ∪ b) ∩ (a⊥ ∪ a)) | |
7 | ax-a2 31 | . . . . . . 7 (a⊥ ∪ a) = (a ∪ a⊥ ) | |
8 | df-t 41 | . . . . . . . 8 1 = (a ∪ a⊥ ) | |
9 | 8 | ax-r1 35 | . . . . . . 7 (a ∪ a⊥ ) = 1 |
10 | 7, 9 | ax-r2 36 | . . . . . 6 (a⊥ ∪ a) = 1 |
11 | 10 | lan 77 | . . . . 5 ((a⊥ ∪ b) ∩ (a⊥ ∪ a)) = ((a⊥ ∪ b) ∩ 1) |
12 | an1 106 | . . . . 5 ((a⊥ ∪ b) ∩ 1) = (a⊥ ∪ b) | |
13 | 11, 12 | ax-r2 36 | . . . 4 ((a⊥ ∪ b) ∩ (a⊥ ∪ a)) = (a⊥ ∪ b) |
14 | 6, 13 | ax-r2 36 | . . 3 ((a⊥ ∪ a) ∩ (a⊥ ∪ b)) = (a⊥ ∪ b) |
15 | 5, 14 | ax-r2 36 | . 2 (a⊥ ∪ (a ∩ b)) = (a⊥ ∪ b) |
16 | 1, 15 | ax-r2 36 | 1 (a →1 b) = (a⊥ ∪ b) |
Colors of variables: term |
Syntax hints: = wb 1 C wc 3 ⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 →1 wi1 12 |
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-i1 44 df-le1 130 df-le2 131 df-c1 132 df-c2 133 |
This theorem is referenced by: u1lemle1 710 u1lem1 734 |
Copyright terms: Public domain | W3C validator |