Theorem dmdoc2i

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

	Ref	Expression
Hypothesis	mdoc1.1	⊢ 𝐴 ∈ Cℋ
Assertion	dmdoc2i	⊢ ( ⊥ ‘ 𝐴 ) 𝑀ℋ* 𝐴

Proof

Step	Hyp	Ref	Expression
1		mdoc1.1	⊢ 𝐴 ∈ Cℋ
2	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
3	2	dmdoc1i	⊢ ( ⊥ ‘ 𝐴 ) 𝑀ℋ* ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )
4	1	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
5	3 4	breqtri	⊢ ( ⊥ ‘ 𝐴 ) 𝑀ℋ* 𝐴