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=LHypK
dihlsprn.u U=DVecHKW
dihlsprn.v V=BaseU
dihlsprn.n N=LSpanU
dihlsprn.i I=DIsoHKW
Assertion dihlsprn KHLWHXVNXranI

Proof

Step Hyp Ref Expression
1 dihlsprn.h H=LHypK
2 dihlsprn.u U=DVecHKW
3 dihlsprn.v V=BaseU
4 dihlsprn.n N=LSpanU
5 dihlsprn.i I=DIsoHKW
6 simpr KHLWHXVX=0UX=0U
7 6 sneqd KHLWHXVX=0UX=0U
8 7 fveq2d KHLWHXVX=0UNX=N0U
9 simpll KHLWHXVX=0UKHLWH
10 1 2 9 dvhlmod KHLWHXVX=0UULMod
11 eqid 0U=0U
12 11 4 lspsn0 ULModN0U=0U
13 10 12 syl KHLWHXVX=0UN0U=0U
14 8 13 eqtrd KHLWHXVX=0UNX=0U
15 1 5 2 11 dih0rn KHLWH0UranI
16 15 ad2antrr KHLWHXVX=0U0UranI
17 14 16 eqeltrd KHLWHXVX=0UNXranI
18 simpll KHLWHXVX0UKHLWH
19 1 2 18 dvhlmod KHLWHXVX0UULMod
20 simplr KHLWHXVX0UXV
21 simpr KHLWHXVX0UX0U
22 eqid LSAtomsU=LSAtomsU
23 3 4 11 22 lsatlspsn2 ULModXVX0UNXLSAtomsU
24 19 20 21 23 syl3anc KHLWHXVX0UNXLSAtomsU
25 1 2 5 22 dih1dimat KHLWHNXLSAtomsUNXranI
26 18 24 25 syl2anc KHLWHXVX0UNXranI
27 17 26 pm2.61dane KHLWHXVNXranI