This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) )