# Metamath Proof Explorer

## Theorem ltrnid

Description: A lattice translation is the identity function iff all atoms not under the fiducial co-atom W are equal to their values. (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses ltrneq.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
ltrneq.l
ltrneq.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
ltrneq.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
ltrneq.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
Assertion ltrnid

### Proof

Step Hyp Ref Expression
1 ltrneq.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 ltrneq.l
3 ltrneq.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 ltrneq.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 ltrneq.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 simp-4l
7 eqid ${⊢}\mathrm{LAut}\left({K}\right)=\mathrm{LAut}\left({K}\right)$
8 4 7 5 ltrnlaut ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}\in \mathrm{LAut}\left({K}\right)$
10 simpr
11 simplll
12 simpllr
13 1 3 atbase ${⊢}{p}\in {A}\to {p}\in {B}$
15 simpr
16 1 2 4 5 ltrnval1
17 11 12 14 15 16 syl112anc
18 17 ex
19 pm2.61
20 18 19 syl
21 20 ralimdva
22 21 imp
24 1 3 7 lauteq ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {F}\in \mathrm{LAut}\left({K}\right)\wedge {x}\in {B}\right)\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={p}\right)\to {F}\left({x}\right)={x}$
25 6 9 10 23 24 syl31anc
26 fvresi ${⊢}{x}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({x}\right)={x}$
28 25 27 eqtr4d
29 28 ralrimiva
30 1 4 5 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}:{B}\underset{1-1 onto}{⟶}{B}$
32 f1ofn ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{B}\to {F}Fn{B}$
33 31 32 syl
34 fnresi ${⊢}\left({\mathrm{I}↾}_{{B}}\right)Fn{B}$
35 eqfnfv ${⊢}\left({F}Fn{B}\wedge \left({\mathrm{I}↾}_{{B}}\right)Fn{B}\right)\to \left({F}={\mathrm{I}↾}_{{B}}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({x}\right)\right)$
36 33 34 35 sylancl
37 29 36 mpbird
38 37 ex
39 13 adantl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {p}\in {A}\right)\to {p}\in {B}$
40 fvresi ${⊢}{p}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({p}\right)={p}$
41 39 40 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {p}\in {A}\right)\to \left({\mathrm{I}↾}_{{B}}\right)\left({p}\right)={p}$
42 fveq1 ${⊢}{F}={\mathrm{I}↾}_{{B}}\to {F}\left({p}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({p}\right)$
43 42 eqeq1d ${⊢}{F}={\mathrm{I}↾}_{{B}}\to \left({F}\left({p}\right)={p}↔\left({\mathrm{I}↾}_{{B}}\right)\left({p}\right)={p}\right)$
44 41 43 syl5ibrcom ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {p}\in {A}\right)\to \left({F}={\mathrm{I}↾}_{{B}}\to {F}\left({p}\right)={p}\right)$
45 44 a1dd
46 45 ralrimdva
47 38 46 impbid