Theorem mdslmd1 10247

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 (meet version).

Hypotheses

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

Assertion

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

Proof of Theorem mdslmd1

Step	Hyp	Ref	Expression
1		mdslmd.1	. . . . . . . . . . 11 |- A e. CH
2		chjclt 9317	. . . . . . . . . . 11 |- ((x e. CH /\ A e. CH) -> (x vH A) e. CH)
3	1, 2	mpan2 695	. . . . . . . . . 10 |- (x e. CH -> (x vH A) e. CH)
4		sseq1 2080	. . . . . . . . . . . 12 |- (y = (x vH A) -> (y (_ D <-> (x vH A) (_ D))
5		opreq1 3965	. . . . . . . . . . . . . 14 |- (y = (x vH A) -> (y vH C) = ((x vH A) vH C))
6	5	ineq1d 2214	. . . . . . . . . . . . 13 |- (y = (x vH A) -> ((y vH C) i^i D) = (((x vH A) vH C) i^i D))
7		opreq1 3965	. . . . . . . . . . . . 13 |- (y = (x vH A) -> (y vH (C i^i D)) = ((x vH A) vH (C i^i D)))
8	6, 7	sseq12d 2088	. . . . . . . . . . . 12 |- (y = (x vH A) -> (((y vH C) i^i D) (_ (y vH (C i^i D)) <-> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D))))
9	4, 8	imbi12d 625	. . . . . . . . . . 11 |- (y = (x vH A) -> ((y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) <-> ((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D)))))
10	9	rcla4v 1871	. . . . . . . . . 10 |- ((x vH A) e. CH -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> ((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D)))))
11	3, 10	syl 10	. . . . . . . . 9 |- (x e. CH -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> ((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D)))))
12	11	adantr 389	. . . . . . . 8 |- ((x e. CH /\ ((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))))) -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> ((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D)))))
13		mdslmd.2	. . . . . . . . 9 |- B e. CH
14		mdslmd.3	. . . . . . . . 9 |- C e. CH
15		mdslmd.4	. . . . . . . . 9 |- D e. CH
16	1, 13, 14, 15	mdslmd1lem3 10245	. . . . . . . 8 |- ((x e. CH /\ ((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))))) -> (((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B))))))
17	12, 16	syld 27	. . . . . . 7 |- ((x e. CH /\ ((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))))) -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B))))))
18	17	ex 373	. . . . . 6 |- (x e. CH -> (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B)))))))
19	18	com3l 34	. . . . 5 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> (x e. CH -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B)))))))
20	19	r19.21adv 1717	. . . 4 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))) -> A.x e. CH ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B))))))
21		mdbr2 10214	. . . . 5 |- ((C e. CH /\ D e. CH) -> (C MH D <-> A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D)))))
22	14, 15, 21	mp2an 696	. . . 4 |- (C MH D <-> A.y e. CH (y (_ D -> ((y vH C) i^i D) (_ (y vH (C i^i D))))
23	14, 13	chincl 9371	. . . . 5 |- (C i^i B) e. CH
24	15, 13	chincl 9371	. . . . 5 |- (D i^i B) e. CH
25	23, 24	mdsl2 10240	. . . 4 |- ((C i^i B) MH (D i^i B) <-> A.x e. CH ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B)))))
26	20, 22, 25	3imtr4g 552	. . 3 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (C MH D -> (C i^i B) MH (D i^i B)))
27		chinclt 9410	. . . . . . . . . . 11 |- ((x e. CH /\ B e. CH) -> (x i^i B) e. CH)
28	13, 27	mpan2 695	. . . . . . . . . 10 |- (x e. CH -> (x i^i B) e. CH)
29		sseq1 2080	. . . . . . . . . . . 12 |- (y = (x i^i B) -> (y (_ (D i^i B) <-> (x i^i B) (_ (D i^i B)))
30		opreq1 3965	. . . . . . . . . . . . . 14 |- (y = (x i^i B) -> (y vH (C i^i B)) = ((x i^i B) vH (C i^i B)))
31	30	ineq1d 2214	. . . . . . . . . . . . 13 |- (y = (x i^i B) -> ((y vH (C i^i B)) i^i (D i^i B)) = (((x i^i B) vH (C i^i B)) i^i (D i^i B)))
32		opreq1 3965	. . . . . . . . . . . . 13 |- (y = (x i^i B) -> (y vH ((C i^i B) i^i (D i^i B))) = ((x i^i B) vH ((C i^i B) i^i (D i^i B))))
33	31, 32	sseq12d 2088	. . . . . . . . . . . 12 |- (y = (x i^i B) -> (((y vH (C i^i B)) i^i (D i^i B)) (_ (y vH ((C i^i B) i^i (D i^i B))) <-> (((x i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((x i^i B) vH ((C i^i B) i^i (D i^i B)))))
34	29, 33	imbi12d 625	. . . . . . . . . . 11 |- (y = (x i^i B) -> ((y (_ (D i^i B) -> ((y vH (C i^i B)) i^i (D i^i B)) (_ (y vH ((C i^i B) i^i (D i^i B)))) <-> ((x i^i B) (_ (D i^i B) -> (((x i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((x i^i B) vH ((C i^i B) i^i (D i^i B))))))
35	34	rcla4v 1871	. . . . . . . . . 10 |- ((x i^i B) e. CH -> (A.y e. CH (y (_ (D i^i B) -> ((y vH (C i^i B)) i^i (D i^i B)) (_ (y vH ((C i^i B) i^i (D i^i B)))) -> ((x i^i B) (_ (D i^i B) -> ((