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

Proof

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