# Metamath Proof Explorer

## 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}}_{ℋ}$
spanunsn.2 ${⊢}{B}\in ℋ$
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}}_{ℋ}$
2 spanunsn.2 ${⊢}{B}\in ℋ$
3 1 chshii ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
4 snssi ${⊢}{B}\in ℋ\to \left\{{B}\right\}\subseteq ℋ$
5 spancl ${⊢}\left\{{B}\right\}\subseteq ℋ\to \mathrm{span}\left(\left\{{B}\right\}\right)\in {\mathbf{S}}_{ℋ}$
6 2 4 5 mp2b ${⊢}\mathrm{span}\left(\left\{{B}\right\}\right)\in {\mathbf{S}}_{ℋ}$
7 3 6 shseli ${⊢}{x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{span}\left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{x}={y}{+}_{ℎ}{z}$
8 2 elspansni ${⊢}{z}\in \mathrm{span}\left(\left\{{B}\right\}\right)↔\exists {w}\in ℂ\phantom{\rule{.4em}{0ex}}{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}}_{ℋ}\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}}_{ℋ}\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}}_{ℋ}\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}}_{ℋ}$
16 15 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ$
17 spansnmul ${⊢}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\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 ℋ$
23 ax-hvdistr1 ${⊢}\left({w}\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\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 ℋ$
29 hvmulcl ${⊢}\left({w}\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\right)\to {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ$
30 22 29 mpan2 ${⊢}{w}\in ℂ\to {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ$
31 hvmulcl ${⊢}\left({w}\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\right)\to {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ$
32 16 31 mpan2 ${⊢}{w}\in ℂ\to {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ$
33 30 32 jca ${⊢}{w}\in ℂ\to \left({w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\right)$
34 ax-hvass ${⊢}\left({y}\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\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)$
35 34 3expb ${⊢}\left({y}\in ℋ\wedge \left({w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\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}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}{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}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{+}_{ℎ}\left({w}{\cdot }_{ℎ}{B}\right)={v}{+}_{ℎ}{u}$
40 snssi ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\to \left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\subseteq ℋ$
41 spancl ${⊢}\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\subseteq ℋ\to \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\in {\mathbf{S}}_{ℋ}$
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}}_{ℋ}$
43 3 42 shseli ${⊢}{y}{+}_{ℎ}\left({w}{\cdot }_{ℎ}{B}\right)\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\right)↔\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}{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}{+}_{ℋ}\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}↔{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}{+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\right)↔{y}{+}_{ℎ}\left({w}{\cdot }_{ℎ}{B}\right)\in \left({A}{+}_{ℋ}\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}{+}_{ℋ}\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}{+}_{ℋ}\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}{+}_{ℋ}\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}{+}_{ℋ}\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 ℂ\phantom{\rule{.4em}{0ex}}{z}={w}{\cdot }_{ℎ}{B}\to \left({x}={y}{+}_{ℎ}{z}\to {x}\in \left({A}{+}_{ℋ}\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}{+}_{ℋ}\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)\phantom{\rule{.4em}{0ex}}{x}={y}{+}_{ℎ}{z}\to {x}\in \left({A}{+}_{ℋ}\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}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{span}\left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{x}={y}{+}_{ℎ}{z}\to {x}\in \left({A}{+}_{ℋ}\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}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)\to {x}\in \left({A}{+}_{ℋ}\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}{+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\right)↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}{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)↔\exists {w}\in ℂ\phantom{\rule{.4em}{0ex}}{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}}_{ℋ}\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}}_{ℋ}\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}}_{ℋ}\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 ℋ\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 ℋ\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 ℋ\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 ℋ\right)\to \left(-{w}\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ$
76 59 22 75 sylancl ${⊢}{w}\in ℂ\to \left(-{w}\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ$
77 ax-hvcom ${⊢}\left({w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\wedge \left(-{w}\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\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 ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\right)\to {y}{+}_{ℎ}\left({w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right)\in ℋ$
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 ℋ$
84 hvaddid2 ${⊢}{y}{+}_{ℎ}\left({w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right)\in ℋ\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 ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\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 ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\right)$
88 28 32 anim12i ${⊢}\left({y}\in {A}\wedge {w}\in ℂ\right)\to \left({y}\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\right)$
89 hvadd4 ${⊢}\left(\left(\left(-{w}\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({A}\right)\left({B}\right)\in ℋ\right)\wedge \left({y}\in ℋ\wedge {w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\in ℋ\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}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{span}\left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{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}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{span}\left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{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}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)↔\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{span}\left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{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}{+}_{ℋ}\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}↔{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}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)↔{y}{+}_{ℎ}\left({w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right)\in \left({A}{+}_{ℋ}\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}{+}_{ℋ}\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}{+}_{ℋ}\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}{+}_{ℋ}\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}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)\right)\right)\right)$
105 104 rexlimdv ${⊢}{y}\in {A}\to \left(\exists {w}\in ℂ\phantom{\rule{.4em}{0ex}}{z}={w}{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\to \left({x}={y}{+}_{ℎ}{z}\to {x}\in \left({A}{+}_{ℋ}\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}{+}_{ℋ}\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)\phantom{\rule{.4em}{0ex}}{x}={y}{+}_{ℎ}{z}\to {x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)\right)$
108 107 rexlimiv ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}{x}={y}{+}_{ℎ}{z}\to {x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)$
109 57 108 sylbi ${⊢}{x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\right)\to {x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)$
110 56 109 impbii ${⊢}{x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)\right)↔{x}\in \left({A}{+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)\right)$
111 110 eqriv ${⊢}{A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)={A}{+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)$
112 1 chssii ${⊢}{A}\subseteq ℋ$
113 2 4 ax-mp ${⊢}\left\{{B}\right\}\subseteq ℋ$
114 112 113 spanuni ${⊢}\mathrm{span}\left({A}\cup \left\{{B}\right\}\right)=\mathrm{span}\left({A}\right){+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)$
115 spanid ${⊢}{A}\in {\mathbf{S}}_{ℋ}\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){+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)={A}{+}_{ℋ}\mathrm{span}\left(\left\{{B}\right\}\right)$
118 114 117 eqtri ${⊢}\mathrm{span}\left({A}\cup \left\{{B}\right\}\right)={A}{+}_{ℋ}\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 ℋ$
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){+}_{ℋ}\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){+}_{ℋ}\mathrm{span}\left(\left\{{\mathrm{proj}}_{ℎ}\left(\perp \left({A}\right)\right)\left({B}\right)\right\}\right)={A}{+}_{ℋ}\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}{+}_{ℋ}\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)$