Metamath Proof Explorer

Theorem mdslmd1lem1

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 mdslmd1lem1 
|- ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( R vH A ) C_ D -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )

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 4 2 chincli 
 |-  ( D i^i B ) e. CH
7 5 6 1 chlej1i 
 |-  ( R C_ ( D i^i B ) -> ( R vH A ) C_ ( ( D i^i B ) vH A ) )
8 simpr 
 |-  ( ( A MH B /\ B MH* A ) -> B MH* A )
9 simpr 
 |-  ( ( A C_ C /\ A C_ D ) -> A C_ D )
10 simpr 
 |-  ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) -> D C_ ( A vH B ) )
11 1 2 4 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ D e. CH )
12 dmdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ D e. CH ) /\ ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
13 11 12 mpan 
 |-  ( ( B MH* A /\ A C_ D /\ D C_ ( A vH B ) ) -> ( ( D i^i B ) vH A ) = D )
14 8 9 10 13 syl3an 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( D i^i B ) vH A ) = D )
15 14 3expb 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( D i^i B ) vH A ) = D )
16 15 sseq2d 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( R vH A ) C_ ( ( D i^i B ) vH A ) <-> ( R vH A ) C_ D ) )
17 7 16 imbitrid 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( R C_ ( D i^i B ) -> ( R vH A ) C_ D ) )
18 17 adantld 
 |-  ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( R vH A ) C_ D ) )
19 18 imim1d 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( R vH A ) C_ D -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) ) ) )
20 simpll 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A MH B /\ B MH* A ) )
21 simpll 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> A C_ C )
22 21 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ C )
23 1 5 chub2i 
 |-  A C_ ( R vH A )
24 22 23 jctil 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A C_ ( R vH A ) /\ A C_ C ) )
25 ssin 
 |-  ( ( A C_ ( R vH A ) /\ A C_ C ) <-> A C_ ( ( R vH A ) i^i C ) )
26 24 25 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ ( ( R vH A ) i^i C ) )
27 inss1 
 |-  ( D i^i B ) C_ D
28 sstr 
 |-  ( ( R C_ ( D i^i B ) /\ ( D i^i B ) C_ D ) -> R C_ D )
29 27 28 mpan2 
 |-  ( R C_ ( D i^i B ) -> R C_ D )
30 sstr 
 |-  ( ( R C_ D /\ D C_ ( A vH B ) ) -> R C_ ( A vH B ) )
31 29 30 sylan 
 |-  ( ( R C_ ( D i^i B ) /\ D C_ ( A vH B ) ) -> R C_ ( A vH B ) )
32 31 ancoms 
 |-  ( ( D C_ ( A vH B ) /\ R C_ ( D i^i B ) ) -> R C_ ( A vH B ) )
33 32 adantll 
 |-  ( ( ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) /\ R C_ ( D i^i B ) ) -> R C_ ( A vH B ) )
34 33 adantll 
 |-  ( ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) /\ R C_ ( D i^i B ) ) -> R C_ ( A vH B ) )
35 34 ad2ant2l 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> R C_ ( A vH B ) )
36 1 2 chub1i 
 |-  A C_ ( A vH B )
37 35 36 jctir 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( R C_ ( A vH B ) /\ A C_ ( A vH B ) ) )
38 1 2 chjcli 
 |-  ( A vH B ) e. CH
39 5 1 38 chlubi 
 |-  ( ( R C_ ( A vH B ) /\ A C_ ( A vH B ) ) <-> ( R vH A ) C_ ( A vH B ) )
40 37 39 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( R vH A ) C_ ( A vH B ) )
41 simprrl 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> C C_ ( A vH B ) )
42 41 adantr 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> C C_ ( A vH B ) )
43 40 42 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH A ) C_ ( A vH B ) /\ C C_ ( A vH B ) ) )
44 5 1 chjcli 
 |-  ( R vH A ) e. CH
45 44 3 38 chlubi 
 |-  ( ( ( R vH A ) C_ ( A vH B ) /\ C C_ ( A vH B ) ) <-> ( ( R vH A ) vH C ) C_ ( A vH B ) )
46 43 45 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH A ) vH C ) C_ ( A vH B ) )
47 1 2 44 3 mdslj1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( ( R vH A ) i^i C ) /\ ( ( R vH A ) vH C ) C_ ( A vH B ) ) ) -> ( ( ( R vH A ) vH C ) i^i B ) = ( ( ( R vH A ) i^i B ) vH ( C i^i B ) ) )
48 20 26 46 47 syl12anc 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH A ) vH C ) i^i B ) = ( ( ( R vH A ) i^i B ) vH ( C i^i B ) ) )
49 simplll 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A MH B )
50 simplrl 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A C_ C /\ A C_ D ) )
51 ssin 
 |-  ( ( A C_ C /\ A C_ D ) <-> A C_ ( C i^i D ) )
