# Metamath Proof Explorer

## 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 {T}\phantom{\rule{.4em}{0ex}}{f}\ne {\mathrm{I}↾}_{{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}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\wedge \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\ne \mathrm{I}\right)$
6 simpl ${⊢}\left({f}\ne {\mathrm{I}↾}_{{B}}\wedge \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\ne \mathrm{I}\right)\to {f}\ne {\mathrm{I}↾}_{{B}}$
7 6 reximi ${⊢}\exists {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\wedge \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\ne \mathrm{I}\right)\to \exists {f}\in {T}\phantom{\rule{.4em}{0ex}}{f}\ne {\mathrm{I}↾}_{{B}}$
8 5 7 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \exists {f}\in {T}\phantom{\rule{.4em}{0ex}}{f}\ne {\mathrm{I}↾}_{{B}}$