Proof of Theorem oal42
Step | Hyp | Ref
| Expression |
1 | | oal42.1 |
. . 3
(b⊥ ∩
((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c))) |
2 | | ancom 74 |
. . . . 5
(b⊥ ∩ (a →2 b)) = ((a
→2 b) ∩ b⊥ ) |
3 | | u2lemanb 616 |
. . . . 5
((a →2 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ ) |
4 | 2, 3 | ax-r2 36 |
. . . 4
(b⊥ ∩ (a →2 b)) = (a⊥ ∩ b⊥ ) |
5 | | ancom 74 |
. . . . 5
(c⊥ ∩ (a →2 c)) = ((a
→2 c) ∩ c⊥ ) |
6 | | u2lemanb 616 |
. . . . 5
((a →2 c) ∩ c⊥ ) = (a⊥ ∩ c⊥ ) |
7 | 5, 6 | ax-r2 36 |
. . . 4
(c⊥ ∩ (a →2 c)) = (a⊥ ∩ c⊥ ) |
8 | 4, 7 | 2or 72 |
. . 3
((b⊥ ∩
(a →2 b)) ∪ (c⊥ ∩ (a →2 c))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ c⊥ )) |
9 | 1, 8 | lbtr 139 |
. 2
(b⊥ ∩
((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))))) ≤ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ c⊥ )) |
10 | | lea 160 |
. . 3
(a⊥ ∩ b⊥ ) ≤ a⊥ |
11 | | lea 160 |
. . 3
(a⊥ ∩ c⊥ ) ≤ a⊥ |
12 | 10, 11 | lel2or 170 |
. 2
((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ c⊥ )) ≤ a⊥ |
13 | 9, 12 | letr 137 |
1
(b⊥ ∩
((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))))) ≤ a⊥ |