Metamath Proof Explorer

Theorem mdslle2i

Description: Order preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mdslle1.1 
 |-  A e. CH
2 mdslle1.2 
 |-  B e. CH
3 mdslle1.3 
 |-  C e. CH
4 mdslle1.4 
 |-  D e. CH
5 3 4 1 chlej1i 
 |-  ( C C_ D -> ( C vH A ) C_ ( D vH A ) )
6 ssrin 
 |-  ( ( C vH A ) C_ ( D vH A ) -> ( ( C vH A ) i^i B ) C_ ( ( D vH A ) i^i B ) )
7 id 
 |-  ( A MH B -> A MH B )
8 ssin 
 |-  ( ( ( A i^i B ) C_ C /\ ( A i^i B ) C_ D ) <-> ( A i^i B ) C_ ( C i^i D ) )
9 8 bicomi 
 |-  ( ( A i^i B ) C_ ( C i^i D ) <-> ( ( A i^i B ) C_ C /\ ( A i^i B ) C_ D ) )
10 9 simplbi 
 |-  ( ( A i^i B ) C_ ( C i^i D ) -> ( A i^i B ) C_ C )
11 3 4 2 chlubi 
 |-  ( ( C C_ B /\ D C_ B ) <-> ( C vH D ) C_ B )
12 11 bicomi 
 |-  ( ( C vH D ) C_ B <-> ( C C_ B /\ D C_ B ) )
13 12 simplbi 
 |-  ( ( C vH D ) C_ B -> C C_ B )
14 1 2 3 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ C e. CH )
15 mdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = C )
16 14 15 mpan 
 |-  ( ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) -> ( ( C vH A ) i^i B ) = C )
17 7 10 13 16 syl3an 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( C vH A ) i^i B ) = C )
18 9 simprbi 
 |-  ( ( A i^i B ) C_ ( C i^i D ) -> ( A i^i B ) C_ D )
19 12 simprbi 
 |-  ( ( C vH D ) C_ B -> D C_ B )
20 1 2 4 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ D e. CH )
21 mdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ D /\ D C_ B ) ) -> ( ( D vH A ) i^i B ) = D )
22 20 21 mpan 
 |-  ( ( A MH B /\ ( A i^i B ) C_ D /\ D C_ B ) -> ( ( D vH A ) i^i B ) = D )
23 7 18 19 22 syl3an 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( D vH A ) i^i B ) = D )
24 17 23 sseq12d 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( ( C vH A ) i^i B ) C_ ( ( D vH A ) i^i B ) <-> C C_ D ) )
25 6 24 imbitrid 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( C vH A ) C_ ( D vH A ) -> C C_ D ) )
26 5 25 impbid2 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( C C_ D <-> ( C vH A ) C_ ( D vH A ) ) )