# Metamath Proof Explorer

## Theorem dia0

Description: The value of the partial isomorphism A at the lattice zero is the singleton of the identity translation i.e. the zero subspace. (Contributed by NM, 26-Nov-2013)

Ref Expression
Hypotheses dia0.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dia0.z
dia0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dia0.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
Assertion dia0

### Proof

Step Hyp Ref Expression
1 dia0.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dia0.z
3 dia0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dia0.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
5 id ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
7 1 2 atl0cl
8 6 7 syl
10 1 3 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
11 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
12 1 11 2 atl0le
13 6 10 12 syl2an
14 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
15 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
16 1 11 3 14 15 4 diaval
17 5 9 13 16 syl12anc
18 6 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {K}\in \mathrm{AtLat}$
19 1 3 14 15 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\in {B}$
20 1 11 2 atlle0
21 18 19 20 syl2anc
22 1 2 3 14 15 trlid0b
23 21 22 bitr4d
24 23 rabbidva
25 1 3 14 idltrn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{B}}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
26 rabsn ${⊢}{\mathrm{I}↾}_{{B}}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\to \left\{{f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)|{f}={\mathrm{I}↾}_{{B}}\right\}=\left\{{\mathrm{I}↾}_{{B}}\right\}$
27 25 26 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left\{{f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)|{f}={\mathrm{I}↾}_{{B}}\right\}=\left\{{\mathrm{I}↾}_{{B}}\right\}$
28 17 24 27 3eqtrd