Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | cmcm3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | |
|
2 | fveq2 | |
|
3 | 2 | breq1d | |
4 | 1 3 | bibi12d | |
5 | breq2 | |
|
6 | breq2 | |
|
7 | 5 6 | bibi12d | |
8 | h0elch | |
|
9 | 8 | elimel | |
10 | 8 | elimel | |
11 | 9 10 | cmcm3i | |
12 | 4 7 11 | dedth2h | |