# 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 ) ) )`