This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trlval

Description: The value of the trace of a lattice translation. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses trlset.b 
|- B = ( Base ` K )
trlset.l 
|- .<_ = ( le ` K )
trlset.j 
|- .\/ = ( join ` K )
trlset.m 
|- ./\ = ( meet ` K )
trlset.a 
|- A = ( Atoms ` K )
trlset.h 
|- H = ( LHyp ` K )
trlset.t 
|- T = ( ( LTrn ` K ) ` W )
trlset.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlval 
|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> ( R ` F ) = ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )

Proof

Step Hyp Ref Expression
1 trlset.b 
 |-  B = ( Base ` K )
2 trlset.l 
 |-  .<_ = ( le ` K )
3 trlset.j 
 |-  .\/ = ( join ` K )
4 trlset.m 
 |-  ./\ = ( meet ` K )
5 trlset.a 
 |-  A = ( Atoms ` K )
6 trlset.h 
 |-  H = ( LHyp ` K )
7 trlset.t 
 |-  T = ( ( LTrn ` K ) ` W )
8 trlset.r 
 |-  R = ( ( trL ` K ) ` W )
9 1 2 3 4 5 6 7 8 trlset 
 |-  ( ( K e. V /\ W e. H ) -> R = ( f e. T |-> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) ) )
10 9 fveq1d 
 |-  ( ( K e. V /\ W e. H ) -> ( R ` F ) = ( ( f e. T |-> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) ) ` F ) )
11 fveq1 
 |-  ( f = F -> ( f ` p ) = ( F ` p ) )
12 11 oveq2d 
 |-  ( f = F -> ( p .\/ ( f ` p ) ) = ( p .\/ ( F ` p ) ) )
13 12 oveq1d 
 |-  ( f = F -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( p .\/ ( F ` p ) ) ./\ W ) )
14 13 eqeq2d 
 |-  ( f = F -> ( x = ( ( p .\/ ( f ` p ) ) ./\ W ) <-> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) )
15 14 imbi2d 
 |-  ( f = F -> ( ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) <-> ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )
16 15 ralbidv 
 |-  ( f = F -> ( A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) <-> A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )
17 16 riotabidv 
 |-  ( f = F -> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) = ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )
18 eqid 
 |-  ( f e. T |-> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) ) = ( f e. T |-> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) )
19 riotaex 
 |-  ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) e. _V
20 17 18 19 fvmpt 
 |-  ( F e. T -> ( ( f e. T |-> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) ) ` F ) = ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )
21 10 20 sylan9eq 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> ( R ` F ) = ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )