Theorem cdlemg1ci2

Description: Any function of the form of the function constructed for cdleme is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg1c.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg1c.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		cdlemg1c.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		cdlemg1c.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ) → 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) )
6		eqid	⊢ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
7	1 2 3 4 6	ltrniotacl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ∈ 𝑇 )
8	7	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ∈ 𝑇 )
9	5 8	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ) → 𝐹 ∈ 𝑇 )