# Metamath Proof Explorer

## Theorem dihlsprn

Description: The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dihlsprn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihlsprn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihlsprn.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dihlsprn.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
dihlsprn.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihlsprn ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$

### Proof

Step Hyp Ref Expression
1 dihlsprn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dihlsprn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dihlsprn.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 dihlsprn.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
5 dihlsprn.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
6 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to {X}={0}_{{U}}$
7 6 sneqd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to \left\{{X}\right\}=\left\{{0}_{{U}}\right\}$
8 7 fveq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{0}_{{U}}\right\}\right)$
9 simpll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 1 2 9 dvhlmod ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to {U}\in \mathrm{LMod}$
11 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
12 11 4 lspsn0 ${⊢}{U}\in \mathrm{LMod}\to {N}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{U}}\right\}$
13 10 12 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{U}}\right\}$
14 8 13 eqtrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)=\left\{{0}_{{U}}\right\}$
15 1 5 2 11 dih0rn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left\{{0}_{{U}}\right\}\in \mathrm{ran}{I}$
16 15 ad2antrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to \left\{{0}_{{U}}\right\}\in \mathrm{ran}{I}$
17 14 16 eqeltrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$
18 simpll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}\ne {0}_{{U}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
19 1 2 18 dvhlmod ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}\ne {0}_{{U}}\right)\to {U}\in \mathrm{LMod}$
20 simplr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}\ne {0}_{{U}}\right)\to {X}\in {V}$
21 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}\ne {0}_{{U}}\right)\to {X}\ne {0}_{{U}}$
22 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
23 3 4 11 22 lsatlspsn2 ${⊢}\left({U}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {X}\ne {0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSAtoms}\left({U}\right)$
24 19 20 21 23 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}\ne {0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSAtoms}\left({U}\right)$
25 1 2 5 22 dih1dimat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSAtoms}\left({U}\right)\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$
26 18 24 25 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\wedge {X}\ne {0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$
27 17 26 pm2.61dane ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$