Theorem cmdmdi

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

	Ref	Expression
Hypotheses	sumdmdi.1	|- A e. CH
	sumdmdi.2	|- B e. CH
Assertion	cmdmdi	|- ( A C_H B -> A MH* B )

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	|- A e. CH
2		sumdmdi.2	|- B e. CH
3	1	choccli	|- ( _|_ ` A ) e. CH
4	2	choccli	|- ( _|_ ` B ) e. CH
5	3 4	cmmdi	|- ( ( _|_ ` A ) C_H ( _|_ ` B ) -> ( _|_ ` A ) MH ( _|_ ` B ) )
6	1 2	cmcm4i	|- ( A C_H B <-> ( _|_ ` A ) C_H ( _|_ ` B ) )
7		dmdmd	|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> ( _|_ ` A ) MH ( _|_ ` B ) ) )
8	1 2 7	mp2an	|- ( A MH* B <-> ( _|_ ` A ) MH ( _|_ ` B ) )
9	5 6 8	3imtr4i	|- ( A C_H B -> A MH* B )