Proof of Theorem nom51
Step | Hyp | Ref
| Expression |
1 | | ancom 74 |
. . . . . . . . 9
(b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ ) |
2 | | anor3 90 |
. . . . . . . . 9
(a⊥ ∩ b⊥ ) = (a ∪ b)⊥ |
3 | 1, 2 | ax-r2 36 |
. . . . . . . 8
(b⊥ ∩ a⊥ ) = (a ∪ b)⊥ |
4 | 3 | ax-r1 35 |
. . . . . . 7
(a ∪ b)⊥ = (b⊥ ∩ a⊥ ) |
5 | 4 | ax-r4 37 |
. . . . . 6
(a ∪ b)⊥ ⊥ = (b⊥ ∩ a⊥
)⊥ |
6 | 5 | lor 70 |
. . . . 5
(b⊥ ∪ (a ∪ b)⊥ ⊥ ) =
(b⊥ ∪ (b⊥ ∩ a⊥ )⊥
) |
7 | 2 | ax-r1 35 |
. . . . . . . . 9
(a ∪ b)⊥ = (a⊥ ∩ b⊥ ) |
8 | | ancom 74 |
. . . . . . . . 9
(a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ ) |
9 | 7, 8 | ax-r2 36 |
. . . . . . . 8
(a ∪ b)⊥ = (b⊥ ∩ a⊥ ) |
10 | 9 | ax-r4 37 |
. . . . . . 7
(a ∪ b)⊥ ⊥ = (b⊥ ∩ a⊥
)⊥ |
11 | 10 | lan 77 |
. . . . . 6
(b⊥
⊥ ∩ (a ∪ b)⊥ ⊥ ) =
(b⊥ ⊥
∩ (b⊥ ∩ a⊥ )⊥
) |
12 | 4, 11 | 2or 72 |
. . . . 5
((a ∪ b)⊥ ∪ (b⊥ ⊥ ∩
(a ∪ b)⊥ ⊥ )) =
((b⊥ ∩ a⊥ ) ∪ (b⊥ ⊥ ∩
(b⊥ ∩ a⊥ )⊥
)) |
13 | 6, 12 | 2an 79 |
. . . 4
((b⊥ ∪
(a ∪ b)⊥ ⊥ ) ∩
((a ∪ b)⊥ ∪ (b⊥ ⊥ ∩
(a ∪ b)⊥ ⊥ ))) =
((b⊥ ∪ (b⊥ ∩ a⊥ )⊥ ) ∩
((b⊥ ∩ a⊥ ) ∪ (b⊥ ⊥ ∩
(b⊥ ∩ a⊥ )⊥
))) |
14 | | df-id2 51 |
. . . 4
(b⊥ ≡2
(a ∪ b)⊥ ) = ((b⊥ ∪ (a ∪ b)⊥ ⊥ ) ∩
((a ∪ b)⊥ ∪ (b⊥ ⊥ ∩
(a ∪ b)⊥ ⊥
))) |
15 | | df-id2 51 |
. . . 4
(b⊥ ≡2
(b⊥ ∩ a⊥ )) = ((b⊥ ∪ (b⊥ ∩ a⊥ )⊥ ) ∩
((b⊥ ∩ a⊥ ) ∪ (b⊥ ⊥ ∩
(b⊥ ∩ a⊥ )⊥
))) |
16 | 13, 14, 15 | 3tr1 63 |
. . 3
(b⊥ ≡2
(a ∪ b)⊥ ) = (b⊥ ≡2 (b⊥ ∩ a⊥ )) |
17 | | nom22 315 |
. . 3
(b⊥ ≡2
(b⊥ ∩ a⊥ )) = (b⊥ →1 a⊥ ) |
18 | 16, 17 | ax-r2 36 |
. 2
(b⊥ ≡2
(a ∪ b)⊥ ) = (b⊥ →1 a⊥ ) |
19 | | nomcon1 302 |
. 2
((a ∪ b) ≡1 b) = (b⊥ ≡2 (a ∪ b)⊥ ) |
20 | | i2i1 267 |
. 2
(a →2 b) = (b⊥ →1 a⊥ ) |
21 | 18, 19, 20 | 3tr1 63 |
1
((a ∪ b) ≡1 b) = (a
→2 b) |