Description: The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihlsprn.h | |
|
dihlsprn.u | |
||
dihlsprn.v | |
||
dihlsprn.n | |
||
dihlsprn.i | |
||
Assertion | dihlsprn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihlsprn.h | |
|
2 | dihlsprn.u | |
|
3 | dihlsprn.v | |
|
4 | dihlsprn.n | |
|
5 | dihlsprn.i | |
|
6 | simpr | |
|
7 | 6 | sneqd | |
8 | 7 | fveq2d | |
9 | simpll | |
|
10 | 1 2 9 | dvhlmod | |
11 | eqid | |
|
12 | 11 4 | lspsn0 | |
13 | 10 12 | syl | |
14 | 8 13 | eqtrd | |
15 | 1 5 2 11 | dih0rn | |
16 | 15 | ad2antrr | |
17 | 14 16 | eqeltrd | |
18 | simpll | |
|
19 | 1 2 18 | dvhlmod | |
20 | simplr | |
|
21 | simpr | |
|
22 | eqid | |
|
23 | 3 4 11 22 | lsatlspsn2 | |
24 | 19 20 21 23 | syl3anc | |
25 | 1 2 5 22 | dih1dimat | |
26 | 18 24 25 | syl2anc | |
27 | 17 26 | pm2.61dane | |