Theorem mdslmd1lem2 10161

Description: Lemma for mdslmd1 10164.

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

Proof of Theorem mdslmd1lem2

Step	Hyp	Ref	Expression
1		mdslmd.1	. . . . . . . 8 |- A e. CH
2		mdslmd.2	. . . . . . . 8 |- B e. CH
3		mdslmd1lem.5	. . . . . . . . . 10 |- R e. CH
4		mdslmd.3	. . . . . . . . . 10 |- C e. CH
5	3, 4	chjcl 9295	. . . . . . . . 9 |- (R vH C) e. CH
6		mdslmd.4	. . . . . . . . 9 |- D e. CH
7	5, 6	chincl 9298	. . . . . . . 8 |- ((R vH C) i^i D) e. CH
8	4, 6	chincl 9298	. . . . . . . . 9 |- (C i^i D) e. CH
9	3, 8	chjcl 9295	. . . . . . . 8 |- (R vH (C i^i D)) e. CH
10	1, 2, 7, 9	mdslle1 10152	. . . . . . 7 |- ((B MH* A /\ A (_ (((R vH C) i^i D) i^i (R vH (C i^i D))) /\ (((R vH C) i^i D) vH (R vH (C i^i D))) (_ (A vH B)) -> (((R vH C) i^i D) (_ (R vH (C i^i D)) <-> (((R vH C) i^i D) i^i B) (_ ((R vH (C i^i D)) i^i B)))
11		pm3.27 323	. . . . . . . 8 |- ((A MH B /\ B MH* A) -> B MH* A)
12	11	ad2antrr 404	. . . . . . 7 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> B MH* A)
13	4, 3	chub2 9308	. . . . . . . . . . . . . 14 |- C (_ (R vH C)
14		sstr 2062	. . . . . . . . . . . . . 14 |- ((A (_ C /\ C (_ (R vH C)) -> A (_ (R vH C))
15	13, 14	mpan2 694	. . . . . . . . . . . . 13 |- (A (_ C -> A (_ (R vH C))
16	15	ad2antrr 404	. . . . . . . . . . . 12 |- (((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> A (_ (R vH C))
17	16	ad2antlr 405	. . . . . . . . . . 11 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> A (_ (R vH C))
18		simplr 413	. . . . . . . . . . . 12 |- (((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> A (_ D)
19	18	ad2antlr 405	. . . . . . . . . . 11 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> A (_ D)
20	17, 19	jca 288	. . . . . . . . . 10 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> (A (_ (R vH C) /\ A (_ D))
21		ssin 2222	. . . . . . . . . 10 |- ((A (_ (R vH C) /\ A (_ D) <-> A (_ ((R vH C) i^i D))
22	20, 21	sylib 198	. . . . . . . . 9 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> A (_ ((R vH C) i^i D))
23		ssin 2222	. . . . . . . . . . . 12 |- ((A (_ C /\ A (_ D) <-> A (_ (C i^i D))
24	8, 3	chub2 9308	. . . . . . . . . . . . 13 |- (C i^i D) (_ (R vH (C i^i D))
25		sstr 2062	. . . . . . . . . . . . 13 |- ((A (_ (C i^i D) /\ (C i^i D) (_ (R vH (C i^i D))) -> A (_ (R vH (C i^i D)))
26	24, 25	mpan2 694	. . . . . . . . . . . 12 |- (A (_ (C i^i D) -> A (_ (R vH (C i^i D)))
27	23, 26	sylbi 199	. . . . . . . . . . 11 |- ((A (_ C /\ A (_ D) -> A (_ (R vH (C i^i D)))
28	27	adantr 389	. . . . . . . . . 10 |- (((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> A (_ (R vH (C i^i D)))
29	28	ad2antlr 405	. . . . . . . . 9 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> A (_ (R vH (C i^i D)))
30	22, 29	jca 288	. . . . . . . 8 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> (A (_ ((R vH C) i^i D) /\ A (_ (R vH (C i^i D))))
31		ssin 2222	. . . . . . . 8 |- ((A (_ ((R vH C) i^i D) /\ A (_ (R vH (C i^i D))) <-> A (_ (((R vH C) i^i D) i^i (R vH (C i^i D))))
32	30, 31	sylib 198	. . . . . . 7 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> A (_ (((R vH C) i^i D) i^i (R vH (C i^i D))))
33		inss2 2221	. . . . . . . . . . . 12 |- ((R vH C) i^i D) (_ D
34		sstr 2062	. . . . . . . . . . . 12 |- ((((R vH C) i^i D) (_ D /\ D (_ (A vH B)) -> ((R vH C) i^i D) (_ (A vH B))
35	33, 34	mpan 693	. . . . . . . . . . 11 |- (D (_ (A vH B) -> ((R vH C) i^i D) (_ (A vH B))
36	35	ad2antll 407	. . . . . . . . . 10 |- (((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> ((R vH C) i^i D) (_ (A vH B))
37	36	ad2antlr 405	. . . . . . . . 9 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> ((R vH C) i^i D) (_ (A vH B))
38		sstr 2062	. . . . . . . . . . . . . . 15 |- ((R (_ D /\ D (_ (A vH B)) -> R (_ (A vH B))
39	38	ancoms 436	. . . . . . . . . . . . . 14 |- ((D (_ (A vH B) /\ R (_ D) -> R (_ (A vH B))
40	39	ad2ant2l 408	. . . . . . . . . . . . 13 |- (((C (_ (A vH B) /\ D (_ (A vH B)) /\ ((C i^i D) (_ R /\ R (_ D)) -> R (_ (A vH B))
41	40	adantll 392	. . . . . . . . . . . 12 |- ((((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) /\ ((C i^i D) (_ R /\ R (_ D)) -> R (_ (A vH B))
42	41	adantll 392	. . . . . . . . . . 11 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> R (_ (A vH B))
43		ssinss1 2227	. . . . . . . . . . . . 13 |- (C (_ (A vH B) -> (C i^i D) (_ (A vH B))
44	43	ad2antrl 406	. . . . . . . . . . . 12 |- (((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B))) -> (C i^i D) (_ (A vH B))
45	44	ad2antlr 405	. . . . . . . . . . 11 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> (C i^i D) (_ (A vH B))
46	42, 45	jca 288	. . . . . . . . . 10 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R (_ D)) -> (R (_ (A vH B) /\ (C i^i D) (_ (A vH B)))
47	1, 2	chjcl 9295	. . . . . . . . . . 11 |- (A vH B) e. CH
48	3, 8, 47	chlub 9309	. . . . . . . . . 10 |- ((R (_ (A vH B) /\ (C i^i D) (_ (A vH B)) <-> (R vH (C i^i D)) (_ (A vH B))
49	46, 48	sylib 198	. . . . . . . . 9 |- ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) /\ ((C i^i D) (_ R /\ R