# Metamath Proof Explorer

## Theorem dib0

Description: The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014)

Ref Expression
Hypotheses dib0.z
dib0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dib0.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
dib0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dib0.o ${⊢}{O}={0}_{{U}}$
Assertion dib0

### Proof

Step Hyp Ref Expression
1 dib0.z
2 dib0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dib0.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
4 dib0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dib0.o ${⊢}{O}={0}_{{U}}$
6 fvex ${⊢}{\mathrm{Base}}_{{K}}\in \mathrm{V}$
7 resiexg ${⊢}{\mathrm{Base}}_{{K}}\in \mathrm{V}\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\in \mathrm{V}$
8 6 7 ax-mp ${⊢}{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\in \mathrm{V}$
9 fvex ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)\in \mathrm{V}$
10 9 mptex ${⊢}\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\in \mathrm{V}$
11 8 10 xpsn ${⊢}\left\{{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right\}×\left\{\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right\}=\left\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)⟩\right\}$
12 id ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
13 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
14 13 adantr ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {K}\in \mathrm{OP}$
15 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
16 15 1 op0cl
17 14 16 syl
18 15 2 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
19 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
20 15 19 1 op0le
21 13 18 20 syl2an
22 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
23 eqid ${⊢}\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)=\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)$
24 eqid ${⊢}\mathrm{DIsoA}\left({K}\right)\left({W}\right)=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
25 15 19 2 22 23 24 3 dibval2
26 12 17 21 25 syl12anc
27 15 1 2 24 dia0
28 27 xpeq1d
29 26 28 eqtrd
30 15 2 22 4 5 23 dvh0g ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)⟩$
31 30 sneqd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left\{{O}\right\}=\left\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},\left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)⟩\right\}$
32 11 29 31 3eqtr4a