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 )