Metamath Proof Explorer

Theorem mdslmd3i

Description: Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of MaedaMaeda p. 2. (Contributed by NM, 23-Dec-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 mdslmd3i 
|- ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) -> D MH ( B i^i C ) )

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 chlej2 
 |-  ( ( ( D e. CH /\ A e. CH /\ x e. CH ) /\ D C_ A ) -> ( x vH D ) C_ ( x vH A ) )
6 5 ex 
 |-  ( ( D e. CH /\ A e. CH /\ x e. CH ) -> ( D C_ A -> ( x vH D ) C_ ( x vH A ) ) )
7 4 1 6 mp3an12 
 |-  ( x e. CH -> ( D C_ A -> ( x vH D ) C_ ( x vH A ) ) )
8 7 impcom 
 |-  ( ( D C_ A /\ x e. CH ) -> ( x vH D ) C_ ( x vH A ) )
9 8 ssrind 
 |-  ( ( D C_ A /\ x e. CH ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) )
10 9 adantll 
 |-  ( ( ( ( A i^i C ) C_ D /\ D C_ A ) /\ x e. CH ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) )
11 10 adantll 
 |-  ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) )
12 11 adantr 
 |-  ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) )
13 ssin 
 |-  ( ( x C_ B /\ x C_ C ) <-> x C_ ( B i^i C ) )
14 inass 
 |-  ( ( ( x vH A ) i^i B ) i^i C ) = ( ( x vH A ) i^i ( B i^i C ) )
15 mdi 
 |-  ( ( ( A e. CH /\ B e. CH /\ x e. CH ) /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
16 1 15 mp3anl1 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
17 2 16 mpanl1 
 |-  ( ( x e. CH /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
18 17 ineq1d 
 |-  ( ( x e. CH /\ ( A MH B /\ x C_ B ) ) -> ( ( ( x vH A ) i^i B ) i^i C ) = ( ( x vH ( A i^i B ) ) i^i C ) )
19 14 18 eqtr3id 
 |-  ( ( x e. CH /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( ( x vH ( A i^i B ) ) i^i C ) )
20 19 adantrlr 
 |-  ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ x C_ B ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( ( x vH ( A i^i B ) ) i^i C ) )
21 20 adantrrr 
 |-  ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( ( x vH ( A i^i B ) ) i^i C ) )
22 1 2 chincli 
 |-  ( A i^i B ) e. CH
23 mdi 
 |-  ( ( ( ( A i^i B ) e. CH /\ C e. CH /\ x e. CH ) /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( ( A i^i B ) i^i C ) ) )
24 22 23 mp3anl1 
 |-  ( ( ( C e. CH /\ x e. CH ) /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( ( A i^i B ) i^i C ) ) )
25 3 24 mpanl1 
 |-  ( ( x e. CH /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( ( A i^i B ) i^i C ) ) )
26 inass 
 |-  ( ( A i^i B ) i^i C ) = ( A i^i ( B i^i C ) )
27 26 oveq2i 
 |-  ( x vH ( ( A i^i B ) i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) )
28 25 27 eqtrdi 
 |-  ( ( x e. CH /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( A i^i ( B i^i C ) ) ) )
29 28 adantrll 
 |-  ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( A i^i ( B i^i C ) ) ) )
30 29 adantrrl 
 |-  ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( A i^i ( B i^i C ) ) ) )
31 21 30 eqtrd 
 |-  ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) )
32 31 ancoms 
 |-  ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) /\ x e. CH ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) )
33 32 an32s 
 |-  ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ x e. CH ) /\ ( x C_ B /\ x C_ C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) )
34 13 33 sylan2br 
 |-  ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) )
35 34 adantllr 
 |-  ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) )
36 inass 
 |-  ( ( A i^i C ) i^i ( B i^i C ) ) = ( A i^i ( C i^i ( B i^i C ) ) )
37 in12 
 |-  ( C i^i ( B i^i C ) ) = ( B i^i ( C i^i C ) )
38 inidm 
 |-  ( C i^i C ) = C
39 38 ineq2i 
 |-  ( B i^i ( C i^i C ) ) = ( B i^i C )
40 37 39 eqtri 
 |-  ( C i^i ( B i^i C ) ) = ( B i^i C )
41 40 ineq2i 
 |-  ( A i^i ( C i^i ( B i^i C ) ) ) = ( A i^i ( B i^i C ) )
42 36 41 eqtr2i 
 |-  ( A i^i ( B i^i C ) ) = ( ( A i^i C ) i^i ( B i^i C ) )
43 ssrin 
 |-  ( ( A i^i C ) C_ D -> ( ( A i^i C ) i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) )
44 42 43 eqsstrid 
 |-  ( ( A i^i C ) C_ D -> ( A i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) )
45 ssrin 
 |-  ( D C_ A -> ( D i^i ( B i^i C ) ) C_ ( A i^i ( B i^i C ) ) )
46 44 45 anim12i 
 |-  ( ( ( A i^i C ) C_ D /\ D C_ A ) -> ( ( A i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) /\ ( D i^i ( B i^i C ) ) C_ ( A i^i ( B i^i C ) ) ) )
47 eqss 
 |-  ( ( A i^i ( B i^i C ) ) = ( D i^i ( B i^i C ) ) <-> ( ( A i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) /\ ( D i^i ( B i^i C ) ) C_ ( A i^i ( B i^i C ) ) ) )
48 46 47 sylibr 
 |-  ( ( ( A i^i C ) C_ D /\ D C_ A ) -> ( A i^i ( B i^i C ) ) = ( D i^i ( B i^i C ) ) )
49 48 oveq2d 
 |-  ( ( ( A i^i C ) C_ D /\ D C_ A ) -> ( x vH ( A i^i ( B i^i C ) ) ) = ( x vH ( D i^i ( B i^i C ) ) ) )
50 49 ad3antlr 
 |-  ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( x vH ( A i^i ( B i^i C ) ) ) = ( x vH ( D i^i ( B i^i C ) ) ) )
51 35 50 eqtrd 
 |-  ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( D i^i ( B i^i C ) ) ) )
52 12 51 sseqtrd 
 |-  ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) )
53 52 ex 
 |-  ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) -> ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) )
54 53 ralrimiva 
 |-  ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) -> A. x e. CH ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) )
55 2 3 chincli 
 |-  ( B i^i C ) e. CH
56 mdbr2 
 |-  ( ( D e. CH /\ ( B i^i C ) e. CH ) -> ( D MH ( B i^i C ) <-> A. x e. CH ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) ) )
57 4 55 56 mp2an 
 |-  ( D MH ( B i^i C ) <-> A. x e. CH ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) )
58 54 57 sylibr 
 |-  ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) -> D MH ( B i^i C ) )