Metamath Proof Explorer

Theorem mdslmd1lem2

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
mdslmd1lem.5 
|- R e. CH
Assertion mdslmd1lem2 
|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( R i^i B ) C_ ( D i^i B ) -> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( ( R vH C ) i^i D ) C_ ( R 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 mdslmd1lem.5 
 |-  R e. CH
6 ssrin 
 |-  ( R C_ D -> ( R i^i B ) C_ ( D i^i B ) )
7 6 adantl 
 |-  ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( R i^i B ) C_ ( D i^i B ) )
8 7 imim1i 
 |-  ( ( ( R i^i B ) C_ ( D i^i B ) -> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
9 simpllr 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> B MH* A )
10 3 5 chub2i 
 |-  C C_ ( R vH C )
11 sstr 
 |-  ( ( A C_ C /\ C C_ ( R vH C ) ) -> A C_ ( R vH C ) )
12 10 11 mpan2 
 |-  ( A C_ C -> A C_ ( R vH C ) )
13 12 ad2antrr 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> A C_ ( R vH C ) )
14 13 ad2antlr 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ ( R vH C ) )
15 simplr 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> A C_ D )
16 15 ad2antlr 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ D )
17 14 16 ssind 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ ( ( R vH C ) i^i D ) )
18 ssin 
 |-  ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
19 3 4 chincli 
 |-  ( C i^i D ) e. CH
20 19 5 chub2i 
 |-  ( C i^i D ) C_ ( R vH ( C i^i D ) )
21 sstr 
 |-  ( ( A C_ ( C i^i D ) /\ ( C i^i D ) C_ ( R vH ( C i^i D ) ) ) -> A C_ ( R vH ( C i^i D ) ) )
22 20 21 mpan2 
 |-  ( A C_ ( C i^i D ) -> A C_ ( R vH ( C i^i D ) ) )
23 18 22 sylbi 
 |-  ( ( A C_ C /\ A C_ D ) -> A C_ ( R vH ( C i^i D ) ) )
24 23 adantr 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> A C_ ( R vH ( C i^i D ) ) )
25 24 ad2antlr 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ ( R vH ( C i^i D ) ) )
26 17 25 ssind 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ ( ( ( R vH C ) i^i D ) i^i ( R vH ( C i^i D ) ) ) )
27 inss2 
 |-  ( ( R vH C ) i^i D ) C_ D
28 sstr 
 |-  ( ( ( ( R vH C ) i^i D ) C_ D /\ D C_ ( A vH B ) ) -> ( ( R vH C ) i^i D ) C_ ( A vH B ) )
29 27 28 mpan 
 |-  ( D C_ ( A vH B ) -> ( ( R vH C ) i^i D ) C_ ( A vH B ) )
30 29 ad2antll 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( R vH C ) i^i D ) C_ ( A vH B ) )
31 30 ad2antlr 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( R vH C ) i^i D ) C_ ( A vH B ) )
32 sstr 
 |-  ( ( R C_ D /\ D C_ ( A vH B ) ) -> R C_ ( A vH B ) )
33 32 ancoms 
 |-  ( ( D C_ ( A vH B ) /\ R C_ D ) -> R C_ ( A vH B ) )
34 33 ad2ant2l 
 |-  ( ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> R C_ ( A vH B ) )
35 34 adantll 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> R C_ ( A vH B ) )
36 35 adantll 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> R C_ ( A vH B ) )
37 ssinss1 
 |-  ( C C_ ( A vH B ) -> ( C i^i D ) C_ ( A vH B ) )
38 37 ad2antrl 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( C i^i D ) C_ ( A vH B ) )
39 38 ad2antlr 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( C i^i D ) C_ ( A vH B ) )
40 36 39 jca 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( R C_ ( A vH B ) /\ ( C i^i D ) C_ ( A vH B ) ) )
41 1 2 chjcli 
 |-  ( A vH B ) e. CH
42 5 19 41 chlubi 
 |-  ( ( R C_ ( A vH B ) /\ ( C i^i D ) C_ ( A vH B ) ) <-> ( R vH ( C i^i D ) ) C_ ( A vH B ) )
43 40 42 sylib 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( R vH ( C i^i D ) ) C_ ( A vH B ) )
44 31 43 jca 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( R vH C ) i^i D ) C_ ( A vH B ) /\ ( R vH ( C i^i D ) ) C_ ( A vH B ) ) )
45 5 3 chjcli 
 |-  ( R vH C ) e. CH
46 45 4 chincli 
 |-  ( ( R vH C ) i^i D ) e. CH
47 5 19 chjcli 
 |-  ( R vH ( C i^i D ) ) e. CH
48 46 47 41 chlubi 
 |-  ( ( ( ( R vH C ) i^i D ) C_ ( A vH B ) /\ ( R vH ( C i^i D ) ) C_ ( A vH B ) ) <-> ( ( ( R vH C ) i^i D ) vH ( R vH ( C i^i D ) ) ) C_ ( A vH B ) )
49 44 48 sylib 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( R vH C ) i^i D ) vH ( R vH ( C i^i D ) ) ) C_ ( A vH B ) )
50 1 2 46 47 mdslle1i 
 |-  ( ( B MH* A /\ A C_ ( ( ( 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 ) ) ) C_ ( A vH B ) ) -> ( ( ( R vH C ) i^i D ) C_ ( R vH ( C i^i D ) ) <-> ( ( ( R vH C ) i^i D ) i^i B ) C_ ( ( R vH ( C i^i D ) ) i^i B ) ) )
