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 |
|
chlej2 |
|- ( ( ( D e. CH /\ A e. CH /\ x e. CH ) /\ D C_ A ) -> ( x vH D ) C_ ( x vH A ) ) |
6 |
5
|
ex |
|- ( ( D e. CH /\ A e. CH /\ x e. CH ) -> ( D C_ A -> ( x vH D ) C_ ( x vH A ) ) ) |
7 |
4 1 6
|
mp3an12 |
|- ( x e. CH -> ( D C_ A -> ( x vH D ) C_ ( x vH A ) ) ) |
8 |
7
|
impcom |
|- ( ( D C_ A /\ x e. CH ) -> ( x vH D ) C_ ( x vH A ) ) |
9 |
8
|
ssrind |
|- ( ( D C_ A /\ x e. CH ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) ) |
10 |
9
|
adantll |
|- ( ( ( ( A i^i C ) C_ D /\ D C_ A ) /\ x e. CH ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) ) |
11 |
10
|
adantll |
|- ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) ) |
12 |
11
|
adantr |
|- ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( ( x vH A ) i^i ( B i^i C ) ) ) |
13 |
|
ssin |
|- ( ( x C_ B /\ x C_ C ) <-> x C_ ( B i^i C ) ) |
14 |
|
inass |
|- ( ( ( x vH A ) i^i B ) i^i C ) = ( ( x vH A ) i^i ( B i^i C ) ) |
15 |
|
mdi |
|- ( ( ( A e. CH /\ B e. CH /\ x e. CH ) /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) |
16 |
1 15
|
mp3anl1 |
|- ( ( ( B e. CH /\ x e. CH ) /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) |
17 |
2 16
|
mpanl1 |
|- ( ( x e. CH /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) |
18 |
17
|
ineq1d |
|- ( ( x e. CH /\ ( A MH B /\ x C_ B ) ) -> ( ( ( x vH A ) i^i B ) i^i C ) = ( ( x vH ( A i^i B ) ) i^i C ) ) |
19 |
14 18
|
syl5eqr |
|- ( ( x e. CH /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( ( x vH ( A i^i B ) ) i^i C ) ) |
20 |
19
|
adantrlr |
|- ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ x C_ B ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( ( x vH ( A i^i B ) ) i^i C ) ) |
21 |
20
|
adantrrr |
|- ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( ( x vH ( A i^i B ) ) i^i C ) ) |
22 |
1 2
|
chincli |
|- ( A i^i B ) e. CH |
23 |
|
mdi |
|- ( ( ( ( A i^i B ) e. CH /\ C e. CH /\ x e. CH ) /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( ( A i^i B ) i^i C ) ) ) |
24 |
22 23
|
mp3anl1 |
|- ( ( ( C e. CH /\ x e. CH ) /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( ( A i^i B ) i^i C ) ) ) |
25 |
3 24
|
mpanl1 |
|- ( ( x e. CH /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( ( A i^i B ) i^i C ) ) ) |
26 |
|
inass |
|- ( ( A i^i B ) i^i C ) = ( A i^i ( B i^i C ) ) |
27 |
26
|
oveq2i |
|- ( x vH ( ( A i^i B ) i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) |
28 |
25 27
|
eqtrdi |
|- ( ( x e. CH /\ ( ( A i^i B ) MH C /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
29 |
28
|
adantrll |
|- ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ x C_ C ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
30 |
29
|
adantrrl |
|- ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) ) -> ( ( x vH ( A i^i B ) ) i^i C ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
31 |
21 30
|
eqtrd |
|- ( ( x e. CH /\ ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
32 |
31
|
ancoms |
|- ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( x C_ B /\ x C_ C ) ) /\ x e. CH ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
33 |
32
|
an32s |
|- ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ x e. CH ) /\ ( x C_ B /\ x C_ C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
34 |
13 33
|
sylan2br |
|- ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
35 |
34
|
adantllr |
|- ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( A i^i ( B i^i C ) ) ) ) |
36 |
|
inass |
|- ( ( A i^i C ) i^i ( B i^i C ) ) = ( A i^i ( C i^i ( B i^i C ) ) ) |
37 |
|
in12 |
|- ( C i^i ( B i^i C ) ) = ( B i^i ( C i^i C ) ) |
38 |
|
inidm |
|- ( C i^i C ) = C |
39 |
38
|
ineq2i |
|- ( B i^i ( C i^i C ) ) = ( B i^i C ) |
40 |
37 39
|
eqtri |
|- ( C i^i ( B i^i C ) ) = ( B i^i C ) |
41 |
40
|
ineq2i |
|- ( A i^i ( C i^i ( B i^i C ) ) ) = ( A i^i ( B i^i C ) ) |
42 |
36 41
|
eqtr2i |
|- ( A i^i ( B i^i C ) ) = ( ( A i^i C ) i^i ( B i^i C ) ) |
43 |
|
ssrin |
|- ( ( A i^i C ) C_ D -> ( ( A i^i C ) i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) ) |
44 |
42 43
|
eqsstrid |
|- ( ( A i^i C ) C_ D -> ( A i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) ) |
45 |
|
ssrin |
|- ( D C_ A -> ( D i^i ( B i^i C ) ) C_ ( A i^i ( B i^i C ) ) ) |
46 |
44 45
|
anim12i |
|- ( ( ( A i^i C ) C_ D /\ D C_ A ) -> ( ( A i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) /\ ( D i^i ( B i^i C ) ) C_ ( A i^i ( B i^i C ) ) ) ) |
47 |
|
eqss |
|- ( ( A i^i ( B i^i C ) ) = ( D i^i ( B i^i C ) ) <-> ( ( A i^i ( B i^i C ) ) C_ ( D i^i ( B i^i C ) ) /\ ( D i^i ( B i^i C ) ) C_ ( A i^i ( B i^i C ) ) ) ) |
48 |
46 47
|
sylibr |
|- ( ( ( A i^i C ) C_ D /\ D C_ A ) -> ( A i^i ( B i^i C ) ) = ( D i^i ( B i^i C ) ) ) |
49 |
48
|
oveq2d |
|- ( ( ( A i^i C ) C_ D /\ D C_ A ) -> ( x vH ( A i^i ( B i^i C ) ) ) = ( x vH ( D i^i ( B i^i C ) ) ) ) |
50 |
49
|
ad3antlr |
|- ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( x vH ( A i^i ( B i^i C ) ) ) = ( x vH ( D i^i ( B i^i C ) ) ) ) |
51 |
35 50
|
eqtrd |
|- ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH A ) i^i ( B i^i C ) ) = ( x vH ( D i^i ( B i^i C ) ) ) ) |
52 |
12 51
|
sseqtrd |
|- ( ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) /\ x C_ ( B i^i C ) ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) |
53 |
52
|
ex |
|- ( ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) /\ x e. CH ) -> ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) ) |
54 |
53
|
ralrimiva |
|- ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) -> A. x e. CH ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) ) |
55 |
2 3
|
chincli |
|- ( B i^i C ) e. CH |
56 |
|
mdbr2 |
|- ( ( D e. CH /\ ( B i^i C ) e. CH ) -> ( D MH ( B i^i C ) <-> A. x e. CH ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) ) ) |
57 |
4 55 56
|
mp2an |
|- ( D MH ( B i^i C ) <-> A. x e. CH ( x C_ ( B i^i C ) -> ( ( x vH D ) i^i ( B i^i C ) ) C_ ( x vH ( D i^i ( B i^i C ) ) ) ) ) |
58 |
54 57
|
sylibr |
|- ( ( ( A MH B /\ ( A i^i B ) MH C ) /\ ( ( A i^i C ) C_ D /\ D C_ A ) ) -> D MH ( B i^i C ) ) |