52 50 51 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ ( C i^i D ) )
53 52 ssrind 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A i^i B ) C_ ( ( C i^i D ) i^i B ) )
54 inindir 
 |-  ( ( C i^i D ) i^i B ) = ( ( C i^i B ) i^i ( D i^i B ) )
55 53 54 sseqtrdi 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A i^i B ) C_ ( ( C i^i B ) i^i ( D i^i B ) ) )
56 simprl 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( C i^i B ) i^i ( D i^i B ) ) C_ R )
57 55 56 sstrd 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A i^i B ) C_ R )
58 inss2 
 |-  ( D i^i B ) C_ B
59 sstr 
 |-  ( ( R C_ ( D i^i B ) /\ ( D i^i B ) C_ B ) -> R C_ B )
60 58 59 mpan2 
 |-  ( R C_ ( D i^i B ) -> R C_ B )
61 60 ad2antll 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> R C_ B )
62 1 2 5 3pm3.2i 
 |-  ( A e. CH /\ B e. CH /\ R e. CH )
63 mdsl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ R e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ R /\ R C_ B ) ) -> ( ( R vH A ) i^i B ) = R )
64 62 63 mpan 
 |-  ( ( A MH B /\ ( A i^i B ) C_ R /\ R C_ B ) -> ( ( R vH A ) i^i B ) = R )
65 49 57 61 64 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH A ) i^i B ) = R )
66 65 oveq1d 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH A ) i^i B ) vH ( C i^i B ) ) = ( R vH ( C i^i B ) ) )
67 48 66 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( R vH ( C i^i B ) ) = ( ( ( R vH A ) vH C ) i^i B ) )
68 67 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) = ( ( ( ( R vH A ) vH C ) i^i B ) i^i ( D i^i B ) ) )
69 inindir 
 |-  ( ( ( ( R vH A ) vH C ) i^i D ) i^i B ) = ( ( ( ( R vH A ) vH C ) i^i B ) i^i ( D i^i B ) )
70 68 69 eqtr4di 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) = ( ( ( ( R vH A ) vH C ) i^i D ) i^i B ) )
71 52 23 jctil 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A C_ ( R vH A ) /\ A C_ ( C i^i D ) ) )
72 ssin 
 |-  ( ( A C_ ( R vH A ) /\ A C_ ( C i^i D ) ) <-> A C_ ( ( R vH A ) i^i ( C i^i D ) ) )
73 71 72 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ ( ( R vH A ) i^i ( C i^i D ) ) )
74 ssinss1 
 |-  ( C C_ ( A vH B ) -> ( C i^i D ) C_ ( A vH B ) )
75 74 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 ) )
76 75 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( C i^i D ) C_ ( A vH B ) )
77 40 76 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH A ) C_ ( A vH B ) /\ ( C i^i D ) C_ ( A vH B ) ) )
78 3 4 chincli 
 |-  ( C i^i D ) e. CH
79 44 78 38 chlubi 
 |-  ( ( ( R vH A ) C_ ( A vH B ) /\ ( C i^i D ) C_ ( A vH B ) ) <-> ( ( R vH A ) vH ( C i^i D ) ) C_ ( A vH B ) )
80 77 79 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( R vH A ) vH ( C i^i D ) ) C_ ( A vH B ) )
81 1 2 44 78 mdslj1i 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( A C_ ( ( R vH A ) i^i ( C i^i D ) ) /\ ( ( R vH A ) vH ( C i^i D ) ) C_ ( A vH B ) ) ) -> ( ( ( R vH A ) vH ( C i^i D ) ) i^i B ) = ( ( ( R vH A ) i^i B ) vH ( ( C i^i D ) i^i B ) ) )
82 20 73 80 81 syl12anc 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH A ) vH ( C i^i D ) ) i^i B ) = ( ( ( R vH A ) i^i B ) vH ( ( C i^i D ) i^i B ) ) )
83 54 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( C i^i D ) i^i B ) = ( ( C i^i B ) i^i ( D i^i B ) ) )
84 65 83 oveq12d 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH A ) i^i B ) vH ( ( C i^i D ) i^i B ) ) = ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) )
85 82 84 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) = ( ( ( R vH A ) vH ( C i^i D ) ) i^i B ) )
86 70 85 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) <-> ( ( ( ( R vH A ) vH C ) i^i D ) i^i B ) C_ ( ( ( R vH A ) vH ( C i^i D ) ) i^i B ) ) )
87 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> B MH* A )
88 simplr 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> A C_ D )
89 88 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ D )
90 44 3 chub1i 
 |-  ( R vH A ) C_ ( ( R vH A ) vH C )
