Metamath Proof Explorer

Theorem dihlsscpre

Description: Closure of isomorphism H for a lattice K when -. X .<_ W . (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihval.b 
|- B = ( Base ` K )
dihval.l 
|- .<_ = ( le ` K )
dihval.j 
|- .\/ = ( join ` K )
dihval.m 
|- ./\ = ( meet ` K )
dihval.a 
|- A = ( Atoms ` K )
dihval.h 
|- H = ( LHyp ` K )
dihval.i 
|- I = ( ( DIsoH ` K ) ` W )
dihval.d 
|- D = ( ( DIsoB ` K ) ` W )
dihval.c 
|- C = ( ( DIsoC ` K ) ` W )
dihval.u 
|- U = ( ( DVecH ` K ) ` W )
dihval.s 
|- S = ( LSubSp ` U )
dihval.p 
|- .(+) = ( LSSum ` U )
Assertion dihlsscpre 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` X ) e. S )

Proof

Step Hyp Ref Expression
1 dihval.b 
 |-  B = ( Base ` K )
2 dihval.l 
 |-  .<_ = ( le ` K )
3 dihval.j 
 |-  .\/ = ( join ` K )
4 dihval.m 
 |-  ./\ = ( meet ` K )
5 dihval.a 
 |-  A = ( Atoms ` K )
6 dihval.h 
 |-  H = ( LHyp ` K )
7 dihval.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dihval.d 
 |-  D = ( ( DIsoB ` K ) ` W )
9 dihval.c 
 |-  C = ( ( DIsoC ` K ) ` W )
10 dihval.u 
 |-  U = ( ( DVecH ` K ) ` W )
11 dihval.s 
 |-  S = ( LSubSp ` U )
12 dihval.p 
 |-  .(+) = ( LSSum ` U )
13 1 2 3 4 5 6 7 8 9 10 11 12 dihvalc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` X ) = ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
14 simp1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( K e. HL /\ W e. H ) )
15 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> q e. A )
16 simp3ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> -. q .<_ W )
17 15 16 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( q e. A /\ -. q .<_ W ) )
18 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> r e. A )
19 simp3rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> -. r .<_ W )
20 18 19 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( r e. A /\ -. r .<_ W ) )
21 simp1rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> X e. B )
22 simp3lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( q .\/ ( X ./\ W ) ) = X )
23 simp3rr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( r .\/ ( X ./\ W ) ) = X )
24 22 23 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( q .\/ ( X ./\ W ) ) = ( r .\/ ( X ./\ W ) ) )
25 1 2 3 4 5 6 8 9 10 12 dihjust 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( r e. A /\ -. r .<_ W ) /\ X e. B ) /\ ( q .\/ ( X ./\ W ) ) = ( r .\/ ( X ./\ W ) ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) )
26 14 17 20 21 24 25 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ r e. A ) /\ ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) )
27 26 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( ( q e. A /\ r e. A ) -> ( ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
28 27 ralrimivv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> A. q e. A A. r e. A ( ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) ) )
29 1 2 3 4 5 6 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) )
30 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( K e. HL /\ W e. H ) )
31 6 10 30 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> U e. LMod )
32 2 5 6 10 9 11 diclss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( C ` q ) e. S )
33 32 adantlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( C ` q ) e. S )
34 hllat 
 |-  ( K e. HL -> K e. Lat )
35 34 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> K e. Lat )
36 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> X e. B )
37 1 6 lhpbase 
 |-  ( W e. H -> W e. B )
38 37 ad3antlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> W e. B )
39 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
40 35 36 38 39 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( X ./\ W ) e. B )
41 1 2 4 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
42 35 36 38 41 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( X ./\ W ) .<_ W )
43 1 2 6 10 8 11 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( D ` ( X ./\ W ) ) e. S )
44 30 40 42 43 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( D ` ( X ./\ W ) ) e. S )
45 11 12 lsmcl 
 |-  ( ( U e. LMod /\ ( C ` q ) e. S /\ ( D ` ( X ./\ W ) ) e. S ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S )
46 31 33 44 45 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S )
47 46 a1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( ( q .\/ ( X ./\ W ) ) = X -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) )
48 47 expr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ q e. A ) -> ( -. q .<_ W -> ( ( q .\/ ( X ./\ W ) ) = X -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) ) )
49 48 impd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ q e. A ) -> ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) )
50 49 ancld 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) /\ q e. A ) -> ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) ) )
51 50 reximdva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> E. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) ) )
52 29 51 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) )
53 breq1 
 |-  ( q = r -> ( q .<_ W <-> r .<_ W ) )
54 53 notbid 
 |-  ( q = r -> ( -. q .<_ W <-> -. r .<_ W ) )
55 oveq1 
 |-  ( q = r -> ( q .\/ ( X ./\ W ) ) = ( r .\/ ( X ./\ W ) ) )
56 55 eqeq1d 
 |-  ( q = r -> ( ( q .\/ ( X ./\ W ) ) = X <-> ( r .\/ ( X ./\ W ) ) = X ) )
57 54 56 anbi12d 
 |-  ( q = r -> ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) <-> ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) )
58 fveq2 
 |-  ( q = r -> ( C ` q ) = ( C ` r ) )
59 58 oveq1d 
 |-  ( q = r -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) )
60 57 59 reusv3 
 |-  ( E. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) e. S ) -> ( A. q e. A A. r e. A ( ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) ) <-> E. u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
61 52 60 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( A. q e. A A. r e. A ( ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) /\ ( -. r .<_ W /\ ( r .\/ ( X ./\ W ) ) = X ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` r ) .(+) ( D ` ( X ./\ W ) ) ) ) <-> E. u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
62 28 61 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) )
63 reusv1 
 |-  ( E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> ( E! u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) <-> E. u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
64 29 63 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( E! u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) <-> E. u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
65 62 64 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E! u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) )
66 riotacl 
 |-  ( E! u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) -> ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) e. S )
67 65 66 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) e. S )
68 13 67 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` X ) e. S )