Metamath Proof Explorer

Theorem ltrnu

Description: Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom W . Similar to definition of translation in Crawley p. 111. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrnu.l 
|- .<_ = ( le ` K )
ltrnu.j 
|- .\/ = ( join ` K )
ltrnu.m 
|- ./\ = ( meet ` K )
ltrnu.a 
|- A = ( Atoms ` K )
ltrnu.h 
|- H = ( LHyp ` K )
ltrnu.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion ltrnu 
|- ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) )

Proof

Step Hyp Ref Expression
1 ltrnu.l 
 |-  .<_ = ( le ` K )
2 ltrnu.j 
 |-  .\/ = ( join ` K )
3 ltrnu.m 
 |-  ./\ = ( meet ` K )
4 ltrnu.a 
 |-  A = ( Atoms ` K )
5 ltrnu.h 
 |-  H = ( LHyp ` K )
6 ltrnu.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 an4 
 |-  ( ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) <-> ( ( P e. A /\ Q e. A ) /\ ( -. P .<_ W /\ -. Q .<_ W ) ) )
8 simpr 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ Q e. A ) ) -> ( P e. A /\ Q e. A ) )
9 simplr 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ Q e. A ) ) -> F e. T )
10 eqid 
 |-  ( ( LDil ` K ) ` W ) = ( ( LDil ` K ) ` W )
11 1 2 3 4 5 10 6 isltrn 
 |-  ( ( K e. V /\ W e. H ) -> ( F e. T <-> ( F e. ( ( LDil ` K ) ` W ) /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) ) )
12 11 ad2antrr 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ Q e. A ) ) -> ( F e. T <-> ( F e. ( ( LDil ` K ) ` W ) /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) ) )
13 simpr 
 |-  ( ( F e. ( ( LDil ` K ) ` W ) /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) -> A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
14 12 13 biimtrdi 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ Q e. A ) ) -> ( F e. T -> A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
15 9 14 mpd 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ Q e. A ) ) -> A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
16 breq1 
 |-  ( p = P -> ( p .<_ W <-> P .<_ W ) )
17 16 notbid 
 |-  ( p = P -> ( -. p .<_ W <-> -. P .<_ W ) )
18 17 anbi1d 
 |-  ( p = P -> ( ( -. p .<_ W /\ -. q .<_ W ) <-> ( -. P .<_ W /\ -. q .<_ W ) ) )
19 id 
 |-  ( p = P -> p = P )
20 fveq2 
 |-  ( p = P -> ( F ` p ) = ( F ` P ) )
21 19 20 oveq12d 
 |-  ( p = P -> ( p .\/ ( F ` p ) ) = ( P .\/ ( F ` P ) ) )
22 21 oveq1d 
 |-  ( p = P -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
23 22 eqeq1d 
 |-  ( p = P -> ( ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) <-> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
24 18 23 imbi12d 
 |-  ( p = P -> ( ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) <-> ( ( -. P .<_ W /\ -. q .<_ W ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
25 breq1 
 |-  ( q = Q -> ( q .<_ W <-> Q .<_ W ) )
26 25 notbid 
 |-  ( q = Q -> ( -. q .<_ W <-> -. Q .<_ W ) )
27 26 anbi2d 
 |-  ( q = Q -> ( ( -. P .<_ W /\ -. q .<_ W ) <-> ( -. P .<_ W /\ -. Q .<_ W ) ) )
28 id 
 |-  ( q = Q -> q = Q )
29 fveq2 
 |-  ( q = Q -> ( F ` q ) = ( F ` Q ) )
30 28 29 oveq12d 
 |-  ( q = Q -> ( q .\/ ( F ` q ) ) = ( Q .\/ ( F ` Q ) ) )
31 30 oveq1d 
 |-  ( q = Q -> ( ( q .\/ ( F ` q ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) )
32 31 eqeq2d 
 |-  ( q = Q -> ( ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) <-> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) ) )
33 27 32 imbi12d 
 |-  ( q = Q -> ( ( ( -. P .<_ W /\ -. q .<_ W ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) <-> ( ( -. P .<_ W /\ -. Q .<_ W ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) ) ) )
34 24 33 rspc2v 
 |-  ( ( P e. A /\ Q e. A ) -> ( A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) -> ( ( -. P .<_ W /\ -. Q .<_ W ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) ) ) )
35 8 15 34 sylc 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ Q e. A ) ) -> ( ( -. P .<_ W /\ -. Q .<_ W ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) ) )
36 35 impr 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( ( P e. A /\ Q e. A ) /\ ( -. P .<_ W /\ -. Q .<_ W ) ) ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) )
37 7 36 sylan2b 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) )
38 37 3impb 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) )