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	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathscr{H}\right)\to A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
2		oveq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
3	1 2	eqeq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)$$
4		sneq	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \left\{B\right\}=\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}$$
5	4	fveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \mathrm{span}\left(\left\{B\right\}\right)=\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)$$
6	5	oveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)$$
7	5	oveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)$$
8	6 7	eqeq12d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)\right)$$
9		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10		ifhvhv0	$$⊢if\left(B\in \mathscr{H},B,0_{ℎ}\right)\in \mathscr{H}$$
11	9 10	spansnji	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right\}\right)$$
12	3 8 11	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathscr{H}\right)\to A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$