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	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	spansnj.2	$$⊢B\in \mathscr{H}$$
Assertion	spansnji	$$⊢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		spansnj.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		spansnj.2	$$⊢B\in \mathscr{H}$$
3	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
4	2	spansnchi	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	chshii	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
6	3 5	shjshsi	$$⊢A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=\perp \left(\perp \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)$$
7	1	chssii	$$⊢A\subseteq \mathscr{H}$$
8	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
9	8 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}$$
10		snssi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\to \left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\subseteq \mathscr{H}$$
11	9 10	ax-mp	$$⊢\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\subseteq \mathscr{H}$$
12	7 11	spanuni	$$⊢\mathrm{span}\left(A\cup \left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)=\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
13		spanid	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(A\right)=A$$
14	3 13	ax-mp	$$⊢\mathrm{span}\left(A\right)=A$$
15	14	oveq1i	$$⊢\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)=A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
16	7 2	spansnpji	$$⊢A\subseteq \perp \left(\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
17	9	spansnchi	$$⊢\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
18	1 17	osumi	$$⊢A\subseteq \perp \left(\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\to A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
19	16 18	ax-mp	$$⊢A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
20	12 15 19	3eqtrri	$$⊢A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)=\mathrm{span}\left(A\cup \left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
21	1 2	spanunsni	$$⊢\mathrm{span}\left(A\cup \left\{B\right\}\right)=\mathrm{span}\left(A\cup \left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
22	20 21	eqtr4i	$$⊢A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)=\mathrm{span}\left(A\cup \left\{B\right\}\right)$$
23		snssi	$$⊢B\in \mathscr{H}\to \left\{B\right\}\subseteq \mathscr{H}$$
24	2 23	ax-mp	$$⊢\left\{B\right\}\subseteq \mathscr{H}$$
25	7 24	spanuni	$$⊢\mathrm{span}\left(A\cup \left\{B\right\}\right)=\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
26	14	oveq1i	$$⊢\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
27	22 25 26	3eqtrri	$$⊢A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
28	1 17	chjcli	$$⊢A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
29	27 28	eqeltri	$$⊢A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
30	29	ococi	$$⊢\perp \left(\perp \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)=A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
31	6 30	eqtr2i	$$⊢A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$