Metamath Proof Explorer


Theorem spansnji

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 AC
spansnj.2 B
Assertion spansnji A+spanB=AspanB

Proof

Step Hyp Ref Expression
1 spansnj.1 AC
2 spansnj.2 B
3 1 chshii AS
4 2 spansnchi spanBC
5 4 chshii spanBS
6 3 5 shjshsi AspanB=A+spanB
7 1 chssii A
8 1 choccli AC
9 8 2 pjhclii projAB
10 snssi projABprojAB
11 9 10 ax-mp projAB
12 7 11 spanuni spanAprojAB=spanA+spanprojAB
13 spanid ASspanA=A
14 3 13 ax-mp spanA=A
15 14 oveq1i spanA+spanprojAB=A+spanprojAB
16 7 2 spansnpji AspanprojAB
17 9 spansnchi spanprojABC
18 1 17 osumi AspanprojABA+spanprojAB=AspanprojAB
19 16 18 ax-mp A+spanprojAB=AspanprojAB
20 12 15 19 3eqtrri AspanprojAB=spanAprojAB
21 1 2 spanunsni spanAB=spanAprojAB
22 20 21 eqtr4i AspanprojAB=spanAB
23 snssi BB
24 2 23 ax-mp B
25 7 24 spanuni spanAB=spanA+spanB
26 14 oveq1i spanA+spanB=A+spanB
27 22 25 26 3eqtrri A+spanB=AspanprojAB
28 1 17 chjcli AspanprojABC
29 27 28 eqeltri A+spanBC
30 29 ococi A+spanB=A+spanB
31 6 30 eqtr2i A+spanB=AspanB