Theorem shsval3i

Description: An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shlesb1.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	shlesb1.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shsval3i	$$⊢A{+}_{\mathscr{H}}B=\mathrm{span}\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		shlesb1.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shlesb1.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3	1 2	shsval2i	$$⊢A{+}_{\mathscr{H}}B=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
4	1	shssii	$$⊢A\subseteq \mathscr{H}$$
5	2	shssii	$$⊢B\subseteq \mathscr{H}$$
6	4 5	unssi	$$⊢A\cup B\subseteq \mathscr{H}$$
7		spanval	$$⊢A\cup B\subseteq \mathscr{H}\to \mathrm{span}\left(A\cup B\right)=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
8	6 7	ax-mp	$$⊢\mathrm{span}\left(A\cup B\right)=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
9	3 8	eqtr4i	$$⊢A{+}_{\mathscr{H}}B=\mathrm{span}\left(A\cup B\right)$$