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