Proof of Theorem ud4lem0a
Step | Hyp | Ref
| Expression |
1 | | ud4lem0a.1 |
. . . . 5
a = b |
2 | 1 | lan 77 |
. . . 4
(c ∩ a) = (c ∩
b) |
3 | 1 | lan 77 |
. . . 4
(c⊥ ∩ a) = (c⊥ ∩ b) |
4 | 2, 3 | 2or 72 |
. . 3
((c ∩ a) ∪ (c⊥ ∩ a)) = ((c ∩
b) ∪ (c⊥ ∩ b)) |
5 | 1 | lor 70 |
. . . 4
(c⊥ ∪ a) = (c⊥ ∪ b) |
6 | 1 | ax-r4 37 |
. . . 4
a⊥ = b⊥ |
7 | 5, 6 | 2an 79 |
. . 3
((c⊥ ∪ a) ∩ a⊥ ) = ((c⊥ ∪ b) ∩ b⊥ ) |
8 | 4, 7 | 2or 72 |
. 2
(((c ∩ a) ∪ (c⊥ ∩ a)) ∪ ((c⊥ ∪ a) ∩ a⊥ )) = (((c ∩ b) ∪
(c⊥ ∩ b)) ∪ ((c⊥ ∪ b) ∩ b⊥ )) |
9 | | df-i4 47 |
. 2
(c →4 a) = (((c ∩
a) ∪ (c⊥ ∩ a)) ∪ ((c⊥ ∪ a) ∩ a⊥ )) |
10 | | df-i4 47 |
. 2
(c →4 b) = (((c ∩
b) ∪ (c⊥ ∩ b)) ∪ ((c⊥ ∪ b) ∩ b⊥ )) |
11 | 8, 9, 10 | 3tr1 63 |
1
(c →4 a) = (c
→4 b) |