Description: The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | spansnj.1 | |
|
spansnj.2 | |
||
Assertion | spansnji | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spansnj.1 | |
|
2 | spansnj.2 | |
|
3 | 1 | chshii | |
4 | 2 | spansnchi | |
5 | 4 | chshii | |
6 | 3 5 | shjshsi | |
7 | 1 | chssii | |
8 | 1 | choccli | |
9 | 8 2 | pjhclii | |
10 | snssi | |
|
11 | 9 10 | ax-mp | |
12 | 7 11 | spanuni | |
13 | spanid | |
|
14 | 3 13 | ax-mp | |
15 | 14 | oveq1i | |
16 | 7 2 | spansnpji | |
17 | 9 | spansnchi | |
18 | 1 17 | osumi | |
19 | 16 18 | ax-mp | |
20 | 12 15 19 | 3eqtrri | |
21 | 1 2 | spanunsni | |
22 | 20 21 | eqtr4i | |
23 | snssi | |
|
24 | 2 23 | ax-mp | |
25 | 7 24 | spanuni | |
26 | 14 | oveq1i | |
27 | 22 25 26 | 3eqtrri | |
28 | 1 17 | chjcli | |
29 | 27 28 | eqeltri | |
30 | 29 | ococi | |
31 | 6 30 | eqtr2i | |