91 23 90 sstri 
 |-  A C_ ( ( R vH A ) vH C )
92 89 91 jctil 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A C_ ( ( R vH A ) vH C ) /\ A C_ D ) )
93 ssin 
 |-  ( ( A C_ ( ( R vH A ) vH C ) /\ A C_ D ) <-> A C_ ( ( ( R vH A ) vH C ) i^i D ) )
94 92 93 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ ( ( ( R vH A ) vH C ) i^i D ) )
95 44 78 chub1i 
 |-  ( R vH A ) C_ ( ( R vH A ) vH ( C i^i D ) )
96 23 95 sstri 
 |-  A C_ ( ( R vH A ) vH ( C i^i D ) )
97 94 96 jctir 
 |-  ( ( ( ( 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( A C_ ( ( ( R vH A ) vH C ) i^i D ) /\ A C_ ( ( R vH A ) vH ( C i^i D ) ) ) )
98 ssin 
 |-  ( ( A C_ ( ( ( R vH A ) vH C ) i^i D ) /\ A C_ ( ( R vH A ) vH ( C i^i D ) ) ) <-> A C_ ( ( ( ( R vH A ) vH C ) i^i D ) i^i ( ( R vH A ) vH ( C i^i D ) ) ) )
99 97 98 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> A C_ ( ( ( ( R vH A ) vH C ) i^i D ) i^i ( ( R vH A ) vH ( C i^i D ) ) ) )
100 inss2 
 |-  ( ( ( R vH A ) vH C ) i^i D ) C_ D
101 sstr 
 |-  ( ( ( ( ( R vH A ) vH C ) i^i D ) C_ D /\ D C_ ( A vH B ) ) -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( A vH B ) )
102 100 101 mpan 
 |-  ( D C_ ( A vH B ) -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( A vH B ) )
103 102 ad2antll 
 |-  ( ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( A vH B ) )
104 103 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( A vH B ) )
105 104 80 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( ( R vH A ) vH C ) i^i D ) C_ ( A vH B ) /\ ( ( R vH A ) vH ( C i^i D ) ) C_ ( A vH B ) ) )
106 44 3 chjcli 
 |-  ( ( R vH A ) vH C ) e. CH
107 106 4 chincli 
 |-  ( ( ( R vH A ) vH C ) i^i D ) e. CH
108 44 78 chjcli 
 |-  ( ( R vH A ) vH ( C i^i D ) ) e. CH
109 107 108 38 chlubi 
 |-  ( ( ( ( ( R vH A ) vH C ) i^i D ) C_ ( A vH B ) /\ ( ( R vH A ) vH ( C i^i D ) ) C_ ( A vH B ) ) <-> ( ( ( ( R vH A ) vH C ) i^i D ) vH ( ( R vH A ) vH ( C i^i D ) ) ) C_ ( A vH B ) )
110 105 109 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( ( R vH A ) vH C ) i^i D ) vH ( ( R vH A ) vH ( C i^i D ) ) ) C_ ( A vH B ) )
111 1 2 107 108 mdslle1i 
 |-  ( ( B MH* A /\ A C_ ( ( ( ( R vH A ) vH C ) i^i D ) i^i ( ( R vH A ) vH ( C i^i D ) ) ) /\ ( ( ( ( R vH A ) vH C ) i^i D ) vH ( ( R vH A ) vH ( C i^i D ) ) ) C_ ( A vH B ) ) -> ( ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) <-> ( ( ( ( R vH A ) vH C ) i^i D ) i^i B ) C_ ( ( ( R vH A ) vH ( C i^i D ) ) i^i B ) ) )
112 87 99 110 111 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) <-> ( ( ( ( R vH A ) vH C ) i^i D ) i^i B ) C_ ( ( ( R vH A ) vH ( C i^i D ) ) i^i B ) ) )
113 86 112 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) ) -> ( ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) <-> ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) ) )
114 113 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) -> ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
115 114 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 B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )
116 19 115 syld 
 |-  ( ( ( A MH B /\ B MH* A ) /\ ( ( A C_ C /\ A C_ D ) /\ ( C C_ ( A vH B ) /\ D C_ ( A vH B ) ) ) ) -> ( ( ( R vH A ) C_ D -> ( ( ( R vH A ) vH C ) i^i D ) C_ ( ( R vH A ) vH ( C i^i D ) ) ) -> ( ( ( ( C i^i B ) i^i ( D i^i B ) ) C_ R /\ R C_ ( D i^i B ) ) -> ( ( R vH ( C i^i B ) ) i^i ( D i^i B ) ) C_ ( R vH ( ( C i^i B ) i^i ( D i^i B ) ) ) ) ) )