Proof of Theorem com3i
Step | Hyp | Ref
| Expression |
1 | | anor1 88 |
. . . . . . . 8
(a ∩ b⊥ ) = (a⊥ ∪ b)⊥ |
2 | 1 | con2 67 |
. . . . . . 7
(a ∩ b⊥ )⊥ = (a⊥ ∪ b) |
3 | 2 | ran 78 |
. . . . . 6
((a ∩ b⊥ )⊥ ∩
a) = ((a⊥ ∪ b) ∩ a) |
4 | | ancom 74 |
. . . . . 6
((a⊥ ∪ b) ∩ a) =
(a ∩ (a⊥ ∪ b)) |
5 | 3, 4 | ax-r2 36 |
. . . . 5
((a ∩ b⊥ )⊥ ∩
a) = (a
∩ (a⊥ ∪ b)) |
6 | | com3i.1 |
. . . . 5
(a ∩ (a⊥ ∪ b)) = (a ∩
b) |
7 | 5, 6 | ax-r2 36 |
. . . 4
((a ∩ b⊥ )⊥ ∩
a) = (a
∩ b) |
8 | 7 | lor 70 |
. . 3
((a ∩ b⊥ ) ∪ ((a ∩ b⊥ )⊥ ∩
a)) = ((a ∩ b⊥ ) ∪ (a ∩ b)) |
9 | | lea 160 |
. . . 4
(a ∩ b⊥ ) ≤ a |
10 | 9 | oml2 451 |
. . 3
((a ∩ b⊥ ) ∪ ((a ∩ b⊥ )⊥ ∩
a)) = a |
11 | | ax-a2 31 |
. . 3
((a ∩ b⊥ ) ∪ (a ∩ b)) =
((a ∩ b) ∪ (a
∩ b⊥
)) |
12 | 8, 10, 11 | 3tr2 64 |
. 2
a = ((a ∩ b) ∪
(a ∩ b⊥ )) |
13 | 12 | df-c1 132 |
1
a C b |