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

Metamath Proof Explorer

Theorem mdslj2i

Description: Meet preservation of the reverse 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 mdslj2i 
|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( C i^i D ) vH A ) = ( ( C vH A ) i^i ( D vH A ) ) )

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