Theorem mdslmd1lem4 10246

Description: Lemma for mdslmd1 10247.

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
mdslmd1lem4	|- ((x e. CH /\ ((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH 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)))) -> (((C i^i D) (_ x /\ x (_ D) -> ((x vH C) i^i D) (_ (x vH (C i^i D)))))

Distinct variable groups:   x,A   x,B   x,C   x,D

Proof of Theorem mdslmd1lem4

Step	Hyp	Ref	Expression
1		ineq1 2208	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (x i^i B) = (if(x e. CH, x, 0H) i^i B))
2	1	sseq1d 2086	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> ((x i^i B) (_ (D i^i B) <-> (if(x e. CH, x, 0H) i^i B) (_ (D i^i B)))
3	1	opreq1d 3972	. . . . . . . 8 |- (x = if(x e. CH, x, 0H) -> ((x i^i B) vH (C i^i B)) = ((if(x e. CH, x, 0H) i^i B) vH (C i^i B)))
4	3	ineq1d 2214	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (((x i^i B) vH (C i^i B)) i^i (D i^i B)) = (((if(x e. CH, x, 0H) i^i B) vH (C i^i B)) i^i (D i^i B)))
5	1	opreq1d 3972	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> ((x i^i B) vH ((C i^i B) i^i (D i^i B))) = ((if(x e. CH, x, 0H) i^i B) vH ((C i^i B) i^i (D i^i B))))
6	4, 5	sseq12d 2088	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> ((((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))) <-> (((if(x e. CH, x, 0H) i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((if(x e. CH, x, 0H) i^i B) vH ((C i^i B) i^i (D i^i B)))))
7	2, 6	imbi12d 625	. . . . 5 |- (x = if(x e. CH, x, 0H) -> (((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)))) <-> ((if(x e. CH, x, 0H) i^i B) (_ (D i^i B) -> (((if(x e. CH, x, 0H) i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((if(x e. CH, x, 0H) i^i B) vH ((C i^i B) i^i (D i^i B))))))
8		sseq2 2081	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> ((C i^i D) (_ x <-> (C i^i D) (_ if(x e. CH, x, 0H)))
9		sseq1 2080	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (x (_ D <-> if(x e. CH, x, 0H) (_ D))
10	8, 9	anbi12d 627	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> (((C i^i D) (_ x /\ x (_ D) <-> ((C i^i D) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ D)))
11		opreq1 3965	. . . . . . . 8 |- (x = if(x e. CH, x, 0H) -> (x vH C) = (if(x e. CH, x, 0H) vH C))
12	11	ineq1d 2214	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> ((x vH C) i^i D) = ((if(x e. CH, x, 0H) vH C) i^i D))
13		opreq1 3965	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (x vH (C i^i D)) = (if(x e. CH, x, 0H) vH (C i^i D)))
14	12, 13	sseq12d 2088	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> (((x vH C) i^i D) (_ (x vH (C i^i D)) <-> ((if(x e. CH, x, 0H) vH C) i^i D) (_ (if(x e. CH, x, 0H) vH (C i^i D))))
15	10, 14	imbi12d 625	. . . . 5 |- (x = if(x e. CH, x, 0H) -> ((((C i^i D) (_ x /\ x (_ D) -> ((x vH C) i^i D) (_ (x vH (C i^i D))) <-> (((C i^i D) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ D) -> ((if(x e. CH, x, 0H) vH C) i^i D) (_ (if(x e. CH, x, 0H) vH (C i^i D)))))
16	7, 15	imbi12d 625	. . . 4 |- (x = if(x e. CH, x, 0H) -> ((((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)))) -> (((C i^i D) (_ x /\ x (_ D) -> ((x vH C) i^i D) (_ (x vH (C i^i D)))) <-> (((if(x e. CH, x, 0H) i^i B) (_ (D i^i B) -> (((if(x e. CH, x, 0H) i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((if(x e. CH, x, 0H) i^i B) vH ((C i^i B) i^i (D i^i B)))) -> (((C i^i D) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ D) -> ((if(x e. CH, x, 0H) vH C) i^i D) (_ (if(x e. CH, x, 0H) vH (C i^i D))))))
17	16	imbi2d 611	. . 3 |- (x = if(x e. CH, x, 0H) -> ((((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH 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)))) -> (((C i^i D) (_ x /\ x (_ D) -> ((x vH C) i^i D) (_ (x vH (C i^i D))))) <-> (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (((if(x e. CH, x, 0H) i^i B) (_ (D i^i B) -> (((if(x e. CH, x, 0H) i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((if(x e. CH, x, 0H) i^i B) vH ((C i^i B) i^i (D i^i B)))) -> (((C i^i D) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ D) -> ((if(x e. CH, x, 0H) vH C) i^i D) (_ (if(x e. CH, x, 0H) vH (C i^i D)))))))
18		mdslmd.1	. . . 4 |- A e. CH
19		mdslmd.2	. . . 4 |- B e. CH
20		mdslmd.3	. . . 4 |- C e. CH
21		mdslmd.4	. . . 4 |- D e. CH
22		h0elch 9115	. . . . 5 |- 0H e. CH
23	22	elimel 2392	. . . 4 |- if(x e. CH, x, 0H) e. CH
24	18, 19, 20, 21, 23	mdslmd1lem2 10244	. . 3 |- (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (((if(x e. CH, x, 0H) i^i B) (_ (D i^i B) -> (((if(x e. CH, x, 0H) i^i B) vH (C i^i B)) i^i (D i^i B)) (_ ((if(x e. CH, x, 0H) i^i B) vH ((C i^i B) i^i (D i^i B)))) -> (((C i^i D) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ D) -> ((if(x e. CH, x, 0H) vH C) i^i D) (_ (if(x e. CH, x, 0H) vH (C i^i D)))))
25	17, 24	dedth 2381	. 2 |- (x e. CH -> (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH 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