Theorem mdslj1 10246

Description: Join preservation of the one-to-one onto 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
mdslj1	|- (((A MH B /\ B MH* A) /\ (A (_ (C i^i D) /\ (C vH D) (_ (A vH B))) -> ((C vH D) i^i B) = ((C i^i B) vH (D i^i B)))

Proof of Theorem mdslj1

Step	Hyp	Ref	Expression
1		mdslle1.1	. . . . . . . . . . . 12 |- A e. CH
2		mdslle1.2	. . . . . . . . . . . 12 |- B e. CH
3		mdslle1.3	. . . . . . . . . . . 12 |- C e. CH
4	1, 2, 3	3pm3.2i 818	. . . . . . . . . . 11 |- (A e. CH /\ B e. CH /\ C e. CH)
5		dmdsl3t 10242	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (B MH* A /\ A (_ C /\ C (_ (A vH B))) -> ((C i^i B) vH A) = C)
6	4, 5	mpan 695	. . . . . . . . . 10 |- ((B MH* A /\ A (_ C /\ C (_ (A vH B)) -> ((C i^i B) vH A) = C)
7		pm3.27 323	. . . . . . . . . 10 |- ((A MH B /\ B MH* A) -> B MH* A)
8		pm3.26 319	. . . . . . . . . 10 |- ((A (_ C /\ A (_ D) -> A (_ C)
9		pm3.26 319	. . . . . . . . . 10 |- ((C (_ (A vH B) /\ D (_ (A vH B)) -> C (_ (A vH B))
10	6, 7, 8, 9	syl3an 868	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((C i^i B) vH A) = C)
11	3, 2	chincl 9383	. . . . . . . . . . . 12 |- (C i^i B) e. CH
12		mdslle1.4	. . . . . . . . . . . . 13 |- D e. CH
13	12, 2	chincl 9383	. . . . . . . . . . . 12 |- (D i^i B) e. CH
14	11, 13	chub1 9392	. . . . . . . . . . 11 |- (C i^i B) (_ ((C i^i B) vH (D i^i B))
15	11, 13	chjcl 9380	. . . . . . . . . . . 12 |- ((C i^i B) vH (D i^i B)) e. CH
16	11, 15, 1	chlej1 9396	. . . . . . . . . . 11 |- ((C i^i B) (_ ((C i^i B) vH (D i^i B)) -> ((C i^i B) vH A) (_ (((C i^i B) vH (D i^i B)) vH A))
17	14, 16	ax-mp 7	. . . . . . . . . 10 |- ((C i^i B) vH A) (_ (((C i^i B) vH (D i^i B)) vH A)
18	17	a1i 8	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((C i^i B) vH A) (_ (((C i^i B) vH (D i^i B)) vH A))
19	10, 18	eqsstr3d 2096	. . . . . . . 8 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> C (_ (((C i^i B) vH (D i^i B)) vH A))
20	1, 2, 12	3pm3.2i 818	. . . . . . . . . . 11 |- (A e. CH /\ B e. CH /\ D e. CH)
21		dmdsl3t 10242	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH /\ D e. CH) /\ (B MH* A /\ A (_ D /\ D (_ (A vH B))) -> ((D i^i B) vH A) = D)
22	20, 21	mpan 695	. . . . . . . . . 10 |- ((B MH* A /\ A (_ D /\ D (_ (A vH B)) -> ((D i^i B) vH A) = D)
23		pm3.27 323	. . . . . . . . . 10 |- ((A (_ C /\ A (_ D) -> A (_ D)
24		pm3.27 323	. . . . . . . . . 10 |- ((C (_ (A vH B) /\ D (_ (A vH B)) -> D (_ (A vH B))
25	22, 7, 23, 24	syl3an 868	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((D i^i B) vH A) = D)
26	13, 11	chub2 9393	. . . . . . . . . . 11 |- (D i^i B) (_ ((C i^i B) vH (D i^i B))
27	13, 15, 1	chlej1 9396	. . . . . . . . . . 11 |- ((D i^i B) (_ ((C i^i B) vH (D i^i B)) -> ((D i^i B) vH A) (_ (((C i^i B) vH (D i^i B)) vH A))
28	26, 27	ax-mp 7	. . . . . . . . . 10 |- ((D i^i B) vH A) (_ (((C i^i B) vH (D i^i B)) vH A)
29	28	a1i 8	. . . . . . . . 9 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((D i^i B) vH A) (_ (((C i^i B) vH (D i^i B)) vH A))
30	25, 29	eqsstr3d 2096	. . . . . . . 8 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> D (_ (((C i^i B) vH (D i^i B)) vH A))
31	19, 30	jca 288	. . . . . . 7 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> (C (_ (((C i^i B) vH (D i^i B)) vH A) /\ D (_ (((C i^i B) vH (D i^i B)) vH A)))
32	15, 1	chjcl 9380	. . . . . . . 8 |- (((C i^i B) vH (D i^i B)) vH A) e. CH
33	3, 12, 32	chlub 9394	. . . . . . 7 |- ((C (_ (((C i^i B) vH (D i^i B)) vH A) /\ D (_ (((C i^i B) vH (D i^i B)) vH A)) <-> (C vH D) (_ (((C i^i B) vH (D i^i B)) vH A))
34	31, 33	sylib 198	. . . . . 6 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> (C vH D) (_ (((C i^i B) vH (D i^i B)) vH A))
35		ssrin 2234	. . . . . 6 |- ((C vH D) (_ (((C i^i B) vH (D i^i B)) vH A) -> ((C vH D) i^i B) (_ ((((C i^i B) vH (D i^i B)) vH A) i^i B))
36	34, 35	syl 10	. . . . 5 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((C vH D) i^i B) (_ ((((C i^i B) vH (D i^i B)) vH A) i^i B))
37	1, 2, 15	3pm3.2i 818	. . . . . . 7 |- (A e. CH /\ B e. CH /\ ((C i^i B) vH (D i^i B)) e. CH)
38		mdsl3t 10243	. . . . . . 7 |- (((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 i^i B) vH (D i^i B)) /\ ((C i^i B) vH (D i^i B)) (_ B)) -> ((((C i^i B) vH (D i^i B)) vH A) i^i B) = ((C i^i B) vH (D i^i B)))
39	37, 38	mpan 695	. . . . . 6 |- ((A MH B /\ (A i^i B) (_ ((C i^i B) vH (D i^i B)) /\ ((C i^i B) vH (D i^i B)) (_ B) -> ((((C i^i B) vH (D i^i B)) vH A) i^i B) = ((C i^i B) vH (D i^i B)))
40		pm3.26 319	. . . . . 6 |- ((A MH B /\ B MH* A) -> A MH B)
41		ssrin 2234	. . . . . . . 8 |- (A (_ C -> (A i^i B) (_ (C i^i B))
42		sstr 2072	. . . . . . . . 9 |- (((A i^i B) (_ (C i^i B) /\ (C i^i B) (_ ((C i^i B) vH (D i^i B))) -> (A i^i B) (_ ((C i^i B) vH (D i^i B)))
43	14, 42	mpan2 696	. . . . . . . 8 |- ((A i^i B) (_ (C i^i B) -> (A i^i B) (_ ((C i^i B) vH (D i^i B)))
44	41, 43	syl 10	. . . . . . 7 |- (A (_ C -> (A i^i B) (_ ((C i^i B) vH (D i^i B)))
45	44	adantr 389	. . . . . 6 |- ((A (_ C /\ A (_ D) -> (A i^i B) (_ ((C i^i B) vH (D i^i B)))
46	11, 13, 2	chlub 9394	. . . . . . . . 9 |- (((C i^i B) (_ B /\ (D i^i B) (_ B) <-> ((C i^i B) vH (D i^i B)) (_ B)
47	46	bicomi 172	. . . . . . . 8 |- (((C i^i B) vH (D i^i B)) (_ B <-> ((C i^i B) (_ B /\ (D i^i B) (_ B))
48		inss2 2231	. . . . . . . 8 |- (C i^i B) (_ B
49		inss2 2231	. . . . . . . 8 |- (D i^i B) (_ B
50	47, 48, 49	mpbir2an 730	. . . . . . 7 |- ((C i^i B) vH (D i^i B)) (_ B
51	50	a1i 8	. . . . . 6 |- ((C (_ (A vH B) /\ D (_ (A vH B)) -> ((C i^i B) vH (D i^i B)) (_ B)
52	39, 40, 45, 51	syl3an 868	. . . . 5 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (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)))
53	36, 52	sseqtrd 2097	. . . 4 |- (((A MH B /\ B MH* A) /\ (A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((C vH D) i^i B) (_ ((