Theorem mdslmd3 10254

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 9429	. . . . . . . . . . . 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 908	. . . . . . . . . 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 2237	. . . . . . . . 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 394	. . . . . . 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 394	. . . . . 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 391	. . . . 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 10217	. . . . . . . . . . . . . . . . 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 912	. . . . . . . . . . . . . . . 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 708	. . . . . . . . . . . . . . 15 |- ((x e. CH /\ (A MH B /\ x (_ B)) -> ((x vH A) i^i B) = (x vH (A i^i B)))
16	15	ineq1d 2219	. . . . . . . . . . . . . 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 2226	. . . . . . . . . . . . . 14 |- (((x vH A) i^i B) i^i C) = ((x vH A) i^i (B i^i C))
18	16, 17	syl5eqr 1524	. . . . . . . . . . . . 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 403	. . . . . . . . . . . 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 405	. . . . . . . . . . 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 9378	. . . . . . . . . . . . . . . 16 |- (A i^i B) e. CH
23		mdit 10217	. . . . . . . . . . . . . . . 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 912	. . . . . . . . . . . . . . 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 708	. . . . . . . . . . . . . 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 2226	. . . . . . . . . . . . . . 15 |- ((A i^i B) i^i C) = (A i^i (B i^i C))
27	26	opreq2i 3978	. . . . . . . . . . . . . 14 |- (x vH ((A i^i B) i^i C)) = (x vH (A i^i (B i^i C)))
28	25, 27	syl6eq 1526	. . . . . . . . . . . . 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 402	. . . . . . . . . . . 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 404	. . . . . . . . . . 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 1510	. . . . . . . . . 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 438	. . . . . . . . 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 491	. . . . . . . 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 2235	. . . . . . . 8 |- ((x (_ B /\ x (_ C) <-> x (_ (B i^i C))
35	33, 34	sylan2br 455	. . . . . . 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 399	. . . . . 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 2237	. . . . . . . . . . . 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 2226	. . . . . . . . . . . . 13 |- ((A i^i C) i^i (B i^i C)) = (A i^i (C i^i (B i^i C)))
39		in12 2227	. . . . . . . . . . . . . . 15 |- (C i^i (B i^i C)) = (B i^i (C i^i C))
40		inidm 2225	. . . . . . . . . . . . . . . 16 |- (C i^i C) = C
41	40	ineq2i 2217	. . . . . . . . . . . . . . 15 |- (B i^i (C i^i C)) = (B i^i C)
42	39, 41	eqtr 1498	. . . . . . . . . . . . . 14 |- (C i^i (B i^i C)) = (B i^i C)
43	42	ineq2i 2217	. . . . . . . . . . . . 13 |- (A i^i (C i^i (B i^i C))) = (A i^i (B i^i C))
44	38, 43	eqtr2 1499	. . . . . . . . . . . 12 |- (A i^i (B i^i C)) = ((A i^i C) i^i (B i^i C))
45	37, 44	syl5ss 2108	. . . . . . . . . . 11 |- ((A i^i C) (_ D -> (A i^i (B i^i C)) (_ (D i^i (B i^i C)))
46		ssrin 2237	. . . . . . . . . . 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 2080	. . . . . . . . . 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 3982	. . . . . . . 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 390	. . . . . . 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