Theorem spanunsni

Description: The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spanunsn.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	spanunsn.2	$$⊢B\in \mathscr{H}$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		spanunsn.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		spanunsn.2	$$⊢B\in \mathscr{H}$$
3	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
4		snssi	$$⊢B\in \mathscr{H}\to \left\{B\right\}\subseteq \mathscr{H}$$
5		spancl	$$⊢\left\{B\right\}\subseteq \mathscr{H}\to \mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
6	2 4 5	mp2b	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
7	3 6	shseli	$$⊢x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\leftrightarrow \exists y\in A\exists z\in \mathrm{span}\left(\left\{B\right\}\right)x=y{+}_{ℎ}z$$
8	2	elspansni	$$⊢z\in \mathrm{span}\left(\left\{B\right\}\right)\leftrightarrow \exists w\in ℂz=w{\cdot }_{ℎ}B$$
9	1 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A$$
10		shmulcl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A\right)\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A$$
11	3 9 10	mp3an13	$$⊢w\in ℂ\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A$$
12		shaddcl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in A\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\in A$$
13	11 12	syl3an3	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\in A$$
14	3 13	mp3an1	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\in A$$
15	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
16	15 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}$$
17		spansnmul	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\wedge w\in ℂ\right)\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
18	16 17	mpan	$$⊢w\in ℂ\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
19	18	adantl	$$⊢\left(y\in A\wedge w\in ℂ\right)\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
20	1 2	pjpji	$$⊢B={\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)$$
21	20	oveq2i	$$⊢w{\cdot }_{ℎ}B=w{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
22	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}$$
23		ax-hvdistr1	$$⊢\left(w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)\to w{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
24	22 16 23	mp3an23	$$⊢w\in ℂ\to w{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
25	21 24	syl5eq	$$⊢w\in ℂ\to w{\cdot }_{ℎ}B=\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
26	25	adantl	$$⊢\left(y\in A\wedge w\in ℂ\right)\to w{\cdot }_{ℎ}B=\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
27	26	oveq2d	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=y{+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
28	1	cheli	$$⊢y\in A\to y\in \mathscr{H}$$
29		hvmulcl	$$⊢\left(w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}$$
30	22 29	mpan2	$$⊢w\in ℂ\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}$$
31		hvmulcl	$$⊢\left(w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}$$
32	16 31	mpan2	$$⊢w\in ℂ\to w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}$$
33	30 32	jca	$$⊢w\in ℂ\to \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)$$
34		ax-hvass	$$⊢\left(y\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)\to \left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=y{+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
35	34	3expb	$$⊢\left(y\in \mathscr{H}\wedge \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)\right)\to \left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=y{+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
36	28 33 35	syl2an	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=y{+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
37	27 36	eqtr4d	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
38		rspceov	$$⊢\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\in A\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\wedge y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)\to \exists v\in A\exists u\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=v{+}_{ℎ}u$$
39	14 19 37 38	syl3anc	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \exists v\in A\exists u\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=v{+}_{ℎ}u$$
40		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}$$
41		spancl	$$⊢\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\subseteq \mathscr{H}\to \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
42	16 40 41	mp2b	$$⊢\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
43	3 42	shseli	$$⊢y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\leftrightarrow \exists v\in A\exists u\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=v{+}_{ℎ}u$$
44	39 43	sylibr	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
45		oveq2	$$⊢z=w{\cdot }_{ℎ}B\to y{+}_{ℎ}z=y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)$$
46	45	eqeq2d	$$⊢z=w{\cdot }_{ℎ}B\to \left(x=y{+}_{ℎ}z\leftrightarrow x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\right)$$
47	46	biimpa	$$⊢\left(z=w{\cdot }_{ℎ}B\wedge x=y{+}_{ℎ}z\right)\to x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)$$
48		eleq1	$$⊢x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\to \left(x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\leftrightarrow y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\right)$$
49	48	biimparc	$$⊢\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\wedge x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\right)\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
50	44 47 49	syl2an	$$⊢\left(\left(y\in A\wedge w\in ℂ\right)\wedge \left(z=w{\cdot }_{ℎ}B\wedge x=y{+}_{ℎ}z\right)\right)\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
51	50	exp43	$$⊢y\in A\to \left(w\in ℂ\to \left(z=w{\cdot }_{ℎ}B\to \left(x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\right)\right)\right)$$
52	51	rexlimdv	$$⊢y\in A\to \left(\exists w\in ℂz=w{\cdot }_{ℎ}B\to \left(x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\right)\right)$$
53	8 52	syl5bi	$$⊢y\in A\to \left(z\in \mathrm{span}\left(\left\{B\right\}\right)\to \left(x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\right)\right)$$
54	53	rexlimdv	$$⊢y\in A\to \left(\exists z\in \mathrm{span}\left(\left\{B\right\}\right)x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\right)$$
55	54	rexlimiv	$$⊢\exists y\in A\exists z\in \mathrm{span}\left(\left\{B\right\}\right)x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
56	7 55	sylbi	$$⊢x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
57	3 42	shseli	$$⊢x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\leftrightarrow \exists y\in A\exists z\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)x=y{+}_{ℎ}z$$
58	16	elspansni	$$⊢z\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\leftrightarrow \exists w\in ℂz=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)$$
59		negcl	$$⊢w\in ℂ\to -w\in ℂ$$
60		shmulcl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge -w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A\right)\to \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A$$
61	3 9 60	mp3an13	$$⊢-w\in ℂ\to \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A$$
62	59 61	syl	$$⊢w\in ℂ\to \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A$$
63		shaddcl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in A\wedge y\in A\right)\to \left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\in A$$
64	62 63	syl3an2	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge w\in ℂ\wedge y\in A\right)\to \left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\in A$$
65	3 64	mp3an1	$$⊢\left(w\in ℂ\wedge y\in A\right)\to \left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\in A$$
66	65	ancoms	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\in A$$
67		spansnmul	$$⊢\left(B\in \mathscr{H}\wedge w\in ℂ\right)\to w{\cdot }_{ℎ}B\in \mathrm{span}\left(\left\{B\right\}\right)$$
68	2 67	mpan	$$⊢w\in ℂ\to w{\cdot }_{ℎ}B\in \mathrm{span}\left(\left\{B\right\}\right)$$
69	68	adantl	$$⊢\left(y\in A\wedge w\in ℂ\right)\to w{\cdot }_{ℎ}B\in \mathrm{span}\left(\left\{B\right\}\right)$$
70		hvm1neg	$$⊢\left(w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)\to -1{\cdot }_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)=\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)$$
71	22 70	mpan2	$$⊢w\in ℂ\to -1{\cdot }_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)=\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)$$
72	71	oveq2d	$$⊢w\in ℂ\to \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right)=\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)$$
73		hvnegid	$$⊢w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\to \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right)=0_{ℎ}$$
74	30 73	syl	$$⊢w\in ℂ\to \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right)=0_{ℎ}$$
75		hvmulcl	$$⊢\left(-w\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)\to \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}$$
76	59 22 75	sylancl	$$⊢w\in ℂ\to \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}$$
77		ax-hvcom	$$⊢\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge \left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)\to \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)=\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)$$
78	30 76 77	syl2anc	$$⊢w\in ℂ\to \left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)=\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)$$
79	72 74 78	3eqtr3d	$$⊢w\in ℂ\to 0_{ℎ}=\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)$$
80	79	adantl	$$⊢\left(y\in A\wedge w\in ℂ\right)\to 0_{ℎ}=\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)$$
81	80	oveq1d	$$⊢\left(y\in A\wedge w\in ℂ\right)\to 0_{ℎ}{+}_{ℎ}\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
82		hvaddcl	$$⊢\left(y\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \mathscr{H}$$
83	28 32 82	syl2an	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \mathscr{H}$$
84		hvaddid2	$$⊢y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
85	83 84	syl	$$⊢\left(y\in A\wedge w\in ℂ\right)\to 0_{ℎ}{+}_{ℎ}\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
86	76 30	jca	$$⊢w\in ℂ\to \left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)$$
87	86	adantl	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)$$
88	28 32	anim12i	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \left(y\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)$$
89		hvadd4	$$⊢\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\in \mathscr{H}\right)\wedge \left(y\in \mathscr{H}\wedge w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\in \mathscr{H}\right)\right)\to \left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
90	87 88 89	syl2anc	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right)\right){+}_{ℎ}\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
91	81 85 90	3eqtr3d	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
92	26	oveq2d	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
93	91 92	eqtr4d	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)$$
94		rspceov	$$⊢\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\in A\wedge w{\cdot }_{ℎ}B\in \mathrm{span}\left(\left\{B\right\}\right)\wedge y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=\left(\left(\left(-w\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(A\right)\left(B\right)\right){+}_{ℎ}y\right){+}_{ℎ}\left(w{\cdot }_{ℎ}B\right)\right)\to \exists v\in A\exists u\in \mathrm{span}\left(\left\{B\right\}\right)y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=v{+}_{ℎ}u$$
95	66 69 93 94	syl3anc	$$⊢\left(y\in A\wedge w\in ℂ\right)\to \exists v\in A\exists u\in \mathrm{span}\left(\left\{B\right\}\right)y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=v{+}_{ℎ}u$$
96	3 6	shseli	$$⊢y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\leftrightarrow \exists v\in A\exists u\in \mathrm{span}\left(\left\{B\right\}\right)y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)=v{+}_{ℎ}u$$
97	95 96	sylibr	$$⊢\left(y\in A\wedge w\in ℂ\right)\to y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)$$
98		oveq2	$$⊢z=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\to y{+}_{ℎ}z=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
99	98	eqeq2d	$$⊢z=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\to \left(x=y{+}_{ℎ}z\leftrightarrow x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)$$
100	99	biimpa	$$⊢\left(z=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\wedge x=y{+}_{ℎ}z\right)\to x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)$$
101		eleq1	$$⊢x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\to \left(x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\leftrightarrow y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)$$
102	101	biimparc	$$⊢\left(y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\wedge x=y{+}_{ℎ}\left(w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right)\right)\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)$$
103	97 100 102	syl2an	$$⊢\left(\left(y\in A\wedge w\in ℂ\right)\wedge \left(z=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\wedge x=y{+}_{ℎ}z\right)\right)\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)$$
104	103	exp43	$$⊢y\in A\to \left(w\in ℂ\to \left(z=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\to \left(x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)\right)\right)$$
105	104	rexlimdv	$$⊢y\in A\to \left(\exists w\in ℂz=w{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\to \left(x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)\right)$$
106	58 105	syl5bi	$$⊢y\in A\to \left(z\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\to \left(x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)\right)$$
107	106	rexlimdv	$$⊢y\in A\to \left(\exists z\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\right)$$
108	107	rexlimiv	$$⊢\exists y\in A\exists z\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)x=y{+}_{ℎ}z\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)$$
109	57 108	sylbi	$$⊢x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)\to x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)$$
110	56 109	impbii	$$⊢x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)\right)\leftrightarrow x\in \left(A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)\right)$$
111	110	eqriv	$$⊢A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)=A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\right)$$
112	1	chssii	$$⊢A\subseteq \mathscr{H}$$
113	2 4	ax-mp	$$⊢\left\{B\right\}\subseteq \mathscr{H}$$
114	112 113	spanuni	$$⊢\mathrm{span}\left(A\cup \left\{B\right\}\right)=\mathrm{span}\left(A\right){+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
115		spanid	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(A\right)=A$$
116	3 115	ax-mp	$$⊢\mathrm{span}\left(A\right)=A$$
117	116	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)$$
118	114 117	eqtri	$$⊢\mathrm{span}\left(A\cup \left\{B\right\}\right)=A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{B\right\}\right)$$
119	16 40	ax-mp	$$⊢\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left(A\right)\right)\left(B\right)\right\}\subseteq \mathscr{H}$$
120	112 119	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)$$
121	116	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)$$
122	120 121	eqtri	$$⊢\mathrm{span}\left(A\cup \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)$$
123	111 118 122	3eqtr4i	$$⊢\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)$$