51 9 26 49 50 syl3anc 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( R vH C ) i^i D ) C_ ( R vH ( C i^i D ) ) <-> ( ( ( R vH C ) i^i D ) i^i B ) C_ ( ( R vH ( C i^i D ) ) i^i B ) ) )
52 inindir 
 |-  ( ( ( R vH C ) i^i D ) i^i B ) = ( ( ( R vH C ) i^i B ) i^i ( D i^i B ) )
53 sstr 
 |-  ( ( A C_ ( C i^i D ) /\ ( C i^i D ) C_ R ) -> A C_ R )
54 18 53 sylanb 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C i^i D ) C_ R ) -> A C_ R )
55 54 ad2ant2r 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ R )
56 simplll 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ C )
57 55 56 ssind 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> A C_ ( R i^i C ) )
58 simplrl 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> C C_ ( A vH B ) )
59 35 58 jca 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( R C_ ( A vH B ) /\ C C_ ( A vH B ) ) )
60 5 3 41 chlubi 
 |-  ( ( R C_ ( A vH B ) /\ C C_ ( A vH B ) ) <-> ( R vH C ) C_ ( A vH B ) )
61 59 60 sylib 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( R vH C ) C_ ( A vH B ) )
62 57 61 jca 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( A C_ ( R i^i C ) /\ ( R vH C ) C_ ( A vH B ) ) )
63 1 2 5 3 mdslj1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( R i^i C ) /\ ( R vH C ) C_ ( A vH B ) ) ) -> ( ( R vH C ) i^i B ) = ( ( R i^i B ) vH ( C i^i B ) ) )
64 62 63 sylan2 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) ) -> ( ( R vH C ) i^i B ) = ( ( R i^i B ) vH ( C i^i B ) ) )
65 64 anassrs 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( R vH C ) i^i B ) = ( ( R i^i B ) vH ( C i^i B ) ) )
66 65 ineq1d 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( R 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 ) ) )
67 52 66 syl5req 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) = ( ( ( R vH C ) i^i D ) i^i B ) )
68 18 biimpi 
 |-  ( ( A C_ C /\ A C_ D ) -> A C_ ( C i^i D ) )
69 68 adantr 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C i^i D ) C_ R ) -> A C_ ( C i^i D ) )
70 54 69 ssind 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C i^i D ) C_ R ) -> A C_ ( R i^i ( C i^i D ) ) )
71 33 adantll 
 |-  ( ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ R C_ D ) -> R C_ ( A vH B ) )
72 37 ad2antrr 
 |-  ( ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ R C_ D ) -> ( C i^i D ) C_ ( A vH B ) )
73 71 72 jca 
 |-  ( ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ R C_ D ) -> ( R C_ ( A vH B ) /\ ( C i^i D ) C_ ( A vH B ) ) )
74 73 42 sylib 
 |-  ( ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ R C_ D ) -> ( R vH ( C i^i D ) ) C_ ( A vH B ) )
75 70 74 anim12i 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C i^i D ) C_ R ) /\ ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ R C_ D ) ) -> ( A C_ ( R i^i ( C i^i D ) ) /\ ( R vH ( C i^i D ) ) C_ ( A vH B ) ) )
76 75 an4s 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( A C_ ( R i^i ( C i^i D ) ) /\ ( R vH ( C i^i D ) ) C_ ( A vH B ) ) )
77 1 2 5 19 mdslj1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( R i^i ( C i^i D ) ) /\ ( R vH ( C i^i D ) ) C_ ( A vH B ) ) ) -> ( ( R vH ( C i^i D ) ) i^i B ) = ( ( R i^i B ) vH ( ( C i^i D ) i^i B ) ) )
78 76 77 sylan2 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) ) -> ( ( R vH ( C i^i D ) ) i^i B ) = ( ( R i^i B ) vH ( ( C i^i D ) i^i B ) ) )
79 78 anassrs 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( R vH ( C i^i D ) ) i^i B ) = ( ( R i^i B ) vH ( ( C i^i D ) i^i B ) ) )
80 inindir 
 |-  ( ( C i^i D ) i^i B ) = ( ( C i^i B ) i^i ( D i^i B ) )
81 80 a1i 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( C i^i D ) i^i B ) = ( ( C i^i B ) i^i ( D i^i B ) ) )
82 81 oveq2d 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( R i^i B ) vH ( ( C i^i D ) i^i B ) ) = ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) )
83 79 82 eqtr2d 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) = ( ( R vH ( C i^i D ) ) i^i B ) )
84 67 83 sseq12d 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) <-> ( ( ( R vH C ) i^i D ) i^i B ) C_ ( ( R vH ( C i^i D ) ) i^i B ) ) )
85 51 84 bitr4d 
 |-  ( ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) /\ ( ( C i^i D ) C_ R /\ R C_ D ) ) -> ( ( ( R vH C ) i^i D ) C_ ( R vH ( C i^i D ) ) <-> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) )
86 85 exbiri 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) -> ( ( R vH C ) i^i D ) C_ ( R vH ( C i^i D ) ) ) ) )
87 86 a2d 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( ( R vH C ) i^i D ) C_ ( R vH ( C i^i D ) ) ) ) )
88 8 87 syl5 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( R i^i B ) C_ ( D i^i B ) -> ( ( ( R i^i B ) vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( ( R i^i B ) vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) -> ( ( ( C i^i D ) C_ R /\ R C_ D ) -> ( ( R vH C ) i^i D ) C_ ( R vH ( C i^i D ) ) ) ) )