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 AC
mdslle1.2 BC
mdslle1.3 CC
mdslle1.4 DC
Assertion mdslle1i B𝑀*AACDCDABCDCBDB

Proof

Step Hyp Ref Expression
1 mdslle1.1 AC
2 mdslle1.2 BC
3 mdslle1.3 CC
4 mdslle1.4 DC
5 ssrin CDCBDB
6 3 2 chincli CBC
7 4 2 chincli DBC
8 6 7 1 chlej1i CBDBCBADBA
9 id B𝑀*AB𝑀*A
10 ssin ACADACD
11 10 bicomi ACDACAD
12 11 simplbi ACDAC
13 1 2 chjcli ABC
14 3 4 13 chlubi CABDABCDAB
15 14 bicomi CDABCABDAB
16 15 simplbi CDABCAB
17 1 2 3 3pm3.2i ACBCCC
18 dmdsl3 ACBCCCB𝑀*AACCABCBA=C
19 17 18 mpan B𝑀*AACCABCBA=C
20 9 12 16 19 syl3an B𝑀*AACDCDABCBA=C
21 11 simprbi ACDAD
22 15 simprbi CDABDAB
23 1 2 4 3pm3.2i ACBCDC
24 dmdsl3 ACBCDCB𝑀*AADDABDBA=D
25 23 24 mpan B𝑀*AADDABDBA=D
26 9 21 22 25 syl3an B𝑀*AACDCDABDBA=D
27 20 26 sseq12d B𝑀*AACDCDABCBADBACD
28 8 27 syl5ib B𝑀*AACDCDABCBDBCD
29 5 28 impbid2 B𝑀*AACDCDABCDCBDB