Metamath Proof Explorer

Theorem dihmeetlem17N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem14.b 
|- B = ( Base ` K )
dihmeetlem14.l 
|- .<_ = ( le ` K )
dihmeetlem14.h 
|- H = ( LHyp ` K )
dihmeetlem14.j 
|- .\/ = ( join ` K )
dihmeetlem14.m 
|- ./\ = ( meet ` K )
dihmeetlem14.a 
|- A = ( Atoms ` K )
dihmeetlem14.u 
|- U = ( ( DVecH ` K ) ` W )
dihmeetlem14.s 
|- .(+) = ( LSSum ` U )
dihmeetlem14.i 
|- I = ( ( DIsoH ` K ) ` W )
dihmeetlem17.o 
|- .0. = ( 0. ` K )
Assertion dihmeetlem17N 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( Y ./\ p ) = .0. )

Proof

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 dihmeetlem17.o 
 |-  .0. = ( 0. ` K )
11 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> K e. HL )
12 11 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> K e. Lat )
13 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> p e. A )
14 1 6 atbase 
 |-  ( p e. A -> p e. B )
15 13 14 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> p e. B )
16 simpr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> Y e. B )
17 1 5 latmcom 
 |-  ( ( K e. Lat /\ p e. B /\ Y e. B ) -> ( p ./\ Y ) = ( Y ./\ p ) )
18 12 15 16 17 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( p ./\ Y ) = ( Y ./\ p ) )
19 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( K e. HL /\ W e. H ) )
20 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( X e. B /\ -. X .<_ W ) )
21 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( p e. A /\ -. p .<_ W ) )
22 simpr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( X ./\ Y ) .<_ W )
23 simpr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> p .<_ X )
24 1 2 4 5 6 3 lhpmcvr4N 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> -. p .<_ Y )
25 19 20 21 16 22 23 24 syl123anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> -. p .<_ Y )
26 hlatl 
 |-  ( K e. HL -> K e. AtLat )
27 11 26 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> K e. AtLat )
28 1 2 5 10 6 atnle 
 |-  ( ( K e. AtLat /\ p e. A /\ Y e. B ) -> ( -. p .<_ Y <-> ( p ./\ Y ) = .0. ) )
29 27 13 16 28 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( -. p .<_ Y <-> ( p ./\ Y ) = .0. ) )
30 25 29 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( p ./\ Y ) = .0. )
31 18 30 eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ p .<_ X ) ) -> ( Y ./\ p ) = .0. )