Description: The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | spansnj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 | |
|
2 | oveq1 | |
|
3 | 1 2 | eqeq12d | |
4 | sneq | |
|
5 | 4 | fveq2d | |
6 | 5 | oveq2d | |
7 | 5 | oveq2d | |
8 | 6 7 | eqeq12d | |
9 | ifchhv | |
|
10 | ifhvhv0 | |
|
11 | 9 10 | spansnji | |
12 | 3 8 11 | dedth2h | |