Theorem mdslmd3 10259

Description: Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of [MaedaMaeda] p. 2.

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
mdslmd3	|- (((A MH B /\ (A i^i B) MH C) /\ ((A i^i C) (_ D /\ D (_ A)) -> D MH (B i^i C))

Proof of Theorem mdslmd3

Step	Hyp	Ref	Expression
1		mdslmd.4	. . . . . . . . . . 11 |- D e. CH
2		mdslmd.1	. . . . . . . . . . 11 |- A e. CH
3		chlej2t 9434	. . . . . . . . . . . 12 |- (((D e. CH /\ A e. CH /\ x e. CH) /\ D (_ A) -> (x vH D) (_ (x vH A))
4	3	ex 373	. . . . . . . . . . 11 |- ((D e. CH /\ A e. CH /\ x e. CH) -> (D (_ A -> (x vH D) (_ (x vH A)))
5	1, 2, 4	mp3an12 906	. . . . . . . . . 10 |- (x e. CH -> (D (_ A -> (x vH D) (_ (x vH A)))
6	5	impcom 351	. . . . . . . . 9 |- ((D (_ A /\ x e. CH) -> (x vH D) (_ (x vH A))
7		ssrin 2234	. . . . . . . . 9 |- ((x vH D) (_ (x vH A) -> ((x vH D) i^i (B i^i C)) (_ ((x vH A) i^i (B i^i C)))
8	6, 7	syl 10	. . . . . . . 8 |- ((D (_ A /\ x e. CH) -> ((x vH D) i^i (B i^i C)) (_ ((x vH A) i^i (B i^i C)))
9	8	adantll 392	. . . . . . 7 |- ((((A i^i C) (_ D /\ D (_ A) /\ x e. CH) -> ((x vH D) i^i (B i^i C)) (_ ((x vH A) i^i (B i^i C)))
10	9	adantll 392	. . . . . 6 |- ((((A MH B /\ (A i^i B) MH C) /\ ((A i^i C) (_ D /\ D (_ A)) /\ x e. CH) -> ((x vH D) i^i (B i^i C)) (_ ((x vH A) i^i (B i^i C)))
11	10	adantr 389	. . . . 5 |- (((((A MH B /\ (A i^i B) MH C) /\ ((A i^i C) (_ D /\ D (_ A)) /\ x e. CH) /\ x (_ (B i^i C)) -> ((x vH D) i^i (B i^i C)) (_ ((x vH A) i^i (B i^i C)))
12		mdslmd.2	. . . . . . . . . . . . . . . 16 |- B e. CH
13		mdit 10222	. . . . . . . . . . . . . . . . 17 |- (((A e. CH /\ B e. CH /\ x e. CH) /\ (A MH B /\ x (_ B)) -> ((x vH A) i^i B) = (x vH (A i^i B)))
14	2, 13	mp3anl1 910	. . . . . . . . . . . . . . . 16 |- (((B e. CH /\ x e. CH) /\ (A MH B /\ x (_ B)) -> ((x vH A) i^i B) = (x vH (A i^i B)))
15	12, 14	mpanl1 706	. . . . . . . . . . . . . . 15 |- ((x e. CH /\ (A MH B /\ x (_ B)) -> ((x vH A) i^i B) = (x vH (A i^i B)))
16	15	ineq1d 2216	. . . . . . . . . . . . . 14 |- ((x e. CH /\ (A MH B /\ x (_ B)) -> (((x vH A) i^i B) i^i C) = ((x vH (A i^i B)) i^i C))
17		inass 2223	. . . . . . . . . . . . . 14 |- (((x vH A) i^i B) i^i C) = ((x vH A) i^i (B i^i C))
18	16, 17	syl5eqr 1521	. . . . . . . . . . . . 13 |- ((x e. CH /\ (A MH B /\ x (_ B)) -> ((x vH A) i^i (B i^i C)) = ((x vH (A i^i B)) i^i C))
19	18	adantrlr 401	. . . . . . . . . . . 12 |- ((x e. CH /\ ((A MH B /\ (A i^i B) MH C) /\ x (_ B)) -> ((x vH A) i^i (B i^i C)) = ((x vH (A i^i B)) i^i C))
20	19	adantrrr 403	. . . . . . . . . . 11 |- ((x e. CH /\ ((A MH B /\ (A i^i B) MH C) /\ (x (_ B /\ x (_ C))) -> ((x vH A) i^i (B i^i C)) = ((x vH (A i^i B)) i^i C))
21		mdslmd.3	. . . . . . . . . . . . . . 15 |- C e. CH
22	2, 12	chincl 9383	. . . . . . . . . . . . . . . 16 |- (A i^i B) e. CH
23		mdit 10222	. . . . . . . . . . . . . . . 16 |- ((((A i^i B) e. CH /\ C e. CH /\ x e. CH) /\ ((A i^i B) MH C /\ x (_ C)) -> ((x vH (A i^i B)) i^i C) = (x vH ((A i^i B) i^i C)))
24	22, 23	mp3anl1 910	. . . . . . . . . . . . . . 15 |- (((C e. CH /\ x e. CH) /\ ((A i^i B) MH C /\ x (_ C)) -> ((x vH (A i^i B)) i^i C) = (x vH ((A i^i B) i^i C)))
25	21, 24	mpanl1 706	. . . . . . . . . . . . . 14 |- ((x e. CH /\ ((A i^i B) MH C /\ x (_ C)) -> ((x vH (A i^i B)) i^i C) = (x vH ((A i^i B) i^i C)))
26		inass 2223	. . . . . . . . . . . . . . 15 |- ((A i^i B) i^i C) = (A i^i (B i^i C))
27	26	opreq2i 3972	. . . . . . . . . . . . . 14 |- (x vH ((A i^i B) i^i C)) = (x vH (A i^i (B i^i C)))
28	25, 27	syl6eq 1523	. . . . . . . . . . . . 13 |- ((x e. CH /\ ((A i^i B) MH C /\ x (_ C)) -> ((x vH (A i^i B)) i^i C) = (x vH (A i^i (B i^i C))))
29	28	adantrll 400	. . . . . . . . . . . 12 |- ((x e. CH /\ ((A MH B /\ (A i^i B) MH C) /\ x (_ C)) -> ((x vH (A i^i B)) i^i C) = (x vH (A i^i (B i^i C))))
30	29	adantrrl 402	. . . . . . . . . . 11 |- ((x e. CH /\ ((A MH B /\ (A i^i B) MH C) /\ (x (_ B /\ x (_ C))) -> ((x vH (A i^i B)) i^i C) = (x vH (A i^i (B i^i C))))
31	20, 30	eqtrd 1507	. . . . . . . . . 10 |- ((x e. CH /\ ((A MH B /\ (A i^i B) MH C) /\ (x (_ B /\ x (_ C))) -> ((x vH A) i^i (B i^i C)) = (x vH (A i^i (B i^i C))))
32	31	ancoms 436	. . . . . . . . 9 |- ((((A MH B /\ (A i^i B) MH C) /\ (x (_ B /\ x (_ C)) /\ x e. CH) -> ((x vH A) i^i (B i^i C)) = (x vH (A i^i (B i^i C))))
33	32	an1rs 489	. . . . . . . 8 |- ((((A MH B /\ (A i^i B) MH C) /\ x e. CH) /\ (x (_ B /\ x (_ C)) -> ((x vH A) i^i (B i^i C)) = (x vH (A i^i (B i^i C))))
34		ssin 2232	. . . . . . . 8 |- ((x (_ B /\ x (_ C) <-> x (_ (B i^i C))
35	33, 34	sylan2br 453	. . . . . . 7 |- ((((A MH B /\ (A i^i B) MH C) /\ x e. CH) /\ x (_ (B i^i C)) -> ((x vH A) i^i (B i^i C)) = (x vH (A i^i (B i^i C))))
36	35	adantllr 397	. . . . . 6 |- (((((A MH B /\ (A i^i B) MH C) /\ ((A i^i C) (_ D /\ D (_ A)) /\ x e. CH) /\ x (_ (B i^i C)) -> ((x vH A) i^i (B i^i C)) = (x vH (A i^i (B i^i C))))
37		ssrin 2234	. . . . . . . . . . . 12 |- ((A i^i C) (_ D -> ((A i^i C) i^i (B i^i C)) (_ (D i^i (B i^i C)))
38		inass 2223	. . . . . . . . . . . . 13 |- ((A i^i C) i^i (B i^i C)) = (A i^i (C i^i (B i^i C)))
39		in12 2224	. . . . . . . . . . . . . . 15 |- (C i^i (B i^i C)) = (B i^i (C i^i C))
40		inidm 2222	. . . . . . . . . . . . . . . 16 |- (C i^i C) = C
41	40	ineq2i 2214	. . . . . . . . . . . . . . 15 |- (B i^i (C i^i C)) = (B i^i C)
42	39, 41	eqtr 1495	. . . . . . . . . . . . . 14 |- (C i^i (B i^i C)) = (B i^i C)
43	42	ineq2i 2214	. . . . . . . . . . . . 13 |- (A i^i (C i^i (B i^i C))) = (A i^i (B i^i C))
44	38, 43	eqtr2 1496	. . . . . . . . . . . 12 |- (A i^i (B i^i C)) = ((A i^i C) i^i (B i^i C))
45	37, 44	syl5ss 2105	. . . . . . . . . . 11 |- ((A i^i C) (_ D -> (A i^i (B i^i C)) (_ (D i^i (B i^i C)))
46		ssrin 2234	. . . . . . . . . . 11 |- (D (_ A -> (D i^i (B i^i C)) (_ (A i^i (B i^i C)))
47	45, 46	anim12i 333	. . . . . . . . . 10 |- (((A i^i C) (_ D /\ D (_ A) -> ((A i^i (B i^i C)) (_ (D i^i (B i^i C)) /\ (D i^i (B i^i C)) (_ (A i^i (B i^i C))))
48		eqss 2077	. . . . . . . . . 10 |- ((A i^i (B i^i C)) = (D i^i (B i^i C)) <-> ((A i^i (B i^i C)) (_ (D i^i (B i^i C)) /\ (D i^i (B i^i C)) (_ (A i^i (B i^i C))))
49	47, 48	sylibr 200	. . . . . . . . 9 |- (((A i^i C) (_ D /\ D (_ A) -> (A i^i (B i^i C)) = (D i^i (B i^i C)))
50	49	opreq2d 3976	. . . . . . . 8 |- (((A i^i C) (_ D /\ D (_ A) -> (x vH (A i^i (B i^i C))) = (x vH (D i^i (B i^i C))))
51	50	adantl 388	. . . . . . 7 |- (((A MH B /\ (A i^i B) MH C) /\ ((A i^i C) (_ D /\ D (_ A)) -> (x vH (A i^i (B i^i C))) = (x vH (D