Metamath Proof Explorer


Theorem spansnj

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 ACBA+spanB=AspanB

Proof

Step Hyp Ref Expression
1 oveq1 A=ifACAA+spanB=ifACA+spanB
2 oveq1 A=ifACAAspanB=ifACAspanB
3 1 2 eqeq12d A=ifACAA+spanB=AspanBifACA+spanB=ifACAspanB
4 sneq B=ifBB0B=ifBB0
5 4 fveq2d B=ifBB0spanB=spanifBB0
6 5 oveq2d B=ifBB0ifACA+spanB=ifACA+spanifBB0
7 5 oveq2d B=ifBB0ifACAspanB=ifACAspanifBB0
8 6 7 eqeq12d B=ifBB0ifACA+spanB=ifACAspanBifACA+spanifBB0=ifACAspanifBB0
9 ifchhv ifACAC
10 ifhvhv0 ifBB0
11 9 10 spansnji ifACA+spanifBB0=ifACAspanifBB0
12 3 8 11 dedth2h ACBA+spanB=AspanB