Theorem dmdsym

Description: Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	dmdsym	|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> B MH* A ) )

Proof

Step	Hyp	Ref	Expression
1		choccl	|- ( A e. CH -> ( _|_ ` A ) e. CH )
2		choccl	|- ( B e. CH -> ( _|_ ` B ) e. CH )
3		mdsym	|- ( ( ( _|_ ` A ) e. CH /\ ( _|_ ` B ) e. CH ) -> ( ( _|_ ` A ) MH ( _|_ ` B ) <-> ( _|_ ` B ) MH ( _|_ ` A ) ) )
4	1 2 3	syl2an	|- ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` A ) MH ( _|_ ` B ) <-> ( _|_ ` B ) MH ( _|_ ` A ) ) )
5		dmdmd	|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> ( _|_ ` A ) MH ( _|_ ` B ) ) )
6		dmdmd	|- ( ( B e. CH /\ A e. CH ) -> ( B MH* A <-> ( _|_ ` B ) MH ( _|_ ` A ) ) )
7	6	ancoms	|- ( ( A e. CH /\ B e. CH ) -> ( B MH* A <-> ( _|_ ` B ) MH ( _|_ ` A ) ) )
8	4 5 7	3bitr4d	|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> B MH* A ) )