Metamath Proof Explorer

Theorem dmdoc2i

Description: Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis mdoc1.1 
|- A e. CH
Assertion dmdoc2i 
|- ( _|_ ` A ) MH* A

Proof

Step Hyp Ref Expression
1 mdoc1.1 
 |-  A e. CH
2 1 choccli 
 |-  ( _|_ ` A ) e. CH
3 2 dmdoc1i 
 |-  ( _|_ ` A ) MH* ( _|_ ` ( _|_ ` A ) )
4 1 ococi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A
5 3 4 breqtri 
 |-  ( _|_ ` A ) MH* A