Metamath Proof Explorer

Theorem mdsldmd1i

Description: Preservation of the dual modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mdslmd.1 
 |-  A e. CH
2 mdslmd.2 
 |-  B e. CH
3 mdslmd.3 
 |-  C e. CH
4 mdslmd.4 
 |-  D e. CH
5 mddmd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> ( _|_ ` A ) MH* ( _|_ ` B ) ) )
6 1 2 5 mp2an 
 |-  ( A MH B <-> ( _|_ ` A ) MH* ( _|_ ` B ) )
7 dmdmd 
 |-  ( ( B e. CH /\ A e. CH ) -> ( B MH* A <-> ( _|_ ` B ) MH ( _|_ ` A ) ) )
8 2 1 7 mp2an 
 |-  ( B MH* A <-> ( _|_ ` B ) MH ( _|_ ` A ) )
9 6 8 anbi12ci 
 |-  ( ( A MH B /\ B MH* A ) <-> ( ( _|_ ` B ) MH ( _|_ ` A ) /\ ( _|_ ` A ) MH* ( _|_ ` B ) ) )
10 3 4 chincli 
 |-  ( C i^i D ) e. CH
11 1 10 chsscon3i 
 |-  ( A C_ ( C i^i D ) <-> ( _|_ ` ( C i^i D ) ) C_ ( _|_ ` A ) )
12 3 4 chdmm1i 
 |-  ( _|_ ` ( C i^i D ) ) = ( ( _|_ ` C ) vH ( _|_ ` D ) )
13 12 sseq1i 
 |-  ( ( _|_ ` ( C i^i D ) ) C_ ( _|_ ` A ) <-> ( ( _|_ ` C ) vH ( _|_ ` D ) ) C_ ( _|_ ` A ) )
14 11 13 bitri 
 |-  ( A C_ ( C i^i D ) <-> ( ( _|_ ` C ) vH ( _|_ ` D ) ) C_ ( _|_ ` A ) )
15 3 4 chjcli 
 |-  ( C vH D ) e. CH
16 1 2 chjcli 
 |-  ( A vH B ) e. CH
17 15 16 chsscon3i 
 |-  ( ( C vH D ) C_ ( A vH B ) <-> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( C vH D ) ) )
18 1 2 chdmj1i 
 |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )
19 incom 
 |-  ( ( _|_ ` A ) i^i ( _|_ ` B ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
20 18 19 eqtri 
 |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
21 3 4 chdmj1i 
 |-  ( _|_ ` ( C vH D ) ) = ( ( _|_ ` C ) i^i ( _|_ ` D ) )
22 20 21 sseq12i 
 |-  ( ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( C vH D ) ) <-> ( ( _|_ ` B ) i^i ( _|_ ` A ) ) C_ ( ( _|_ ` C ) i^i ( _|_ ` D ) ) )
23 17 22 bitri 
 |-  ( ( C vH D ) C_ ( A vH B ) <-> ( ( _|_ ` B ) i^i ( _|_ ` A ) ) C_ ( ( _|_ ` C ) i^i ( _|_ ` D ) ) )
24 14 23 anbi12ci 
 |-  ( ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) <-> ( ( ( _|_ ` B ) i^i ( _|_ ` A ) ) C_ ( ( _|_ ` C ) i^i ( _|_ ` D ) ) /\ ( ( _|_ ` C ) vH ( _|_ ` D ) ) C_ ( _|_ ` A ) ) )
25 2 choccli 
 |-  ( _|_ ` B ) e. CH
26 1 choccli 
 |-  ( _|_ ` A ) e. CH
27 3 choccli 
 |-  ( _|_ ` C ) e. CH
28 4 choccli 
 |-  ( _|_ ` D ) e. CH
29 25 26 27 28 mdslmd2i 
 |-  ( ( ( ( _|_ ` B ) MH ( _|_ ` A ) /\ ( _|_ ` A ) MH* ( _|_ ` B ) ) /\ ( ( ( _|_ ` B ) i^i ( _|_ ` A ) ) C_ ( ( _|_ ` C ) i^i ( _|_ ` D ) ) /\ ( ( _|_ ` C ) vH ( _|_ ` D ) ) C_ ( _|_ ` A ) ) ) -> ( ( _|_ ` C ) MH ( _|_ ` D ) <-> ( ( _|_ ` C ) vH ( _|_ ` B ) ) MH ( ( _|_ ` D ) vH ( _|_ ` B ) ) ) )
30 9 24 29 syl2anb 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( _|_ ` C ) MH ( _|_ ` D ) <-> ( ( _|_ ` C ) vH ( _|_ ` B ) ) MH ( ( _|_ ` D ) vH ( _|_ ` B ) ) ) )
31 dmdmd 
 |-  ( ( C e. CH /\ D e. CH ) -> ( C MH* D <-> ( _|_ ` C ) MH ( _|_ ` D ) ) )
32 3 4 31 mp2an 
 |-  ( C MH* D <-> ( _|_ ` C ) MH ( _|_ ` D ) )
33 3 2 chincli 
 |-  ( C i^i B ) e. CH
34 4 2 chincli 
 |-  ( D i^i B ) e. CH
35 dmdmd 
 |-  ( ( ( C i^i B ) e. CH /\ ( D i^i B ) e. CH ) -> ( ( C i^i B ) MH* ( D i^i B ) <-> ( _|_ ` ( C i^i B ) ) MH ( _|_ ` ( D i^i B ) ) ) )
36 33 34 35 mp2an 
 |-  ( ( C i^i B ) MH* ( D i^i B ) <-> ( _|_ ` ( C i^i B ) ) MH ( _|_ ` ( D i^i B ) ) )
37 3 2 chdmm1i 
 |-  ( _|_ ` ( C i^i B ) ) = ( ( _|_ ` C ) vH ( _|_ ` B ) )
38 4 2 chdmm1i 
 |-  ( _|_ ` ( D i^i B ) ) = ( ( _|_ ` D ) vH ( _|_ ` B ) )
39 37 38 breq12i 
 |-  ( ( _|_ ` ( C i^i B ) ) MH ( _|_ ` ( D i^i B ) ) <-> ( ( _|_ ` C ) vH ( _|_ ` B ) ) MH ( ( _|_ ` D ) vH ( _|_ ` B ) ) )
40 36 39 bitri 
 |-  ( ( C i^i B ) MH* ( D i^i B ) <-> ( ( _|_ ` C ) vH ( _|_ ` B ) ) MH ( ( _|_ ` D ) vH ( _|_ ` B ) ) )
41 30 32 40 3bitr4g 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( C MH* D <-> ( C i^i B ) MH* ( D i^i B ) ) )