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

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∃! 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )