Proof of Theorem gomaex3lem1
Step | Hyp | Ref
| Expression |
1 | | comid 187 |
. . . 4
c C c |
2 | 1 | comcom2 183 |
. . 3
c C c⊥ |
3 | | gomaex3lem1.3 |
. . . 4
c ≤ d⊥ |
4 | 3 | lecom 180 |
. . 3
c C d⊥ |
5 | 2, 4 | fh3 471 |
. 2
(c ∪ (c⊥ ∩ d⊥ )) = ((c ∪ c⊥ ) ∩ (c ∪ d⊥ )) |
6 | | anor3 90 |
. . 3
(c⊥ ∩ d⊥ ) = (c ∪ d)⊥ |
7 | 6 | lor 70 |
. 2
(c ∪ (c⊥ ∩ d⊥ )) = (c ∪ (c ∪
d)⊥ ) |
8 | | ancom 74 |
. . 3
((c ∪ c⊥ ) ∩ (c ∪ d⊥ )) = ((c ∪ d⊥ ) ∩ (c ∪ c⊥ )) |
9 | 3 | df-le2 131 |
. . . . . 6
(c ∪ d⊥ ) = d⊥ |
10 | 9 | ax-r1 35 |
. . . . 5
d⊥ = (c ∪ d⊥ ) |
11 | | df-t 41 |
. . . . 5
1 = (c ∪ c⊥ ) |
12 | 10, 11 | 2an 79 |
. . . 4
(d⊥ ∩ 1) =
((c ∪ d⊥ ) ∩ (c ∪ c⊥ )) |
13 | 12 | ax-r1 35 |
. . 3
((c ∪ d⊥ ) ∩ (c ∪ c⊥ )) = (d⊥ ∩ 1) |
14 | | an1 106 |
. . 3
(d⊥ ∩ 1) =
d⊥ |
15 | 8, 13, 14 | 3tr 65 |
. 2
((c ∪ c⊥ ) ∩ (c ∪ d⊥ )) = d⊥ |
16 | 5, 7, 15 | 3tr2 64 |
1
(c ∪ (c ∪ d)⊥ ) = d⊥ |