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

Metamath Proof Explorer

Theorem mdslj1i

Description: Join 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 
|- A e. CH
mdslle1.2 
|- B e. CH
mdslle1.3 
|- C e. CH
mdslle1.4 
|- D e. CH
Assertion mdslj1i 
|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )

Proof

Step Hyp Ref Expression
1 mdslle1.1 
 |-  A e. CH
2 mdslle1.2 
 |-  B e. CH
3 mdslle1.3 
 |-  C e. CH
4 mdslle1.4 
 |-  D e. CH
5 ssin 
 |-  ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
6 5 bicomi 
 |-  ( A C_ ( C i^i D ) <-> ( A C_ C /\ A C_ D ) )
7 1 2 chjcli 
 |-  ( A vH B ) e. CH
8 3 4 7 chlubi 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) <-> ( C vH D ) C_ ( A vH B ) )
9 8 bicomi 
 |-  ( ( C vH D ) C_ ( A vH B ) <-> ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) )
10 6 9 anbi12i 
 |-  ( ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) <-> ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) )
11 simpr 
 |-  ( ( A MH B /\ B MH* A ) -> B MH* A )
12 simpl 
 |-  ( ( A C_ C /\ A C_ D ) -> A C_ C )
13 simpl 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> C C_ ( A vH B ) )
14 1 2 3 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ C e. CH )
15 dmdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH A ) = C )
16 14 15 mpan 
 |-  ( ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) -> ( ( C i^i B ) vH A ) = C )
17 11 12 13 16 syl3an 
 |-  ( ( ( 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 ) vH A ) = C )
18 3 2 chincli 
 |-  ( C i^i B ) e. CH
19 4 2 chincli 
 |-  ( D i^i B ) e. CH
20 18 19 chub1i 
 |-  ( C i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) )
21 18 19 chjcli 
 |-  ( ( C i^i B ) vH ( D i^i B ) ) e. CH
22 18 21 1 chlej1i 
 |-  ( ( C i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) -> ( ( C i^i B ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
23 20 22 mp1i 
 |-  ( ( ( 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 ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
24 17 23 eqsstrrd 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> C C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
25 simpr 
 |-  ( ( A C_ C /\ A C_ D ) -> A C_ D )
26 simpr 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> D C_ ( A vH B ) )
27 1 2 4 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ D e. CH )
28 dmdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
29 27 28 mpan 
 |-  ( ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) -> ( ( D i^i B ) vH A ) = D )
30 11 25 26 29 syl3an 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
31 19 18 chub2i 
 |-  ( D i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) )
32 19 21 1 chlej1i 
 |-  ( ( D i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) -> ( ( D i^i B ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
33 31 32 mp1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
34 30 33 eqsstrrd 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> D C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
35 24 34 jca 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( C C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) /\ D C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) ) )
36 21 1 chjcli 
 |-  ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) e. CH
37 3 4 36 chlubi 
 |-  ( ( C C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) /\ D C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) ) <-> ( C vH D ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
38 35 37 sylib 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( C vH D ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
39 38 ssrind 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) i^i B ) )
40 simpl 
 |-  ( ( A MH B /\ B MH* A ) -> A MH B )
41 ssrin 
 |-  ( A C_ C -> ( A i^i B ) C_ ( C i^i B ) )
42 41 20 sstrdi 
 |-  ( A C_ C -> ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
43 42 adantr 
 |-  ( ( A C_ C /\ A C_ D ) -> ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
44 inss2 
 |-  ( C i^i B ) C_ B
45 inss2 
 |-  ( D i^i B ) C_ B
46 18 19 2 chlubi 
 |-  ( ( ( C i^i B ) C_ B /\ ( D i^i B ) C_ B ) <-> ( ( C i^i B ) vH ( D i^i B ) ) C_ B )
47 46 bicomi 
 |-  ( ( ( C i^i B ) vH ( D i^i B ) ) C_ B <-> ( ( C i^i B ) C_ B /\ ( D i^i B ) C_ B ) )
48 44 45 47 mpbir2an 
 |-  ( ( C i^i B ) vH ( D i^i B ) ) C_ B
49 48 a1i 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> ( ( C i^i B ) vH ( D i^i B ) ) C_ B )
50 1 2 21 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ ( ( C i^i B ) vH ( D i^i B ) ) e. CH )
51 mdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ ( ( C i^i B ) vH ( D i^i B ) ) e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) /\ ( ( C i^i B ) vH ( D i^i B ) ) C_ B ) ) -> ( ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )
52 50 51 mpan 
 |-  ( ( A MH B /\ ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) /\ ( ( C i^i B ) vH ( D i^i B ) ) C_ B ) -> ( ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )
53 40 43 49 52 syl3an 
 |-  ( ( ( 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 ) vH ( D i^i B ) ) vH A ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )
54 39 53 sseqtrd 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
55 54 3expb 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
56 10 55 sylan2b 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
57 3 4 2 lediri 
 |-  ( ( C i^i B ) vH ( D i^i B ) ) C_ ( ( C vH D ) i^i B )
58 57 a1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH ( D i^i B ) ) C_ ( ( C vH D ) i^i B ) )
59 56 58 eqssd 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )