Theorem mddmd

Description: The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

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