Theorem mdslmd2i

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 (join version). (Contributed by NM, 29-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	mdslmd2i	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( C MH D <-> ( C vH A ) MH ( D vH A ) ) )

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	3 4	chjcli	|- ( C vH D ) e. CH
6	5 2 1	chlej1i	|- ( ( C vH D ) C_ B -> ( ( C vH D ) vH A ) C_ ( B vH A ) )
7	3 4 1	chjjdiri	|- ( ( C vH D ) vH A ) = ( ( C vH A ) vH ( D vH A ) )
8	2 1	chjcomi	|- ( B vH A ) = ( A vH B )
9	6 7 8	3sstr3g	|- ( ( C vH D ) C_ B -> ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) )
10	9	adantl	|- ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) )
11	1 3	chub2i	|- A C_ ( C vH A )
12	1 4	chub2i	|- A C_ ( D vH A )
13	11 12	ssini	|- A C_ ( ( C vH A ) i^i ( D vH A ) )
14	10 13	jctil	|- ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( A C_ ( ( C vH A ) i^i ( D vH A ) ) /\ ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) ) )
15	3 1	chjcli	|- ( C vH A ) e. CH
16	4 1	chjcli	|- ( D vH A ) e. CH
17	1 2 15 16	mdslmd1i	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( ( C vH A ) i^i ( D vH A ) ) /\ ( ( C vH A ) vH ( D vH A ) ) C_ ( A vH B ) ) ) -> ( ( C vH A ) MH ( D vH A ) <-> ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) ) )
18	14 17	sylan2	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( C vH A ) MH ( D vH A ) <-> ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) ) )
19		id	|- ( A MH B -> A MH B )
20		inss1	|- ( C i^i D ) C_ C
21		sstr	|- ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C i^i D ) C_ C ) -> ( A i^i B ) C_ C )
22	20 21	mpan2	|- ( ( A i^i B ) C_ ( C i^i D ) -> ( A i^i B ) C_ C )
23	3 4	chub1i	|- C C_ ( C vH D )
24		sstr	|- ( ( C C_ ( C vH D ) /\ ( C vH D ) C_ B ) -> C C_ B )
25	23 24	mpan	|- ( ( C vH D ) C_ B -> C C_ B )
26	1 2 3	3pm3.2i	|- ( A e. CH /\ B e. CH /\ C e. CH )
27		mdsl3	|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = C )
28	26 27	mpan	|- ( ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) -> ( ( C vH A ) i^i B ) = C )
29	19 22 25 28	syl3an	|- ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( C vH A ) i^i B ) = C )
30		inss2	|- ( C i^i D ) C_ D
31		sstr	|- ( ( ( A i^i B ) C_ ( C i^i D ) /\ ( C i^i D ) C_ D ) -> ( A i^i B ) C_ D )
32	30 31	mpan2	|- ( ( A i^i B ) C_ ( C i^i D ) -> ( A i^i B ) C_ D )
33	4 3	chub2i	|- D C_ ( C vH D )
34		sstr	|- ( ( D C_ ( C vH D ) /\ ( C vH D ) C_ B ) -> D C_ B )
35	33 34	mpan	|- ( ( C vH D ) C_ B -> D C_ B )
36	1 2 4	3pm3.2i	|- ( A e. CH /\ B e. CH /\ D e. CH )
37		mdsl3	|- ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ D /\ D C_ B ) ) -> ( ( D vH A ) i^i B ) = D )
38	36 37	mpan	|- ( ( A MH B /\ ( A i^i B ) C_ D /\ D C_ B ) -> ( ( D vH A ) i^i B ) = D )
39	19 32 35 38	syl3an	|- ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( D vH A ) i^i B ) = D )
40	29 39	breq12d	|- ( ( A MH B /\ ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) -> ( ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) <-> C MH D ) )
41	40	3expb	|- ( ( A MH B /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) <-> C MH D ) )
42	41	adantlr	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( ( C vH A ) i^i B ) MH ( ( D vH A ) i^i B ) <-> C MH D ) )
43	18 42	bitr2d	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( C MH D <-> ( C vH A ) MH ( D vH A ) ) )