Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  mdslmd2i Unicode version

Theorem mdslmd2i 22910
 Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2 (join version). (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
mdslmd.1
mdslmd.2
mdslmd.3
mdslmd.4
Assertion
Ref Expression
mdslmd2i

Proof of Theorem mdslmd2i
StepHypRef Expression
1 mdslmd.3 . . . . . . . 8
2 mdslmd.4 . . . . . . . 8
31, 2chjcli 22036 . . . . . . 7
4 mdslmd.2 . . . . . . 7
5 mdslmd.1 . . . . . . 7
63, 4, 5chlej1i 22052 . . . . . 6
71, 2, 5chjjdiri 22103 . . . . . 6
84, 5chjcomi 22047 . . . . . 6
96, 7, 83sstr3g 3218 . . . . 5
109adantl 452 . . . 4
115, 1chub2i 22049 . . . . 5
125, 2chub2i 22049 . . . . 5
1311, 12ssini 3392 . . . 4
1410, 13jctil 523 . . 3
151, 5chjcli 22036 . . . 4
162, 5chjcli 22036 . . . 4
175, 4, 15, 16mdslmd1i 22909 . . 3
1814, 17sylan2 460 . 2
19 id 19 . . . . . 6
20 inss1 3389 . . . . . . 7
21 sstr 3187 . . . . . . 7
2220, 21mpan2 652 . . . . . 6
231, 2chub1i 22048 . . . . . . 7
24 sstr 3187 . . . . . . 7
2523, 24mpan 651 . . . . . 6
265, 4, 13pm3.2i 1130 . . . . . . 7
27 mdsl3 22896 . . . . . . 7
2826, 27mpan 651 . . . . . 6
2919, 22, 25, 28syl3an 1224 . . . . 5
30 inss2 3390 . . . . . . 7
31 sstr 3187 . . . . . . 7
3230, 31mpan2 652 . . . . . 6
332, 1chub2i 22049 . . . . . . 7
34 sstr 3187 . . . . . . 7
3533, 34mpan 651 . . . . . 6
365, 4, 23pm3.2i 1130 . . . . . . 7
37 mdsl3 22896 . . . . . . 7
3836, 37mpan 651 . . . . . 6
3919, 32, 35, 38syl3an 1224 . . . . 5
4029, 39breq12d 4036 . . . 4
41403expb 1152 . . 3