This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )