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

Metamath Proof Explorer

Theorem cdlemftr0

Description: Special case of cdlemf showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013)

Ref Expression
Hypotheses cdlemftr0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemftr0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemftr0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemftr0 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cdlemftr0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemftr0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 cdlemftr0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 3 4 cdlemftr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≠ I ) )
6 simpl ⊢ ( ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≠ I ) → 𝑓 ≠ ( I ↾ 𝐵 ) )
7 6 reximi ⊢ ( ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≠ I ) → ∃ 𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵 ) )
8 5 7 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵 ) )