This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdslmd2i

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.)

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

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 3 4 chjcli 
 |-  ( C vH D ) e. CH
6 5 2 1 chlej1i 
 |-  ( ( C vH D ) C_ B -> ( ( C vH D ) vH A ) C_ ( B vH A ) )
7 3 4 1 chjjdiri 
 |-  ( ( C vH D ) vH A ) = ( ( C vH A ) vH ( D vH A ) )
8 2 1 chjcomi 
 |-  ( B vH A ) = ( A vH B )
9 6 7 8 3sstr3g 
 |-  ( ( C vH D ) C_ B -> ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) )
10 9 adantl 
 |-  ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) )
11 1 3 chub2i 
 |-  A C_ ( C vH A )
12 1 4 chub2i 
 |-  A C_ ( D vH A )
13 11 12 ssini 
 |-  A C_ ( ( C vH A ) i^i ( D vH A ) )
14 10 13 jctil 
 |-  ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( A C_ ( ( C vH A ) i^i ( D vH A ) ) /\ ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) ) )
15 3 1 chjcli 
 |-  ( C vH A ) e. CH
16 4 1 chjcli 
 |-  ( D vH A ) e. CH
17 1 2 15 16 mdslmd1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( ( C vH A ) i^i ( D vH A ) ) /\ ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) ) ) -> ( ( C vH A ) MH ( D vH A ) <-> ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) ) )
18 14 17 sylan2 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( C vH A ) MH ( D vH A ) <-> ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) ) )
19 id 
 |-  ( A MH B -> A MH B )
20 inss1 
 |-  ( C i^i D ) C_ C
21 sstr 
 |-  ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C i^i D ) C_ C ) -> ( A i^i B ) C_ C )
22 20 21 mpan2 
 |-  ( ( A i^i B ) C_ ( C i^i D ) -> ( A i^i B ) C_ C )
23 3 4 chub1i 
 |-  C C_ ( C vH D )
24 sstr 
 |-  ( ( C C_ ( C vH D ) /\ ( C vH D ) C_ B ) -> C C_ B )
25 23 24 mpan 
 |-  ( ( C vH D ) C_ B -> C C_ B )
26 1 2 3 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ C e. CH )
27 mdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = C )
28 26 27 mpan 
 |-  ( ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) -> ( ( C vH A ) i^i B ) = C )
29 19 22 25 28 syl3an 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( C vH A ) i^i B ) = C )
30 inss2 
 |-  ( C i^i D ) C_ D
31 sstr 
 |-  ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C i^i D ) C_ D ) -> ( A i^i B ) C_ D )
32 30 31 mpan2 
 |-  ( ( A i^i B ) C_ ( C i^i D ) -> ( A i^i B ) C_ D )
33 4 3 chub2i 
 |-  D C_ ( C vH D )
34 sstr 
 |-  ( ( D C_ ( C vH D ) /\ ( C vH D ) C_ B ) -> D C_ B )
35 33 34 mpan 
 |-  ( ( C vH D ) C_ B -> D C_ B )
36 1 2 4 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ D e. CH )
37 mdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ D /\ D C_ B ) ) -> ( ( D vH A ) i^i B ) = D )
38 36 37 mpan 
 |-  ( ( A MH B /\ ( A i^i B ) C_ D /\ D C_ B ) -> ( ( D vH A ) i^i B ) = D )
39 19 32 35 38 syl3an 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( D vH A ) i^i B ) = D )
40 29 39 breq12d 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) <-> C MH D ) )
41 40 3expb 
 |-  ( ( A MH B /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) <-> C MH D ) )
42 41 adantlr 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) <-> C MH D ) )
43 18 42 bitr2d 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( C MH D <-> ( C vH A ) MH ( D vH A ) ) )