Metamath Proof Explorer

Theorem mdsl2i

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of MaedaMaeda p. 2. (Contributed by NM, 28-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdsl.1 
|- A e. CH
mdsl.2 
|- B e. CH
Assertion mdsl2i 
|- ( A MH B <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )

Proof

Step Hyp Ref Expression
1 mdsl.1 
 |-  A e. CH
2 mdsl.2 
 |-  B e. CH
3 chub1 
 |-  ( ( x e. CH /\ A e. CH ) -> x C_ ( x vH A ) )
4 1 3 mpan2 
 |-  ( x e. CH -> x C_ ( x vH A ) )
5 iba 
 |-  ( x C_ B -> ( x C_ ( x vH A ) <-> ( x C_ ( x vH A ) /\ x C_ B ) ) )
6 ssin 
 |-  ( ( x C_ ( x vH A ) /\ x C_ B ) <-> x C_ ( ( x vH A ) i^i B ) )
7 5 6 bitrdi 
 |-  ( x C_ B -> ( x C_ ( x vH A ) <-> x C_ ( ( x vH A ) i^i B ) ) )
8 4 7 syl5ibcom 
 |-  ( x e. CH -> ( x C_ B -> x C_ ( ( x vH A ) i^i B ) ) )
9 chub2 
 |-  ( ( A e. CH /\ x e. CH ) -> A C_ ( x vH A ) )
10 1 9 mpan 
 |-  ( x e. CH -> A C_ ( x vH A ) )
11 10 ssrind 
 |-  ( x e. CH -> ( A i^i B ) C_ ( ( x vH A ) i^i B ) )
12 8 11 jctird 
 |-  ( x e. CH -> ( x C_ B -> ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) ) )
13 chjcl 
 |-  ( ( x e. CH /\ A e. CH ) -> ( x vH A ) e. CH )
14 1 13 mpan2 
 |-  ( x e. CH -> ( x vH A ) e. CH )
15 chincl 
 |-  ( ( ( x vH A ) e. CH /\ B e. CH ) -> ( ( x vH A ) i^i B ) e. CH )
16 2 15 mpan2 
 |-  ( ( x vH A ) e. CH -> ( ( x vH A ) i^i B ) e. CH )
17 14 16 syl 
 |-  ( x e. CH -> ( ( x vH A ) i^i B ) e. CH )
18 1 2 chincli 
 |-  ( A i^i B ) e. CH
19 chlub 
 |-  ( ( x e. CH /\ ( A i^i B ) e. CH /\ ( ( x vH A ) i^i B ) e. CH ) -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
20 18 19 mp3an2 
 |-  ( ( x e. CH /\ ( ( x vH A ) i^i B ) e. CH ) -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
21 17 20 mpdan 
 |-  ( x e. CH -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
22 12 21 sylibd 
 |-  ( x e. CH -> ( x C_ B -> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
23 eqss 
 |-  ( ( ( x vH A ) i^i B ) = ( 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 A ) i^i B ) ) )
24 23 rbaib 
 |-  ( ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
25 22 24 syl6 
 |-  ( x e. CH -> ( x C_ B -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
26 25 adantld 
 |-  ( x e. CH -> ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
27 26 pm5.74d 
 |-  ( x e. CH -> ( ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
28 2 1 chub2i 
 |-  B C_ ( A vH B )
29 sstr 
 |-  ( ( x C_ B /\ B C_ ( A vH B ) ) -> x C_ ( A vH B ) )
30 28 29 mpan2 
 |-  ( x C_ B -> x C_ ( A vH B ) )
31 30 pm4.71ri 
 |-  ( x C_ B <-> ( x C_ ( A vH B ) /\ x C_ B ) )
32 31 anbi2i 
 |-  ( ( ( A i^i B ) C_ x /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ ( x C_ ( A vH B ) /\ x C_ B ) ) )
33 anass 
 |-  ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ ( x C_ ( A vH B ) /\ x C_ B ) ) )
34 32 33 bitr4i 
 |-  ( ( ( A i^i B ) C_ x /\ x C_ B ) <-> ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) )
35 34 imbi1i 
 |-  ( ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )
36 27 35 bitr3di 
 |-  ( x e. CH -> ( ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) <-> ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
37 impexp 
 |-  ( ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
38 36 37 bitrdi 
 |-  ( x e. CH -> ( ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) <-> ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) )
39 38 ralbiia 
 |-  ( A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
40 1 2 mdsl1i 
 |-  ( A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) <-> A MH B )
41 39 40 bitr2i 
 |-  ( A MH B <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )