Theorem dmdcompli

Description: A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdcompl.1	|- A e. CH
	mdcompl.2	|- B e. CH
Assertion	dmdcompli	|- ( A MH* B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdcompl.1	|- A e. CH
2		mdcompl.2	|- B e. CH
3	1 2	chincli	|- ( A i^i B ) e. CH
4	3	mdoc1i	|- ( A i^i B ) MH ( _|_ ` ( A i^i B ) )
5	3	dmdoc2i	|- ( _|_ ` ( A i^i B ) ) MH* ( A i^i B )
6		ssid	|- ( A i^i B ) C_ ( A i^i B )
7	1 2	chjcli	|- ( A vH B ) e. CH
8	7	chssii	|- ( A vH B ) C_ ~H
9	3	chjoi	|- ( ( A i^i B ) vH ( _|_ ` ( A i^i B ) ) ) = ~H
10	8 9	sseqtrri	|- ( A vH B ) C_ ( ( A i^i B ) vH ( _|_ ` ( A i^i B ) ) )
11	3	choccli	|- ( _|_ ` ( A i^i B ) ) e. CH
12	3 11 1 2	mdsldmd1i	|- ( ( ( ( A i^i B ) MH ( _|_ ` ( A i^i B ) ) /\ ( _|_ ` ( A i^i B ) ) MH* ( A i^i B ) ) /\ ( ( A i^i B ) C_ ( A i^i B ) /\ ( A vH B ) C_ ( ( A i^i B ) vH ( _|_ ` ( A i^i B ) ) ) ) ) -> ( A MH* B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) ) )
13	4 5 6 10 12	mp4an	|- ( A MH* B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) )