Theorem mdslmd1lem3 10254

Description: Lemma for mdslmd1 10256.

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

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

Proof of Theorem mdslmd1lem3

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (x vH A) = (if(x e. CH, x, 0H) vH A))
2	1	sseq1d 2088	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> ((x vH A) (_ D <-> (if(x e. CH, x, 0H) vH A) (_ D))
3	1	opreq1d 3975	. . . . . . . 8 |- (x = if(x e. CH, x, 0H) -> ((x vH A) vH C) = ((if(x e. CH, x, 0H) vH A) vH C))
4	3	ineq1d 2216	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (((x vH A) vH C) i^i D) = (((if(x e. CH, x, 0H) vH A) vH C) i^i D))
5	1	opreq1d 3975	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> ((x vH A) vH (C i^i D)) = ((if(x e. CH, x, 0H) vH A) vH (C i^i D)))
6	4, 5	sseq12d 2090	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> ((((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D)) <-> (((if(x e. CH, x, 0H) vH A) vH C) i^i D) (_ ((if(x e. CH, x, 0H) vH A) vH (C i^i D))))
7	2, 6	imbi12d 626	. . . . 5 |- (x = if(x e. CH, x, 0H) -> (((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D))) <-> ((if(x e. CH, x, 0H) vH A) (_ D -> (((if(x e. CH, x, 0H) vH A) vH C) i^i D) (_ ((if(x e. CH, x, 0H) vH A) vH (C i^i D)))))
8		sseq2 2083	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (((C i^i B) i^i (D i^i B)) (_ x <-> ((C i^i B) i^i (D i^i B)) (_ if(x e. CH, x, 0H)))
9		sseq1 2082	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (x (_ (D i^i B) <-> if(x e. CH, x, 0H) (_ (D i^i B)))
10	8, 9	anbi12d 628	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) <-> (((C i^i B) i^i (D i^i B)) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ (D i^i B))))
11		opreq1 3968	. . . . . . . 8 |- (x = if(x e. CH, x, 0H) -> (x vH (C i^i B)) = (if(x e. CH, x, 0H) vH (C i^i B)))
12	11	ineq1d 2216	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> ((x vH (C i^i B)) i^i (D i^i B)) = ((if(x e. CH, x, 0H) vH (C i^i B)) i^i (D i^i B)))
13		opreq1 3968	. . . . . . 7 |- (x = if(x e. CH, x, 0H) -> (x vH ((C i^i B) i^i (D i^i B))) = (if(x e. CH, x, 0H) vH ((C i^i B) i^i (D i^i B))))
14	12, 13	sseq12d 2090	. . . . . 6 |- (x = if(x e. CH, x, 0H) -> (((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B))) <-> ((if(x e. CH, x, 0H) vH (C i^i B)) i^i (D i^i B)) (_ (if(x e. CH, x, 0H) vH ((C i^i B) i^i (D i^i B)))))
15	10, 14	imbi12d 626	. . . . 5 |- (x = if(x e. CH, x, 0H) -> (((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B)))) <-> ((((C i^i B) i^i (D i^i B)) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ (D i^i B)) -> ((if(x e. CH, x, 0H) vH (C i^i B)) i^i (D i^i B)) (_ (if(x e. CH, x, 0H) vH ((C i^i B) i^i (D i^i B))))))
16	7, 15	imbi12d 626	. . . 4 |- (x = if(x e. CH, x, 0H) -> ((((x vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B))))) <-> (((if(x e. CH, x, 0H) vH A) (_ D -> (((if(x e. CH, x, 0H) vH A) vH C) i^i D) (_ ((if(x e. CH, x, 0H) vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ (D i^i B)) -> ((if(x e. CH, x, 0H) vH (C i^i B)) i^i (D i^i B)) (_ (if(x e. CH, x, 0H) vH ((C i^i B) i^i (D i^i B)))))))
17	16	imbi2d 612	. . 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 vH A) (_ D -> (((x vH A) vH C) i^i D) (_ ((x vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ x /\ x (_ (D i^i B)) -> ((x vH (C i^i B)) i^i (D i^i B)) (_ (x vH ((C i^i B) i^i (D i^i B)))))) <-> (((A MH B /\ B MH* A) /\ ((A (_ C /\ A (_ D) /\ (C (_ (A vH B) /\ D (_ (A vH B)))) -> (((if(x e. CH, x, 0H) vH A) (_ D -> (((if(x e. CH, x, 0H) vH A) vH C) i^i D) (_ ((if(x e. CH, x, 0H) vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ (D i^i B)) -> ((if(x e. CH, x, 0H) vH (C i^i B)) i^i (D i^i B)) (_ (if(x e. CH, x, 0H) vH ((C i^i B) i^i (D i^i B))))))))
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 9127	. . . . 5 |- 0H e. CH
23	22	elimel 2394	. . . 4 |- if(x e. CH, x, 0H) e. CH
24	18, 19, 20, 21, 23	mdslmd1lem1 10252	. . 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) vH A) (_ D -> (((if(x e. CH, x, 0H) vH A) vH C) i^i D) (_ ((if(x e. CH, x, 0H) vH A) vH (C i^i D))) -> ((((C i^i B) i^i (D i^i B)) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ (D i^i B)) -> ((if(x e. CH, x, 0H) vH (C i^i B)) i^i (D i^i B)) (_ (if(x e. CH, x, 0H) vH ((C i^i B) i^i (D i^i B))))))
25	17, 24	dedth 2383