# Metamath Proof Explorer

## Theorem dihprrn

Description: The span of a vector pair belongs to the range of isomorphism H i.e. is a closed subspace. (Contributed by NM, 29-Sep-2014)

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

### Proof

Step Hyp Ref Expression
1 dihprrn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dihprrn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dihprrn.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 dihprrn.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
5 dihprrn.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
6 dihprrn.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 dihprrn.x ${⊢}{\phi }\to {X}\in {V}$
8 dihprrn.y ${⊢}{\phi }\to {Y}\in {V}$
9 prcom ${⊢}\left\{{X},{Y}\right\}=\left\{{Y},{X}\right\}$
10 preq2 ${⊢}{X}={0}_{{U}}\to \left\{{Y},{X}\right\}=\left\{{Y},{0}_{{U}}\right\}$
11 9 10 syl5eq ${⊢}{X}={0}_{{U}}\to \left\{{X},{Y}\right\}=\left\{{Y},{0}_{{U}}\right\}$
12 11 fveq2d ${⊢}{X}={0}_{{U}}\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{Y},{0}_{{U}}\right\}\right)$
13 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
14 1 2 6 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
15 3 13 4 14 8 lsppr0 ${⊢}{\phi }\to {N}\left(\left\{{Y},{0}_{{U}}\right\}\right)={N}\left(\left\{{Y}\right\}\right)$
16 12 15 sylan9eqr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{Y}\right\}\right)$
17 1 2 3 4 5 dihlsprn ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{ran}{I}$
18 6 8 17 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{ran}{I}$
19 18 adantr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{ran}{I}$
20 16 19 eqeltrd ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{ran}{I}$
21 preq2 ${⊢}{Y}={0}_{{U}}\to \left\{{X},{Y}\right\}=\left\{{X},{0}_{{U}}\right\}$
22 21 fveq2d ${⊢}{Y}={0}_{{U}}\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X},{0}_{{U}}\right\}\right)$
23 3 13 4 14 7 lsppr0 ${⊢}{\phi }\to {N}\left(\left\{{X},{0}_{{U}}\right\}\right)={N}\left(\left\{{X}\right\}\right)$
24 22 23 sylan9eqr ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X}\right\}\right)$
25 1 2 3 4 5 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}$
26 6 7 25 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$
27 26 adantr ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{ran}{I}$
28 24 27 eqeltrd ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{ran}{I}$
29 6 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
30 7 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {X}\in {V}$
31 8 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {Y}\in {V}$
32 simprl ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {X}\ne {0}_{{U}}$
33 simprr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {Y}\ne {0}_{{U}}$
34 1 2 3 4 5 29 30 31 13 32 33 dihprrnlem2 ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{ran}{I}$
35 20 28 34 pm2.61da2ne ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{ran}{I}$