Metamath Proof Explorer


Theorem dmdoc1i

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

Ref Expression
Hypothesis mdoc1.1 𝐴C
Assertion dmdoc1i 𝐴 𝑀* ( ⊥ ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 mdoc1.1 𝐴C
2 1 cmidi 𝐴 𝐶 𝐴
3 1 1 2 cmcm2ii 𝐴 𝐶 ( ⊥ ‘ 𝐴 )
4 1 choccli ( ⊥ ‘ 𝐴 ) ∈ C
5 1 4 cmdmdi ( 𝐴 𝐶 ( ⊥ ‘ 𝐴 ) → 𝐴 𝑀* ( ⊥ ‘ 𝐴 ) )
6 3 5 ax-mp 𝐴 𝑀* ( ⊥ ‘ 𝐴 )