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 ↾ 𝐵 ) )