Theorem spanun

Description: The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	spanun	$$⊢\left(A\subseteq \mathscr{H}\wedge B\subseteq \mathscr{H}\right)\to \mathrm{span}\left(A\cup B\right)=\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		uneq1	$$⊢A=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to A\cup B=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup B$$
2	1	fveq2d	$$⊢A=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to \mathrm{span}\left(A\cup B\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup B\right)$$
3		fveq2	$$⊢A=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to \mathrm{span}\left(A\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right)$$
4	3	oveq1d	$$⊢A=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to \mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)$$
5	2 4	eqeq12d	$$⊢A=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to \left(\mathrm{span}\left(A\cup B\right)=\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)\leftrightarrow \mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup B\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)\right)$$
6		uneq2	$$⊢B=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup B=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)$$
7	6	fveq2d	$$⊢B=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to \mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup B\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)$$
8		fveq2	$$⊢B=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to \mathrm{span}\left(B\right)=\mathrm{span}\left(if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)$$
9	8	oveq2d	$$⊢B=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to \mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)$$
10	7 9	eqeq12d	$$⊢B=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to \left(\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup B\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)\leftrightarrow \mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)\right)$$
11		sseq1	$$⊢A=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to \left(A\subseteq \mathscr{H}\leftrightarrow if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\subseteq \mathscr{H}\right)$$
12		sseq1	$$⊢\mathscr{H}=if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\to \left(\mathscr{H}\subseteq \mathscr{H}\leftrightarrow if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\subseteq \mathscr{H}\right)$$
13		ssid	$$⊢\mathscr{H}\subseteq \mathscr{H}$$
14	11 12 13	elimhyp	$$⊢if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\subseteq \mathscr{H}$$
15		sseq1	$$⊢B=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to \left(B\subseteq \mathscr{H}\leftrightarrow if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\subseteq \mathscr{H}\right)$$
16		sseq1	$$⊢\mathscr{H}=if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\to \left(\mathscr{H}\subseteq \mathscr{H}\leftrightarrow if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\subseteq \mathscr{H}\right)$$
17	15 16 13	elimhyp	$$⊢if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\subseteq \mathscr{H}$$
18	14 17	spanuni	$$⊢\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\cup if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)=\mathrm{span}\left(if\left(A\subseteq \mathscr{H},A,\mathscr{H}\right)\right){+}_{\mathscr{H}}\mathrm{span}\left(if\left(B\subseteq \mathscr{H},B,\mathscr{H}\right)\right)$$
19	5 10 18	dedth2h	$$⊢\left(A\subseteq \mathscr{H}\wedge B\subseteq \mathscr{H}\right)\to \mathrm{span}\left(A\cup B\right)=\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(B\right)$$