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={\mathrm{Base}}_K$$
	cdlemftr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemftr.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemftr.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
Assertion	cdlemftr1	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists f\in T\left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemftr.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemftr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		cdlemftr.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		cdlemftr.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
5	1 2 3 4	cdlemftr2	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists f\in T\left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\wedge R\left(f\right)\ne X\right)$$
6		3simpa	$$⊢\left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\wedge R\left(f\right)\ne X\right)\to \left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\right)$$
7	6	reximi	$$⊢\exists f\in T\left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\wedge R\left(f\right)\ne X\right)\to \exists f\in T\left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\right)$$
8	5 7	syl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists f\in T\left(f\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(f\right)\ne X\right)$$