Theorem mdslmd4i

Description: Modular pair condition that implies the modular pair property in a sublattice. Lemma 1.5.2 of MaedaMaeda p. 2. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslmd.1	|- A e. CH
	mdslmd.2	|- B e. CH
	mdslmd.3	|- C e. CH
	mdslmd.4	|- D e. CH
Assertion	mdslmd4i	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> C MH D )

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	|- A e. CH
2		mdslmd.2	|- B e. CH
3		mdslmd.3	|- C e. CH
4		mdslmd.4	|- D e. CH
5		simp1	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> A MH B )
6	1 2	chincli	|- ( A i^i B ) e. CH
7		ssmd1	|- ( ( ( A i^i B ) e. CH /\ D e. CH /\ ( A i^i B ) C_ D ) -> ( A i^i B ) MH D )
8	6 4 7	mp3an12	|- ( ( A i^i B ) C_ D -> ( A i^i B ) MH D )
9	8	adantr	|- ( ( ( A i^i B ) C_ D /\ D C_ B ) -> ( A i^i B ) MH D )
10	9	3ad2ant3	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> ( A i^i B ) MH D )
11		sslin	|- ( D C_ B -> ( A i^i D ) C_ ( A i^i B ) )
12		sstr	|- ( ( ( A i^i D ) C_ ( A i^i B ) /\ ( A i^i B ) C_ C ) -> ( A i^i D ) C_ C )
13	11 12	sylan	|- ( ( D C_ B /\ ( A i^i B ) C_ C ) -> ( A i^i D ) C_ C )
14	13	ancoms	|- ( ( ( A i^i B ) C_ C /\ D C_ B ) -> ( A i^i D ) C_ C )
15	14	ad2ant2rl	|- ( ( ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> ( A i^i D ) C_ C )
16	15	3adant1	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> ( A i^i D ) C_ C )
17		simp2r	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> C C_ A )
18	1 2 4 3	mdslmd3i	|- ( ( ( A MH B /\ ( A i^i B ) MH D ) /\ ( ( A i^i D ) C_ C /\ C C_ A ) ) -> C MH ( B i^i D ) )
19	5 10 16 17 18	syl22anc	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> C MH ( B i^i D ) )
20		sseqin2	|- ( D C_ B <-> ( B i^i D ) = D )
21	20	biimpi	|- ( D C_ B -> ( B i^i D ) = D )
22	21	adantl	|- ( ( ( A i^i B ) C_ D /\ D C_ B ) -> ( B i^i D ) = D )
23	22	3ad2ant3	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> ( B i^i D ) = D )
24	19 23	breqtrd	|- ( ( A MH B /\ ( ( A i^i B ) C_ C /\ C C_ A ) /\ ( ( A i^i B ) C_ D /\ D C_ B ) ) -> C MH D )