# Metamath Proof Explorer

## Theorem diassdvaN

Description: The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses diassdva.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
diassdva.l
diassdva.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
diassdva.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
diassdva.u ${⊢}{U}=\mathrm{DVecA}\left({K}\right)\left({W}\right)$
diassdva.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
Assertion diassdvaN

### Proof

Step Hyp Ref Expression
1 diassdva.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 diassdva.l
3 diassdva.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 diassdva.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
5 diassdva.u ${⊢}{U}=\mathrm{DVecA}\left({K}\right)\left({W}\right)$
6 diassdva.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
7 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 1 2 3 7 8 4 diaval
10 ssrab2
11 3 7 5 6 dvavbase ${⊢}\left({K}\in {Y}\wedge {W}\in {H}\right)\to {V}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$