Proof of Theorem ud4lem0b
Step | Hyp | Ref
| Expression |
1 | | ud4lem0a.1 |
. . . . 5
a = b |
2 | 1 | ran 78 |
. . . 4
(a ∩ c) = (b ∩
c) |
3 | 1 | ax-r4 37 |
. . . . 5
a⊥ = b⊥ |
4 | 3 | ran 78 |
. . . 4
(a⊥ ∩ c) = (b⊥ ∩ c) |
5 | 2, 4 | 2or 72 |
. . 3
((a ∩ c) ∪ (a⊥ ∩ c)) = ((b ∩
c) ∪ (b⊥ ∩ c)) |
6 | 3 | ax-r5 38 |
. . . 4
(a⊥ ∪ c) = (b⊥ ∪ c) |
7 | 6 | ran 78 |
. . 3
((a⊥ ∪ c) ∩ c⊥ ) = ((b⊥ ∪ c) ∩ c⊥ ) |
8 | 5, 7 | 2or 72 |
. 2
(((a ∩ c) ∪ (a⊥ ∩ c)) ∪ ((a⊥ ∪ c) ∩ c⊥ )) = (((b ∩ c) ∪
(b⊥ ∩ c)) ∪ ((b⊥ ∪ c) ∩ c⊥ )) |
9 | | df-i4 47 |
. 2
(a →4 c) = (((a ∩
c) ∪ (a⊥ ∩ c)) ∪ ((a⊥ ∪ c) ∩ c⊥ )) |
10 | | df-i4 47 |
. 2
(b →4 c) = (((b ∩
c) ∪ (b⊥ ∩ c)) ∪ ((b⊥ ∪ c) ∩ c⊥ )) |
11 | 8, 9, 10 | 3tr1 63 |
1
(a →4 c) = (b
→4 c) |