Theorem mdslmd1lem1 10247

Description: Lemma for mdslmd1 10251.

Hypotheses

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

Assertion

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

Proof of Theorem mdslmd1lem1

Step	Hyp	Ref	Expression
1		mdslmd.1	. . . . . . . . . 10 |- A e. CH
2		mdslmd.2	. . . . . . . . . 10 |- B e. CH
3		mdslmd.4	. . . . . . . . . 10 |- D e. CH
4	1, 2, 3	3pm3.2i 820	. . . . . . . . 9 |- (A e. CH /\ B e. CH /\ D e. CH)
5		dmdsl3t 10237	. . . . . . . . 9 |- (((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)
6	4, 5	mpan 697	. . . . . . . 8 |- ((B MH* A /\ A (_ D /\ D (_ (A vH B)) -> ((D i^i B) vH A) = D)
7		pm3.27 323	. . . . . . . 8 |- ((A MH B /\ B MH* A) -> B MH* A)
8		pm3.27 323	. . . . . . . 8 |- ((A (_ C /\ A (_ D) -> A (_ D)
9		pm3.27 323	. . . . . . . 8 |- ((C (_ (A vH B) /\ D (_ (A vH B)) -> D (_ (A vH B))
10	6, 7, 8, 9	syl3an 870	. . . . . . 7 |- (((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)
11	10	3expb 836	. . . . . 6 |- (((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)
12	11	sseq2d 2092	. . . . 5 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> ((R vH A) (_ ((D i^i B) vH A) <-> (R vH A) (_ D))
13		mdslmd1lem.5	. . . . . 6 |- R e. CH
14	3, 2	chincl 9378	. . . . . 6 |- (D i^i B) e. CH
15	13, 14, 1	chlej1 9391	. . . . 5 |- (R (_ (D i^i B) -> (R vH A) (_ ((D i^i B) vH A))
16	12, 15	syl5bi 208	. . . 4 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (R (_ (D i^i B) -> (R vH A) (_ D))
17	16	adantld 392	. . 3 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> ((((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B)) -> (R vH A) (_ D))
18	17	imim1d 28	. 2 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (((R vH A) (_ D -> (((R vH A) vH C) i^i D) (_ ((R vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B)) -> (((R vH A) vH C) i^i D) (_ ((R vH A) vH (C i^i D)))))
19	13, 1	chjcl 9375	. . . . . . . . . . . 12 |- (R vH A) e. CH
20		mdslmd.3	. . . . . . . . . . . 12 |- C e. CH
21	1, 2, 19, 20	mdslj1 10241	. . . . . . . . . . 11 |- (((A MH B /\ B MH* A) /\ (A (_ ((R vH A) i^i C) /\ ((R vH A) vH C) (_ (A vH B))) -> (((R vH A) vH C) i^i B) = (((R vH A) i^i B) vH (C i^i B)))
22		simpll 414	. . . . . . . . . . 11 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> (A MH B /\ B MH* A))
23		simpll 414	. . . . . . . . . . . . . . 15 |- (((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> A (_ C)
24	23	ad2antlr 407	. . . . . . . . . . . . . 14 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> A (_ C)
25	1, 13	chub2 9388	. . . . . . . . . . . . . 14 |- A (_ (R vH A)
26	24, 25	jctil 292	. . . . . . . . . . . . 13 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> (A (_ (R vH A) /\ A (_ C))
27		ssin 2235	. . . . . . . . . . . . 13 |- ((A (_ (R vH A) /\ A (_ C) <-> A (_ ((R vH A) i^i C))
28	26, 27	sylib 198	. . . . . . . . . . . 12 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> A (_ ((R vH A) i^i C))
29		sstr 2075	. . . . . . . . . . . . . . . . . . . . 21 |- ((R (_ D /\ D (_ (A vH B)) -> R (_ (A vH B))
30		inss1 2233	. . . . . . . . . . . . . . . . . . . . . 22 |- (D i^i B) (_ D
31		sstr 2075	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R (_ (D i^i B) /\ (D i^i B) (_ D) -> R (_ D)
32	30, 31	mpan2 698	. . . . . . . . . . . . . . . . . . . . 21 |- (R (_ (D i^i B) -> R (_ D)
33	29, 32	sylan 450	. . . . . . . . . . . . . . . . . . . 20 |- ((R (_ (D i^i B) /\ D (_ (A vH B)) -> R (_ (A vH B))
34	33	ancoms 438	. . . . . . . . . . . . . . . . . . 19 |- ((D (_ (A vH B) /\ R (_ (D i^i B)) -> R (_ (A vH B))
35	34	adantll 394	. . . . . . . . . . . . . . . . . 18 |- (((C (_ (A vH B) /\ D (_ (A vH B)) /\ R (_ (D i^i B)) -> R (_ (A vH B))
36	35	adantll 394	. . . . . . . . . . . . . . . . 17 |- ((((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) /\ R (_ (D i^i B)) -> R (_ (A vH B))
37	36	ad2ant2l 410	. . . . . . . . . . . . . . . 16 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> R (_ (A vH B))
38	1, 2	chub1 9387	. . . . . . . . . . . . . . . 16 |- A (_ (A vH B)
39	37, 38	jctir 293	. . . . . . . . . . . . . . 15 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> (R (_ (A vH B) /\ A (_ (A vH B)))
40	1, 2	chjcl 9375	. . . . . . . . . . . . . . . 16 |- (A vH B) e. CH
41	13, 1, 40	chlub 9389	. . . . . . . . . . . . . . 15 |- ((R (_ (A vH B) /\ A (_ (A vH B)) <-> (R vH A) (_ (A vH B))
42	39, 41	sylib 198	. . . . . . . . . . . . . 14 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> (R vH A) (_ (A vH B))
43		pm3.26 319	. . . . . . . . . . . . . . . 16 |- ((C (_ (A vH B) /\ D (_ (A vH B)) -> C (_ (A vH B))
44	43	ad2antll 409	. . . . . . . . . . . . . . 15 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> C (_ (A vH B))
45	44	adantr 391	. . . . . . . . . . . . . 14 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B) i^i (D i^i B)) (_ R /\ R (_ (D i^i B))) -> C (_ (A vH B))
46	42, 45	jca 288	. . . . . . . . . . . . 13 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ (((C i^i B