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

Metamath Proof Explorer

Theorem mdslmd1i

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 (meet version). (Contributed by NM, 27-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 mdslmd1i 
|- ( ( ( 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 ssin 
 |-  ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
6 1 2 chjcli 
 |-  ( A vH B ) e. CH
7 3 4 6 chlubi 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) <-> ( C vH D ) C_ ( A vH B ) )
8 5 7 anbi12i 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) <-> ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) )
9 chjcl 
 |-  ( ( x e. CH /\ A e. CH ) -> ( x vH A ) e. CH )
10 1 9 mpan2 
 |-  ( x e. CH -> ( x vH A ) e. CH )
11 sseq1 
 |-  ( y = ( x vH A ) -> ( y C_ D <-> ( x vH A ) C_ D ) )
12 oveq1 
 |-  ( y = ( x vH A ) -> ( y vH C ) = ( ( x vH A ) vH C ) )
13 12 ineq1d 
 |-  ( y = ( x vH A ) -> ( ( y vH C ) i^i D ) = ( ( ( x vH A ) vH C ) i^i D ) )
14 oveq1 
 |-  ( y = ( x vH A ) -> ( y vH ( C i^i D ) ) = ( ( x vH A ) vH ( C i^i D ) ) )
15 13 14 sseq12d 
 |-  ( y = ( x vH A ) -> ( ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) <-> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) )
16 11 15 imbi12d 
 |-  ( y = ( x vH A ) -> ( ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) <-> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
17 16 rspcv 
 |-  ( ( x vH A ) e. CH -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
18 10 17 syl 
 |-  ( x e. CH -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
19 18 adantr 
 |-  ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
20 1 2 3 4 mdslmd1lem3 
 |-  ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
21 19 20 syld 
 |-  ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
22 21 ex 
 |-  ( x e. CH -> ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) ) )
23 22 com3l 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( x e. CH -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) ) )
24 23 ralrimdv 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> A. x e. CH ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
25 mdbr2 
 |-  ( ( C e. CH /\ D e. CH ) -> ( C MH D <-> A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) ) )
26 3 4 25 mp2an 
 |-  ( C MH D <-> A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) )
27 3 2 chincli 
 |-  ( C i^i B ) e. CH
28 4 2 chincli 
 |-  ( D i^i B ) e. CH
29 27 28 mdsl2i 
 |-  ( ( C i^i B ) MH ( D i^i B ) <-> A. x e. CH ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
30 24 26 29 3imtr4g 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( C MH D -> ( C i^i B ) MH ( D i^i B ) ) )
31 chincl 
 |-  ( ( x e. CH /\ B e. CH ) -> ( x i^i B ) e. CH )
32 2 31 mpan2 
 |-  ( x e. CH -> ( x i^i B ) e. CH )
33 sseq1 
 |-  ( y = ( x i^i B ) -> ( y C_ ( D i^i B ) <-> ( x i^i B ) C_ ( D i^i B ) ) )
34 oveq1 
 |-  ( y = ( x i^i B ) -> ( y vH ( C i^i B ) ) = ( ( x i^i B ) vH ( C i^i B ) ) )
35 34 ineq1d 
 |-  ( y = ( x i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) = ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) )
36 oveq1 
 |-  ( y = ( x i^i B ) -> ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) = ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) )
37 35 36 sseq12d 
 |-  ( y = ( x i^i B ) -> ( ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) <-> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
38 33 37 imbi12d 
 |-  ( y = ( x i^i B ) -> ( ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) <-> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
39 38 rspcv 
 |-  ( ( x i^i B ) e. CH -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
40 32 39 syl 
 |-  ( x e. CH -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
41 40 adantr 
 |-  ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
42 1 2 3 4 mdslmd1lem4 
 |-  ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
43 41 42 syld 
 |-  ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
44 43 ex 
 |-  ( x e. CH -> ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) ) )
45 44 com3l 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( x e. CH -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) ) )
46 45 ralrimdv 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> A. x e. CH ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
47 mdbr2 
 |-  ( ( ( C i^i B ) e. CH /\ ( D i^i B ) e. CH ) -> ( ( C i^i B ) MH ( D i^i B ) <-> A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
48 27 28 47 mp2an 
 |-  ( ( C i^i B ) MH ( D i^i B ) <-> A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
49 3 4 mdsl2i 
 |-  ( C MH D <-> A. x e. CH ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) )
50 46 48 49 3imtr4g 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( C i^i B ) MH ( D i^i B ) -> C MH D ) )
51 30 50 impbid 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( C MH D <-> ( C i^i B ) MH ( D i^i B ) ) )
52 8 51 sylan2br 
 |-  ( ( ( 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 ) ) )