Theorem ltrniotaval

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

	Ref	Expression
Hypotheses	ltrniotaval.l	⊢ ≤ = ( le ‘ 𝐾 )
	ltrniotaval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	ltrniotaval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	ltrniotaval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	ltrniotaval.f	⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
Assertion	ltrniotaval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		ltrniotaval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		ltrniotaval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		ltrniotaval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		ltrniotaval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		ltrniotaval.f	⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
6	1 2 3 4	cdleme	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∃! 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
7		nfriota1	⊢ Ⅎ 𝑓 ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
8	5 7	nfcxfr	⊢ Ⅎ 𝑓 𝐹
9		nfcv	⊢ Ⅎ 𝑓 𝑃
10	8 9	nffv	⊢ Ⅎ 𝑓 ( 𝐹 ‘ 𝑃 )
11	10	nfeq1	⊢ Ⅎ 𝑓 ( 𝐹 ‘ 𝑃 ) = 𝑄
12		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑃 ) = ( 𝐹 ‘ 𝑃 ) )
13	12	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ↔ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) )
14	11 5 13	riotaprop	⊢ ( ∃! 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) )
15	14	simprd	⊢ ( ∃! 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 → ( 𝐹 ‘ 𝑃 ) = 𝑄 )
16	6 15	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑄 )