Theorem mdslj2 10247

Description: Meet preservation of the reverse mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2.

Hypotheses

Ref	Expression
mdslle1.1	|- A e. CH
mdslle1.2	|- B e. CH
mdslle1.3	|- C e. CH
mdslle1.4	|- D e. CH

Assertion

Ref	Expression
mdslj2	|- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ (C i^i D) /\ (C vH D) (_ B)) -> ((C i^i D) vH A) = ((C vH A) i^i (D vH A)))

Proof of Theorem mdslj2

Step	Hyp	Ref	Expression
1		mdslle1.3	. . . 4 |- C e. CH
2		mdslle1.4	. . . 4 |- D e. CH
3		mdslle1.1	. . . 4 |- A e. CH
4	1, 2, 3	lejdir 9462	. . 3 |- ((C i^i D) vH A) (_ ((C vH A) i^i (D vH A))
5	4	a1i 8	. 2 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ (C i^i D) /\ (C vH D) (_ B)) -> ((C i^i D) vH A) (_ ((C vH A) i^i (D vH A)))
6		mdslle1.2	. . . . . . . 8 |- B e. CH
7	1, 3	chjcl 9380	. . . . . . . . 9 |- (C vH A) e. CH
8	2, 3	chjcl 9380	. . . . . . . . 9 |- (D vH A) e. CH
9	7, 8	chincl 9383	. . . . . . . 8 |- ((C vH A) i^i (D vH A)) e. CH
10	3, 6, 9	3pm3.2i 818	. . . . . . 7 |- (A e. CH /\ B e. CH /\ ((C vH A) i^i (D vH A)) e. CH)
11		dmdsl3t 10242	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ ((C vH A) i^i (D vH A)) e. CH) /\ (B MH* A /\ A (_ ((C vH A) i^i (D vH A)) /\ ((C vH A) i^i (D vH A)) (_ (A vH B))) -> ((((C vH A) i^i (D vH A)) i^i B) vH A) = ((C vH A) i^i (D vH A)))
12	10, 11	mpan 695	. . . . . 6 |- ((B MH* A /\ A (_ ((C vH A) i^i (D vH A)) /\ ((C vH A) i^i (D vH A)) (_ (A vH B)) -> ((((C vH A) i^i (D vH A)) i^i B) vH A) = ((C vH A) i^i (D vH A)))
13		pm3.27 323	. . . . . 6 |- ((A MH B /\ B MH* A) -> B MH* A)
14	3, 1	chub2 9393	. . . . . . . 8 |- A (_ (C vH A)
15	3, 2	chub2 9393	. . . . . . . 8 |- A (_ (D vH A)
16	14, 15	ssini 2233	. . . . . . 7 |- A (_ ((C vH A) i^i (D vH A))
17	16	a1i 8	. . . . . 6 |- (((A i^i B) (_ C /\ (A i^i B) (_ D) -> A (_ ((C vH A) i^i (D vH A)))
18	1, 6, 3	chlej1 9396	. . . . . . . . 9 |- (C (_ B -> (C vH A) (_ (B vH A))
19	6, 3	chjcom 9391	. . . . . . . . 9 |- (B vH A) = (A vH B)
20	18, 19	syl6ss 2107	. . . . . . . 8 |- (C (_ B -> (C vH A) (_ (A vH B))
21		ssinss1 2237	. . . . . . . 8 |- ((C vH A) (_ (A vH B) -> ((C vH A) i^i (D vH A)) (_ (A vH B))
22	20, 21	syl 10	. . . . . . 7 |- (C (_ B -> ((C vH A) i^i (D vH A)) (_ (A vH B))
23	22	adantr 389	. . . . . 6 |- ((C (_ B /\ D (_ B) -> ((C vH A) i^i (D vH A)) (_ (A vH B))
24	12, 13, 17, 23	syl3an 868	. . . . 5 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> ((((C vH A) i^i (D vH A)) i^i B) vH A) = ((C vH A) i^i (D vH A)))
25		inss1 2230	. . . . . . . . . . 11 |- ((C vH A) i^i (D vH A)) (_ (C vH A)
26		ssrin 2234	. . . . . . . . . . 11 |- (((C vH A) i^i (D vH A)) (_ (C vH A) -> (((C vH A) i^i (D vH A)) i^i B) (_ ((C vH A) i^i B))
27	25, 26	ax-mp 7	. . . . . . . . . 10 |- (((C vH A) i^i (D vH A)) i^i B) (_ ((C vH A) i^i B)
28	27	a1i 8	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> (((C vH A) i^i (D vH A)) i^i B) (_ ((C vH A) i^i B))
29	3, 6, 1	3pm3.2i 818	. . . . . . . . . . 11 |- (A e. CH /\ B e. CH /\ C e. CH)
30		mdsl3t 10243	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A MH B /\ (A i^i B) (_ C /\ C (_ B)) -> ((C vH A) i^i B) = C)
31	29, 30	mpan 695	. . . . . . . . . 10 |- ((A MH B /\ (A i^i B) (_ C /\ C (_ B) -> ((C vH A) i^i B) = C)
32		pm3.26 319	. . . . . . . . . 10 |- ((A MH B /\ B MH* A) -> A MH B)
33		pm3.26 319	. . . . . . . . . 10 |- (((A i^i B) (_ C /\ (A i^i B) (_ D) -> (A i^i B) (_ C)
34		pm3.26 319	. . . . . . . . . 10 |- ((C (_ B /\ D (_ B) -> C (_ B)
35	31, 32, 33, 34	syl3an 868	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> ((C vH A) i^i B) = C)
36	28, 35	sseqtrd 2097	. . . . . . . 8 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> (((C vH A) i^i (D vH A)) i^i B) (_ C)
37		inss2 2231	. . . . . . . . . . 11 |- ((C vH A) i^i (D vH A)) (_ (D vH A)
38		ssrin 2234	. . . . . . . . . . 11 |- (((C vH A) i^i (D vH A)) (_ (D vH A) -> (((C vH A) i^i (D vH A)) i^i B) (_ ((D vH A) i^i B))
39	37, 38	ax-mp 7	. . . . . . . . . 10 |- (((C vH A) i^i (D vH A)) i^i B) (_ ((D vH A) i^i B)
40	39	a1i 8	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> (((C vH A) i^i (D vH A)) i^i B) (_ ((D vH A) i^i B))
41	3, 6, 2	3pm3.2i 818	. . . . . . . . . . 11 |- (A e. CH /\ B e. CH /\ D e. CH)
42		mdsl3t 10243	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH /\ D e. CH) /\ (A MH B /\ (A i^i B) (_ D /\ D (_ B)) -> ((D vH A) i^i B) = D)
43	41, 42	mpan 695	. . . . . . . . . 10 |- ((A MH B /\ (A i^i B) (_ D /\ D (_ B) -> ((D vH A) i^i B) = D)
44		pm3.27 323	. . . . . . . . . 10 |- (((A i^i B) (_ C /\ (A i^i B) (_ D) -> (A i^i B) (_ D)
45		pm3.27 323	. . . . . . . . . 10 |- ((C (_ B /\ D (_ B) -> D (_ B)
46	43, 32, 44, 45	syl3an 868	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> ((D vH A) i^i B) = D)
47	40, 46	sseqtrd 2097	. . . . . . . 8 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> (((C vH A) i^i (D vH A)) i^i B) (_ D)
48	36, 47	jca 288	. . . . . . 7 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> ((((C vH A) i^i (D vH A)) i^i B) (_ C /\ (((C vH A) i^i (D vH A)) i^i B) (_ D))
49		ssin 2232	. . . . . . 7 |- (((((C vH A) i^i (D vH A)) i^i B) (_ C /\ (((C vH A) i^i (D vH A)) i^i B) (_ D) <-> (((C vH A) i^i (D vH A)) i^i B) (_ (C i^i D))
50	48, 49	sylib 198	. . . . . 6 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> (((C vH A) i^i (D vH A)) i^i B) (_ (C i^i D))
51	9, 6	chincl 9383	. . . . . . 7 |- (((C vH A) i^i (D vH A)) i^i B) e. CH
52	1, 2	chincl 9383	. . . . . . 7 |- (C i^i D) e. CH
53	51, 52, 3	chlej1 9396	. . . . . 6 |- ((((C vH A) i^i (D vH A)) i^i B) (_ (C i^i D) -> ((((C vH A) i^i (D vH A)) i^i B) vH A) (_ ((C i^i D) vH A))
54	50, 53	syl 10	. . . . 5 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> ((((C vH A) i^i (D vH A)) i^i B) vH A) (_ ((C i^i D) vH A))
55	24, 54	eqsstr3d 2096	. . . 4 |- (((A MH B /\ B MH* A) /\ ((A i^i B) (_ C /\ (A i^i B) (_ D) /\ (C (_ B /\ D (_ B)) -> ((C vH A) i^i (D vH A