Theorem mdslmd1i

Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2 (meet version). (Contributed by NM, 27-Apr-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	mdslmd1i	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( C MH D <-> ( C i^i B ) MH ( D i^i B ) ) )

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		ssin	|- ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
6	1 2	chjcli	|- ( A vH B ) e. CH
7	3 4 6	chlubi	|- ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) <-> ( C vH D ) C_ ( A vH B ) )
8	5 7	anbi12i	|- ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) <-> ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) )
9		chjcl	|- ( ( x e. CH /\ A e. CH ) -> ( x vH A ) e. CH )
10	1 9	mpan2	|- ( x e. CH -> ( x vH A ) e. CH )
11		sseq1	|- ( y = ( x vH A ) -> ( y C_ D <-> ( x vH A ) C_ D ) )
12		oveq1	|- ( y = ( x vH A ) -> ( y vH C ) = ( ( x vH A ) vH C ) )
13	12	ineq1d	|- ( y = ( x vH A ) -> ( ( y vH C ) i^i D ) = ( ( ( x vH A ) vH C ) i^i D ) )
14		oveq1	|- ( y = ( x vH A ) -> ( y vH ( C i^i D ) ) = ( ( x vH A ) vH ( C i^i D ) ) )
15	13 14	sseq12d	|- ( y = ( x vH A ) -> ( ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) <-> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) )
16	11 15	imbi12d	|- ( y = ( x vH A ) -> ( ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) <-> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
17	16	rspcv	|- ( ( x vH A ) e. CH -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
18	10 17	syl	|- ( x e. CH -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
19	18	adantr	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) ) )
20	1 2 3 4	mdslmd1lem3	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( ( ( x vH A ) C_ D -> ( ( ( x vH A ) vH C ) i^i D ) C_ ( ( x vH A ) vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
21	19 20	syld	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
22	21	ex	|- ( x e. CH -> ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) ) )
23	22	com3l	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> ( x e. CH -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) ) )
24	23	ralrimdv	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) -> A. x e. CH ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
25		mdbr2	|- ( ( C e. CH /\ D e. CH ) -> ( C MH D <-> A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) ) )
26	3 4 25	mp2an	|- ( C MH D <-> A. y e. CH ( y C_ D -> ( ( y vH C ) i^i D ) C_ ( y vH ( C i^i D ) ) ) )
27	3 2	chincli	|- ( C i^i B ) e. CH
28	4 2	chincli	|- ( D i^i B ) e. CH
29	27 28	mdsl2i	|- ( ( C i^i B ) MH ( D i^i B ) <-> A. x e. CH ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ x /\ x C_ ( D i^i B ) ) -> ( ( x vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( x vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
30	24 26 29	3imtr4g	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( C MH D -> ( C i^i B ) MH ( D i^i B ) ) )
31		chincl	|- ( ( x e. CH /\ B e. CH ) -> ( x i^i B ) e. CH )
32	2 31	mpan2	|- ( x e. CH -> ( x i^i B ) e. CH )
33		sseq1	|- ( y = ( x i^i B ) -> ( y C_ ( D i^i B ) <-> ( x i^i B ) C_ ( D i^i B ) ) )
34		oveq1	|- ( y = ( x i^i B ) -> ( y vH ( C i^i B ) ) = ( ( x i^i B ) vH ( C i^i B ) ) )
35	34	ineq1d	|- ( y = ( x i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) = ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) )
36		oveq1	|- ( y = ( x i^i B ) -> ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) = ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) )
37	35 36	sseq12d	|- ( y = ( x i^i B ) -> ( ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) <-> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
38	33 37	imbi12d	|- ( y = ( x i^i B ) -> ( ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) <-> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
39	38	rspcv	|- ( ( x i^i B ) e. CH -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
40	32 39	syl	|- ( x e. CH -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
41	40	adantr	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
42	1 2 3 4	mdslmd1lem4	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
43	41 42	syld	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
44	43	ex	|- ( x e. CH -> ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) ) )
45	44	com3l	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( x e. CH -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) ) )
46	45	ralrimdv	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> A. x e. CH ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )
47		mdbr2	|- ( ( ( C i^i B ) e. CH /\ ( D i^i B ) e. CH ) -> ( ( C i^i B ) MH ( D i^i B ) <-> A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
48	27 28 47	mp2an	|- ( ( C i^i B ) MH ( D i^i B ) <-> A. y e. CH ( y C_ ( D i^i B ) -> ( ( y vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( y vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
49	3 4	mdsl2i	|- ( C MH D <-> A. x e. CH ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) )
50	46 48 49	3imtr4g	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( C i^i B ) MH ( D i^i B ) -> C MH D ) )
51	30 50	impbid	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( C MH D <-> ( C i^i B ) MH ( D i^i B ) ) )
52	8 51	sylan2br	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( C MH D <-> ( C i^i B ) MH ( D i^i B ) ) )