Description: Subspace span of union is a subset of subspace join. (Contributed by NM, 6-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | djhspss.h | |
|
djhspss.u | |
||
djhspss.v | |
||
djhspss.n | |
||
djhspss.j | |
||
djhspss.k | |
||
djhspss.x | |
||
djhspss.y | |
||
Assertion | djhspss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | djhspss.h | |
|
2 | djhspss.u | |
|
3 | djhspss.v | |
|
4 | djhspss.n | |
|
5 | djhspss.j | |
|
6 | djhspss.k | |
|
7 | djhspss.x | |
|
8 | djhspss.y | |
|
9 | eqid | |
|
10 | 7 8 | unssd | |
11 | 1 2 9 3 4 6 10 | dochspss | |
12 | 1 2 3 9 5 | djhval2 | |
13 | 6 7 8 12 | syl3anc | |
14 | 11 13 | sseqtrrd | |