Theorem cdleme

Description: Lemma E in Crawley p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		cdleme.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		cdleme.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5	1 2 3 4	cdleme50ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
6		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) ) → 𝑓 ∈ 𝑇 )
8		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) ) → 𝑧 ∈ 𝑇 )
9		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
10		eqtr3	⊢ ( ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) → ( 𝑓 ‘ 𝑃 ) = ( 𝑧 ‘ 𝑃 ) )
11	10	3ad2ant3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) ) → ( 𝑓 ‘ 𝑃 ) = ( 𝑧 ‘ 𝑃 ) )
12	1 2 3 4	cdlemd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑓 ‘ 𝑃 ) = ( 𝑧 ‘ 𝑃 ) ) → 𝑓 = 𝑧 )
13	6 7 8 9 11 12	syl311anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ∧ ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) ) → 𝑓 = 𝑧 )
14	13	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑓 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) → 𝑓 = 𝑧 ) ) )
15	14	ralrimivv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∀ 𝑓 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) → 𝑓 = 𝑧 ) )
16		fveq1	⊢ ( 𝑓 = 𝑧 → ( 𝑓 ‘ 𝑃 ) = ( 𝑧 ‘ 𝑃 ) )
17	16	eqeq1d	⊢ ( 𝑓 = 𝑧 → ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ↔ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) )
18	17	reu4	⊢ ( ∃! 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ↔ ( ∃ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑓 ‘ 𝑃 ) = 𝑄 ∧ ( 𝑧 ‘ 𝑃 ) = 𝑄 ) → 𝑓 = 𝑧 ) ) )
19	5 15 18	sylanbrc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∃! 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )