Theorem mdslj2i

Description: Meet preservation of the reverse 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	mdslj2i	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A i^i B ) C_ ( C i^i D ) /\ ( C vH D ) C_ B ) ) -> ( ( C i^i D ) vH A ) = ( ( C vH A ) i^i ( D vH A ) ) )

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