Proof of Theorem comd
Step | Hyp | Ref
| Expression |
1 | | comcom.1 |
. . . . 5
a C b |
2 | 1 | comcom4 455 |
. . . 4
a⊥ C
b⊥ |
3 | 2 | df-c2 133 |
. . 3
a⊥ = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥
)) |
4 | 3 | con3 68 |
. 2
a = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥
))⊥ |
5 | | oran 87 |
. . . 4
((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) =
((a⊥ ∩ b⊥ )⊥ ∩
(a⊥ ∩ b⊥ ⊥
)⊥ )⊥ |
6 | 5 | con2 67 |
. . 3
((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥
))⊥ = ((a⊥ ∩ b⊥ )⊥ ∩
(a⊥ ∩ b⊥ ⊥
)⊥ ) |
7 | | oran 87 |
. . . . 5
(a ∪ b) = (a⊥ ∩ b⊥
)⊥ |
8 | | oran 87 |
. . . . 5
(a ∪ b⊥ ) = (a⊥ ∩ b⊥ ⊥
)⊥ |
9 | 7, 8 | 2an 79 |
. . . 4
((a ∪ b) ∩ (a
∪ b⊥ )) = ((a⊥ ∩ b⊥ )⊥ ∩
(a⊥ ∩ b⊥ ⊥
)⊥ ) |
10 | 9 | ax-r1 35 |
. . 3
((a⊥ ∩ b⊥ )⊥ ∩
(a⊥ ∩ b⊥ ⊥
)⊥ ) = ((a ∪ b) ∩ (a
∪ b⊥
)) |
11 | 6, 10 | ax-r2 36 |
. 2
((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥
))⊥ = ((a ∪ b) ∩ (a
∪ b⊥
)) |
12 | 4, 11 | ax-r2 36 |
1
a = ((a ∪ b) ∩
(a ∪ b⊥ )) |