cdlemftr0

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

	Ref	Expression
Hypotheses	cdlemftr0.b	$⊢ B = {Base}_{K}$
	cdlemftr0.h	$⊢ H = LHyp (K)$
	cdlemftr0.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemftr0	$⊢ (K \in HL \land W \in H) \to \exists f \in T f \neq {I ↾}_{B}$

Step	Hyp	Ref	Expression
1		cdlemftr0.b	$⊢ B = {Base}_{K}$
2		cdlemftr0.h	$⊢ H = LHyp (K)$
3		cdlemftr0.t	$⊢ T = LTrn (K) (W)$
4		eqid	$⊢ trL (K) (W) = trL (K) (W)$
5	1 2 3 4	cdlemftr1	$⊢ (K \in HL \land W \in H) \to \exists f \in T (f \neq {I ↾}_{B} \land trL (K) (W) (f) \neq I)$
6		simpl	$⊢ (f \neq {I ↾}_{B} \land trL (K) (W) (f) \neq I) \to f \neq {I ↾}_{B}$
7	6	reximi	$⊢ \exists f \in T (f \neq {I ↾}_{B} \land trL (K) (W) (f) \neq I) \to \exists f \in T f \neq {I ↾}_{B}$
8	5 7	syl	$⊢ (K \in HL \land W \in H) \to \exists f \in T f \neq {I ↾}_{B}$

Metamath Proof Explorer