Theorem mdslmd1lem4

Description: Lemma for mdslmd1i . (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslmd.1	|- A e. CH
	mdslmd.2	|- B e. CH
	mdslmd.3	|- C e. CH
	mdslmd.4	|- D e. CH
Assertion	mdslmd1lem4	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	|- A e. CH
2		mdslmd.2	|- B e. CH
3		mdslmd.3	|- C e. CH
4		mdslmd.4	|- D e. CH
5		ineq1	|- ( x = if ( x e. CH , x , 0H ) -> ( x i^i B ) = ( if ( x e. CH , x , 0H ) i^i B ) )
6	5	sseq1d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( x i^i B ) C_ ( D i^i B ) <-> ( if ( x e. CH , x , 0H ) i^i B ) C_ ( D i^i B ) ) )
7	5	oveq1d	|- ( 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 ) ) )
8	7	ineq1d	|- ( 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 ) ) )
9	5	oveq1d	|- ( 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 ) ) ) )
10	8 9	sseq12d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( 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 ) ) C_ ( ( if ( x e. CH , x , 0H ) i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
11	6 10	imbi12d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) <-> ( ( if ( x e. CH , x , 0H ) i^i B ) C_ ( 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_ ( ( if ( x e. CH , x , 0H ) i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
12		sseq2	|- ( x = if ( x e. CH , x , 0H ) -> ( ( C i^i D ) C_ x <-> ( C i^i D ) C_ if ( x e. CH , x , 0H ) ) )
13		sseq1	|- ( x = if ( x e. CH , x , 0H ) -> ( x C_ D <-> if ( x e. CH , x , 0H ) C_ D ) )
14	12 13	anbi12d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) <-> ( ( C i^i D ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ D ) ) )
15		oveq1	|- ( x = if ( x e. CH , x , 0H ) -> ( x vH C ) = ( if ( x e. CH , x , 0H ) vH C ) )
16	15	ineq1d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( x vH C ) i^i D ) = ( ( if ( x e. CH , x , 0H ) vH C ) i^i D ) )
17		oveq1	|- ( x = if ( x e. CH , x , 0H ) -> ( x vH ( C i^i D ) ) = ( if ( x e. CH , x , 0H ) vH ( C i^i D ) ) )
18	16 17	sseq12d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) <-> ( ( if ( x e. CH , x , 0H ) vH C ) i^i D ) C_ ( if ( x e. CH , x , 0H ) vH ( C i^i D ) ) ) )
19	14 18	imbi12d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) <-> ( ( ( C i^i D ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ D ) -> ( ( if ( x e. CH , x , 0H ) vH C ) i^i D ) C_ ( if ( x e. CH , x , 0H ) vH ( C i^i D ) ) ) ) )
20	11 19	imbi12d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) <-> ( ( ( if ( x e. CH , x , 0H ) i^i B ) C_ ( 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_ ( ( if ( x e. CH , x , 0H ) i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ D ) -> ( ( if ( x e. CH , x , 0H ) vH C ) i^i D ) C_ ( if ( x e. CH , x , 0H ) vH ( C i^i D ) ) ) ) ) )
21	20	imbi2d	|- ( x = if ( x e. CH , x , 0H ) -> ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) ) <-> ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( if ( x e. CH , x , 0H ) i^i B ) C_ ( 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_ ( ( if ( x e. CH , x , 0H ) i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ D ) -> ( ( if ( x e. CH , x , 0H ) vH C ) i^i D ) C_ ( if ( x e. CH , x , 0H ) vH ( C i^i D ) ) ) ) ) ) )
22		h0elch	|- 0H e. CH
23	22	elimel	|- if ( x e. CH , x , 0H ) e. CH
24	1 2 3 4 23	mdslmd1lem2	|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( if ( x e. CH , x , 0H ) i^i B ) C_ ( 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_ ( ( if ( x e. CH , x , 0H ) i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ D ) -> ( ( if ( x e. CH , x , 0H ) vH C ) i^i D ) C_ ( if ( x e. CH , x , 0H ) vH ( C i^i D ) ) ) ) )
25	21 24	dedth	|- ( x e. CH -> ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) ) )
26	25	imp	|- ( ( x e. CH /\ ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) ) -> ( ( ( x i^i B ) C_ ( D i^i B ) -> ( ( ( x i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( x i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ x /\ x C_ D ) -> ( ( x vH C ) i^i D ) C_ ( x vH ( C i^i D ) ) ) ) )