Theorem mdslj1i

Description: Join preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslle1.1	|- A e. CH
	mdslle1.2	|- B e. CH
	mdslle1.3	|- C e. CH
	mdslle1.4	|- D e. CH
Assertion	mdslj1i	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdslle1.1	|- A e. CH
2		mdslle1.2	|- B e. CH
3		mdslle1.3	|- C e. CH
4		mdslle1.4	|- D e. CH
5		ssin	|- ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
6	5	bicomi	|- ( A C_ ( C i^i D ) <-> ( A C_ C /\ A C_ D ) )
7	1 2	chjcli	|- ( A vH B ) e. CH
8	3 4 7	chlubi	|- ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) <-> ( C vH D ) C_ ( A vH B ) )
9	8	bicomi	|- ( ( C vH D ) C_ ( A vH B ) <-> ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) )
10	6 9	anbi12i	|- ( ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) <-> ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) )
11		simpr	|- ( ( A MH B /\ B MH* A ) -> B MH* A )
12		simpl	|- ( ( A C_ C /\ A C_ D ) -> A C_ C )
13		simpl	|- ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> C C_ ( A vH B ) )
14	1 2 3	3pm3.2i	|- ( A e. CH /\ B e. CH /\ C e. CH )
15		dmdsl3	|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH A ) = C )
16	14 15	mpan	|- ( ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) -> ( ( C i^i B ) vH A ) = C )
17	11 12 13 16	syl3an	|- ( ( ( 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 ) vH A ) = C )
18	3 2	chincli	|- ( C i^i B ) e. CH
19	4 2	chincli	|- ( D i^i B ) e. CH
20	18 19	chub1i	|- ( C i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) )
21	18 19	chjcli	|- ( ( C i^i B ) vH ( D i^i B ) ) e. CH
22	18 21 1	chlej1i	|- ( ( C i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) -> ( ( C i^i B ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
23	20 22	mp1i	|- ( ( ( 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 ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
24	17 23	eqsstrrd	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> C C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
25		simpr	|- ( ( A C_ C /\ A C_ D ) -> A C_ D )
26		simpr	|- ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> D C_ ( A vH B ) )
27	1 2 4	3pm3.2i	|- ( A e. CH /\ B e. CH /\ D e. CH )
28		dmdsl3	|- ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
29	27 28	mpan	|- ( ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) -> ( ( D i^i B ) vH A ) = D )
30	11 25 26 29	syl3an	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
31	19 18	chub2i	|- ( D i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) )
32	19 21 1	chlej1i	|- ( ( D i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) -> ( ( D i^i B ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
33	31 32	mp1i	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
34	30 33	eqsstrrd	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> D C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
35	24 34	jca	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( C C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) /\ D C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) ) )
36	21 1	chjcli	|- ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) e. CH
37	3 4 36	chlubi	|- ( ( C C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) /\ D C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) ) <-> ( C vH D ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
38	35 37	sylib	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( C vH D ) C_ ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) )
39	38	ssrind	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) i^i B ) )
40		simpl	|- ( ( A MH B /\ B MH* A ) -> A MH B )
41		ssrin	|- ( A C_ C -> ( A i^i B ) C_ ( C i^i B ) )
42	41 20	sstrdi	|- ( A C_ C -> ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
43	42	adantr	|- ( ( A C_ C /\ A C_ D ) -> ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
44		inss2	|- ( C i^i B ) C_ B
45		inss2	|- ( D i^i B ) C_ B
46	18 19 2	chlubi	|- ( ( ( C i^i B ) C_ B /\ ( D i^i B ) C_ B ) <-> ( ( C i^i B ) vH ( D i^i B ) ) C_ B )
47	46	bicomi	|- ( ( ( C i^i B ) vH ( D i^i B ) ) C_ B <-> ( ( C i^i B ) C_ B /\ ( D i^i B ) C_ B ) )
48	44 45 47	mpbir2an	|- ( ( C i^i B ) vH ( D i^i B ) ) C_ B
49	48	a1i	|- ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> ( ( C i^i B ) vH ( D i^i B ) ) C_ B )
50	1 2 21	3pm3.2i	|- ( A e. CH /\ B e. CH /\ ( ( C i^i B ) vH ( D i^i B ) ) e. CH )
51		mdsl3	|- ( ( ( A e. CH /\ B e. CH /\ ( ( C i^i B ) vH ( D i^i B ) ) e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) /\ ( ( C i^i B ) vH ( D i^i B ) ) C_ B ) ) -> ( ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )
52	50 51	mpan	|- ( ( A MH B /\ ( A i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) /\ ( ( C i^i B ) vH ( D i^i B ) ) C_ B ) -> ( ( ( ( C i^i B ) vH ( D i^i B ) ) vH A ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )
53	40 43 49 52	syl3an	|- ( ( ( 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 ) vH ( D i^i B ) ) vH A ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )
54	39 53	sseqtrd	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
55	54	3expb	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
56	10 55	sylan2b	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) C_ ( ( C i^i B ) vH ( D i^i B ) ) )
57	3 4 2	lediri	|- ( ( C i^i B ) vH ( D i^i B ) ) C_ ( ( C vH D ) i^i B )
58	57	a1i	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH ( D i^i B ) ) C_ ( ( C vH D ) i^i B ) )
59	56 58	eqssd	|- ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( C i^i D ) /\ ( C vH D ) C_ ( A vH B ) ) ) -> ( ( C vH D ) i^i B ) = ( ( C i^i B ) vH ( D i^i B ) ) )