Metamath Proof Explorer

Theorem mdslle1i

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 mdslle1i 
|- ( ( B MH* A /\ A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) -> ( C C_ D <-> ( C i^i B ) C_ ( D i^i B ) ) )

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 ssrin 
 |-  ( C C_ D -> ( C i^i B ) C_ ( D i^i B ) )
6 3 2 chincli 
 |-  ( C i^i B ) e. CH
7 4 2 chincli 
 |-  ( D i^i B ) e. CH
8 6 7 1 chlej1i 
 |-  ( ( C i^i B ) C_ ( D i^i B ) -> ( ( C i^i B ) vH A ) C_ ( ( D i^i B ) vH A ) )
9 id 
 |-  ( B MH* A -> B MH* A )
10 ssin 
 |-  ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
11 10 bicomi 
 |-  ( A C_ ( C i^i D ) <-> ( A C_ C /\ A C_ D ) )
12 11 simplbi 
 |-  ( A C_ ( C i^i D ) -> A C_ C )
13 1 2 chjcli 
 |-  ( A vH B ) e. CH
14 3 4 13 chlubi 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) <-> ( C vH D ) C_ ( A vH B ) )
15 14 bicomi 
 |-  ( ( C vH D ) C_ ( A vH B ) <-> ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) )
16 15 simplbi 
 |-  ( ( C vH D ) C_ ( A vH B ) -> C C_ ( A vH B ) )
17 1 2 3 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ C e. CH )
18 dmdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH A ) = C )
19 17 18 mpan 
 |-  ( ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) -> ( ( C i^i B ) vH A ) = C )
20 9 12 16 19 syl3an 
 |-  ( ( B MH* A /\ A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) -> ( ( C i^i B ) vH A ) = C )
21 11 simprbi 
 |-  ( A C_ ( C i^i D ) -> A C_ D )
22 15 simprbi 
 |-  ( ( C vH D ) C_ ( A vH B ) -> D C_ ( A vH B ) )
23 1 2 4 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ D e. CH )
24 dmdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
25 23 24 mpan 
 |-  ( ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) -> ( ( D i^i B ) vH A ) = D )
26 9 21 22 25 syl3an 
 |-  ( ( B MH* A /\ A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) -> ( ( D i^i B ) vH A ) = D )
27 20 26 sseq12d 
 |-  ( ( B MH* A /\ A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) -> ( ( ( C i^i B ) vH A ) C_ ( ( D i^i B ) vH A ) <-> C C_ D ) )
28 8 27 syl5ib 
 |-  ( ( B MH* A /\ A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) -> ( ( C i^i B ) C_ ( D i^i B ) -> C C_ D ) )
29 5 28 impbid2 
 |-  ( ( B MH* A /\ A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) -> ( C C_ D <-> ( C i^i B ) C_ ( D i^i B ) ) )