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

Metamath Proof Explorer

Theorem ltrniotaval

Description: Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014)

Ref Expression
Hypotheses ltrniotaval.l 
|- .<_ = ( le ` K )
ltrniotaval.a 
|- A = ( Atoms ` K )
ltrniotaval.h 
|- H = ( LHyp ` K )
ltrniotaval.t 
|- T = ( ( LTrn ` K ) ` W )
ltrniotaval.f 
|- F = ( iota_ f e. T ( f ` P ) = Q )
Assertion ltrniotaval 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( F ` P ) = Q )

Proof

Step Hyp Ref Expression
1 ltrniotaval.l 
 |-  .<_ = ( le ` K )
2 ltrniotaval.a 
 |-  A = ( Atoms ` K )
3 ltrniotaval.h 
 |-  H = ( LHyp ` K )
4 ltrniotaval.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 ltrniotaval.f 
 |-  F = ( iota_ f e. T ( f ` P ) = Q )
6 1 2 3 4 cdleme 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E! f e. T ( f ` P ) = Q )
7 nfriota1 
 |-  F/_ f ( iota_ f e. T ( f ` P ) = Q )
8 5 7 nfcxfr 
 |-  F/_ f F
9 nfcv 
 |-  F/_ f P
10 8 9 nffv 
 |-  F/_ f ( F ` P )
11 10 nfeq1 
 |-  F/ f ( F ` P ) = Q
12 fveq1 
 |-  ( f = F -> ( f ` P ) = ( F ` P ) )
13 12 eqeq1d 
 |-  ( f = F -> ( ( f ` P ) = Q <-> ( F ` P ) = Q ) )
14 11 5 13 riotaprop 
 |-  ( E! f e. T ( f ` P ) = Q -> ( F e. T /\ ( F ` P ) = Q ) )
15 14 simprd 
 |-  ( E! f e. T ( f ` P ) = Q -> ( F ` P ) = Q )
16 6 15 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( F ` P ) = Q )