Theorem mdoc1i

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

	Ref	Expression
Hypothesis	mdoc1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdoc1i	$$⊢A{𝑀}_{\mathscr{H}}\perp \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdoc1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	cmidi	$$⊢A{𝐶}_{\mathscr{H}}A$$
3	1 1 2	cmcm2ii	$$⊢A{𝐶}_{\mathscr{H}}\perp \left(A\right)$$
4	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 4	cmmdi	$$⊢A{𝐶}_{\mathscr{H}}\perp \left(A\right)\to A{𝑀}_{\mathscr{H}}\perp \left(A\right)$$
6	3 5	ax-mp	$$⊢A{𝑀}_{\mathscr{H}}\perp \left(A\right)$$