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

Metamath Proof Explorer

Theorem cdlemftr1

Description: Part of proof of Lemma G of Crawley p. 116, sixth line of third paragraph on p. 117: there is "a translation h, different from the identity, such that tr h =/= tr f." (Contributed by NM, 25-Jul-2013)

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

Proof

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