Metamath Proof Explorer

Theorem mdsl0

Description: A sublattice condition that transfers the modular pair property. Exercise 12 of Kalmbach p. 103. Also Lemma 1.5.3 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdsl0 
|- ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) /\ A MH B ) -> C MH D ) )

Proof

Step Hyp Ref Expression
1 sstr2 
 |-  ( x C_ D -> ( D C_ B -> x C_ B ) )
2 1 com12 
 |-  ( D C_ B -> ( x C_ D -> x C_ B ) )
3 2 ad2antlr 
 |-  ( ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) -> ( x C_ D -> x C_ B ) )
4 3 ad2antlr 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) /\ x e. CH ) -> ( x C_ D -> x C_ B ) )
5 chlej2 
 |-  ( ( ( C e. CH /\ A e. CH /\ x e. CH ) /\ C C_ A ) -> ( x vH C ) C_ ( x vH A ) )
6 ss2in 
 |-  ( ( ( x vH C ) C_ ( x vH A ) /\ D C_ B ) -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) )
7 6 ex 
 |-  ( ( x vH C ) C_ ( x vH A ) -> ( D C_ B -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) ) )
8 5 7 syl 
 |-  ( ( ( C e. CH /\ A e. CH /\ x e. CH ) /\ C C_ A ) -> ( D C_ B -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) ) )
9 8 ex 
 |-  ( ( C e. CH /\ A e. CH /\ x e. CH ) -> ( C C_ A -> ( D C_ B -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) ) ) )
10 9 3expia 
 |-  ( ( C e. CH /\ A e. CH ) -> ( x e. CH -> ( C C_ A -> ( D C_ B -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) ) ) ) )
11 10 ancoms 
 |-  ( ( A e. CH /\ C e. CH ) -> ( x e. CH -> ( C C_ A -> ( D C_ B -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) ) ) ) )
12 11 ad2ant2r 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( x e. CH -> ( C C_ A -> ( D C_ B -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) ) ) ) )
13 12 imp43 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ x e. CH ) /\ ( C C_ A /\ D C_ B ) ) -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) )
14 13 adantrr 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ x e. CH ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) )
15 oveq2 
 |-  ( ( A i^i B ) = 0H -> ( x vH ( A i^i B ) ) = ( x vH 0H ) )
16 chj0 
 |-  ( x e. CH -> ( x vH 0H ) = x )
17 15 16 sylan9eqr 
 |-  ( ( x e. CH /\ ( A i^i B ) = 0H ) -> ( x vH ( A i^i B ) ) = x )
18 17 adantl 
 |-  ( ( ( C e. CH /\ D e. CH ) /\ ( x e. CH /\ ( A i^i B ) = 0H ) ) -> ( x vH ( A i^i B ) ) = x )
19 chincl 
 |-  ( ( C e. CH /\ D e. CH ) -> ( C i^i D ) e. CH )
20 chub1 
 |-  ( ( x e. CH /\ ( C i^i D ) e. CH ) -> x C_ ( x vH ( C i^i D ) ) )
21 20 ancoms 
 |-  ( ( ( C i^i D ) e. CH /\ x e. CH ) -> x C_ ( x vH ( C i^i D ) ) )
22 19 21 sylan 
 |-  ( ( ( C e. CH /\ D e. CH ) /\ x e. CH ) -> x C_ ( x vH ( C i^i D ) ) )
23 22 adantrr 
 |-  ( ( ( C e. CH /\ D e. CH ) /\ ( x e. CH /\ ( A i^i B ) = 0H ) ) -> x C_ ( x vH ( C i^i D ) ) )
24 18 23 eqsstrd 
 |-  ( ( ( C e. CH /\ D e. CH ) /\ ( x e. CH /\ ( A i^i B ) = 0H ) ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) )
25 24 adantll 
 |-  ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( x e. CH /\ ( A i^i B ) = 0H ) ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) )
26 25 anassrs 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ x e. CH ) /\ ( A i^i B ) = 0H ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) )
27 26 adantrl 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ x e. CH ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) )
28 sstr2 
 |-  ( ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( A i^i B ) ) ) )
29 sstr2 
 |-  ( ( ( x vH C ) i^i D ) C_ ( x vH ( A i^i B ) ) -> ( ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) )
30 28 29 syl6 
 |-  ( ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) -> ( ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
31 30 com23 
 |-  ( ( ( x vH C ) i^i D ) C_ ( ( x vH A ) i^i B ) -> ( ( x vH ( A i^i B ) ) C_ ( x vH ( C i^i D ) ) -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
32 14 27 31 sylc 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ x e. CH ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) )
33 32 an32s 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) /\ x e. CH ) -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) )
34 4 33 imim12d 
 |-  ( ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) /\ x e. CH ) -> ( ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) -> ( x C_ D -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
35 34 ralimdva 
 |-  ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) -> A. x e. CH ( x C_ D -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
36 mdbr2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
37 36 ad2antrr 
 |-  ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
38 mdbr2 
 |-  ( ( C e. CH /\ D e. CH ) -> ( C MH D <-> A. x e. CH ( x C_ D -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
39 38 ad2antlr 
 |-  ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( C MH D <-> A. x e. CH ( x C_ D -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
40 35 37 39 3imtr4d 
 |-  ( ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) /\ ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) ) -> ( A MH B -> C MH D ) )
41 40 expimpd 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( ( ( C C_ A /\ D C_ B ) /\ ( A i^i B ) = 0H ) /\ A MH B ) -> C MH D ) )