Step |
Hyp |
Ref |
Expression |
1 |
|
dihmeetlem14.b |
|- B = ( Base ` K ) |
2 |
|
dihmeetlem14.l |
|- .<_ = ( le ` K ) |
3 |
|
dihmeetlem14.h |
|- H = ( LHyp ` K ) |
4 |
|
dihmeetlem14.j |
|- .\/ = ( join ` K ) |
5 |
|
dihmeetlem14.m |
|- ./\ = ( meet ` K ) |
6 |
|
dihmeetlem14.a |
|- A = ( Atoms ` K ) |
7 |
|
dihmeetlem14.u |
|- U = ( ( DVecH ` K ) ` W ) |
8 |
|
dihmeetlem14.s |
|- .(+) = ( LSSum ` U ) |
9 |
|
dihmeetlem14.i |
|- I = ( ( DIsoH ` K ) ` W ) |
10 |
|
incom |
|- ( ( I ` p ) i^i ( I ` Y ) ) = ( ( I ` Y ) i^i ( I ` p ) ) |
11 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
12 |
1 2 3 4 5 6 7 8 9 11
|
dihmeetlem18N |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( ( I ` Y ) i^i ( I ` p ) ) = { ( 0g ` U ) } ) |
13 |
10 12
|
syl5eq |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( ( I ` p ) i^i ( I ` Y ) ) = { ( 0g ` U ) } ) |
14 |
13
|
oveq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( ( I ` ( X ./\ Y ) ) .(+) ( ( I ` p ) i^i ( I ` Y ) ) ) = ( ( I ` ( X ./\ Y ) ) .(+) { ( 0g ` U ) } ) ) |
15 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( K e. HL /\ W e. H ) ) |
16 |
|
simpl2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> X e. B ) |
17 |
|
simpl3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> Y e. B ) |
18 |
|
simpr1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( p e. A /\ -. p .<_ W ) ) |
19 |
|
simpr31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> p .<_ X ) |
20 |
|
simpr33 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( X ./\ Y ) .<_ W ) |
21 |
1 2 3 4 5 6 7 8 9
|
dihmeetlem12N |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ p .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( I ` ( X ./\ Y ) ) .(+) ( ( I ` p ) i^i ( I ` Y ) ) ) = ( ( I ` X ) i^i ( I ` Y ) ) ) |
22 |
15 16 17 18 19 20 21
|
syl33anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( ( I ` ( X ./\ Y ) ) .(+) ( ( I ` p ) i^i ( I ` Y ) ) ) = ( ( I ` X ) i^i ( I ` Y ) ) ) |
23 |
3 7 15
|
dvhlmod |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> U e. LMod ) |
24 |
|
simpl1l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> K e. HL ) |
25 |
24
|
hllatd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> K e. Lat ) |
26 |
1 5
|
latmcl |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B ) |
27 |
25 16 17 26
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( X ./\ Y ) e. B ) |
28 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
29 |
1 3 9 7 28
|
dihlss |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X ./\ Y ) e. B ) -> ( I ` ( X ./\ Y ) ) e. ( LSubSp ` U ) ) |
30 |
15 27 29
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( I ` ( X ./\ Y ) ) e. ( LSubSp ` U ) ) |
31 |
28
|
lsssubg |
|- ( ( U e. LMod /\ ( I ` ( X ./\ Y ) ) e. ( LSubSp ` U ) ) -> ( I ` ( X ./\ Y ) ) e. ( SubGrp ` U ) ) |
32 |
23 30 31
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( I ` ( X ./\ Y ) ) e. ( SubGrp ` U ) ) |
33 |
11 8
|
lsm01 |
|- ( ( I ` ( X ./\ Y ) ) e. ( SubGrp ` U ) -> ( ( I ` ( X ./\ Y ) ) .(+) { ( 0g ` U ) } ) = ( I ` ( X ./\ Y ) ) ) |
34 |
32 33
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( ( I ` ( X ./\ Y ) ) .(+) { ( 0g ` U ) } ) = ( I ` ( X ./\ Y ) ) ) |
35 |
14 22 34
|
3eqtr3rd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ Y e. B ) /\ ( ( p e. A /\ -. p .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ ( p .<_ X /\ r .<_ Y /\ ( X ./\ Y ) .<_ W ) ) ) -> ( I ` ( X ./\ Y ) ) = ( ( I ` X ) i^i ( I ` Y ) ) ) |