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 ⊢ 𝐴 ∈ Cℋ
spanunsn.2 ⊢ 𝐵 ∈ ℋ
Assertion spanunsni ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )

Proof

Step Hyp Ref Expression
1 spanunsn.1 ⊢ 𝐴 ∈ Cℋ
2 spanunsn.2 ⊢ 𝐵 ∈ ℋ
3 1 chshii ⊢ 𝐴 ∈ Sℋ
4 snssi ⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
5 spancl ⊢ ( { 𝐵 } ⊆ ℋ → ( span ‘ { 𝐵 } ) ∈ Sℋ )
6 2 4 5 mp2b ⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ
7 3 6 shseli ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { 𝐵 } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
8 2 elspansni ⊢ ( 𝑧 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑤 ∈ ℂ 𝑧 = ( 𝑤 ·ℎ 𝐵 ) )
9 1 2 pjclii ⊢ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ 𝐴
10 shmulcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ 𝐴 ) → ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 )
11 3 9 10 mp3an13 ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 )
12 shaddcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ∈ 𝐴 )
13 11 12 syl3an3 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ∈ 𝐴 )
14 3 13 mp3an1 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ∈ 𝐴 )
15 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
16 15 2 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ
17 spansnmul ⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ ∧ 𝑤 ∈ ℂ ) → ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
18 16 17 mpan ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
19 18 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
20 1 2 pjpji ⊢ 𝐵 = ( ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) )
21 20 oveq2i ⊢ ( 𝑤 ·ℎ 𝐵 ) = ( 𝑤 ·ℎ ( ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) )
22 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℋ
23 ax-hvdistr1 ⊢ ( ( 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ ) → ( 𝑤 ·ℎ ( ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
24 22 16 23 mp3an23 ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ ( ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
25 21 24 eqtrid ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ 𝐵 ) = ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
26 25 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑤 ·ℎ 𝐵 ) = ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
27 26 oveq2d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( 𝑦 +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
28 1 cheli ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
29 hvmulcl ⊢ ( ( 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℋ ) → ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ )
30 22 29 mpan2 ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ )
31 hvmulcl ⊢ ( ( 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ ) → ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ )
32 16 31 mpan2 ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ )
33 30 32 jca ⊢ ( 𝑤 ∈ ℂ → ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ ) )
34 ax-hvass ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ ) → ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( 𝑦 +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
35 34 3expb ⊢ ( ( 𝑦 ∈ ℋ ∧ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ ) ) → ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( 𝑦 +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
36 28 33 35 syl2an ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( 𝑦 +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
37 27 36 eqtr4d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
38 rspceov ⊢ ( ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ∈ 𝐴 ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ∧ ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( 𝑣 +ℎ 𝑢 ) )
39 14 19 37 38 syl3anc ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( 𝑣 +ℎ 𝑢 ) )
40 snssi ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ → { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ )
41 spancl ⊢ ( { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ → ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ∈ Sℋ )
42 16 40 41 mp2b ⊢ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ∈ Sℋ
43 3 42 shseli ⊢ ( ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( 𝑣 +ℎ 𝑢 ) )
44 39 43 sylibr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
45 oveq2 ⊢ ( 𝑧 = ( 𝑤 ·ℎ 𝐵 ) → ( 𝑦 +ℎ 𝑧 ) = ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) )
46 45 eqeq2d ⊢ ( 𝑧 = ( 𝑤 ·ℎ 𝐵 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ) )
47 46 biimpa ⊢ ( ( 𝑧 = ( 𝑤 ·ℎ 𝐵 ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) → 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) )
48 eleq1 ⊢ ( 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ↔ ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ) )
49 48 biimparc ⊢ ( ( ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ∧ 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
50 44 47 49 syl2an ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) ∧ ( 𝑧 = ( 𝑤 ·ℎ 𝐵 ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
51 50 exp43 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑤 ∈ ℂ → ( 𝑧 = ( 𝑤 ·ℎ 𝐵 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ) ) ) )
52 51 rexlimdv ⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑤 ∈ ℂ 𝑧 = ( 𝑤 ·ℎ 𝐵 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ) ) )
53 8 52 biimtrid ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ ( span ‘ { 𝐵 } ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ) ) )
54 53 rexlimdv ⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑧 ∈ ( span ‘ { 𝐵 } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ) )
55 54 rexlimiv ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { 𝐵 } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
56 7 55 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
57 3 42 shseli ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
58 16 elspansni ⊢ ( 𝑧 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ↔ ∃ 𝑤 ∈ ℂ 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) )
59 negcl ⊢ ( 𝑤 ∈ ℂ → - 𝑤 ∈ ℂ )
60 shmulcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ - 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ 𝐴 ) → ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 )
61 3 9 60 mp3an13 ⊢ ( - 𝑤 ∈ ℂ → ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 )
62 59 61 syl ⊢ ( 𝑤 ∈ ℂ → ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 )
63 shaddcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) ∈ 𝐴 )
64 62 63 syl3an2 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑤 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) ∈ 𝐴 )
65 3 64 mp3an1 ⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) ∈ 𝐴 )
66 65 ancoms ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) ∈ 𝐴 )
67 spansnmul ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑤 ∈ ℂ ) → ( 𝑤 ·ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) )
68 2 67 mpan ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 ·ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) )
69 68 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑤 ·ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) )
70 hvm1neg ⊢ ( ( 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℋ ) → ( - 1 ·ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) = ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) )
71 22 70 mpan2 ⊢ ( 𝑤 ∈ ℂ → ( - 1 ·ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) = ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) )
72 71 oveq2d ⊢ ( 𝑤 ∈ ℂ → ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( - 1 ·ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ) = ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) )
73 hvnegid ⊢ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ → ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( - 1 ·ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ) = 0ℎ )
74 30 73 syl ⊢ ( 𝑤 ∈ ℂ → ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( - 1 ·ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) ) = 0ℎ )
75 hvmulcl ⊢ ( ( - 𝑤 ∈ ℂ ∧ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℋ ) → ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ )
76 59 22 75 sylancl ⊢ ( 𝑤 ∈ ℂ → ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ )
77 ax-hvcom ⊢ ( ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ) → ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) = ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) )
78 30 76 77 syl2anc ⊢ ( 𝑤 ∈ ℂ → ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) = ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) )
79 72 74 78 3eqtr3d ⊢ ( 𝑤 ∈ ℂ → 0ℎ = ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) )
80 79 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → 0ℎ = ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) )
81 80 oveq1d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 0ℎ +ℎ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
82 hvaddcl ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ℋ )
83 28 32 82 syl2an ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ℋ )
84 hvaddlid ⊢ ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ℋ → ( 0ℎ +ℎ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
85 83 84 syl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 0ℎ +ℎ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
86 76 30 jca ⊢ ( 𝑤 ∈ ℂ → ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ) )
87 86 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ) )
88 28 32 anim12i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ ) )
89 hvadd4 ⊢ ( ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ∈ ℋ ) ∧ ( 𝑦 ∈ ℋ ∧ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∈ ℋ ) ) → ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
90 87 88 89 syl2anc ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) ) +ℎ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
91 81 85 90 3eqtr3d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
92 26 oveq2d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( 𝑤 ·ℎ 𝐵 ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( ( 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
93 91 92 eqtr4d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( 𝑤 ·ℎ 𝐵 ) ) )
94 rspceov ⊢ ( ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) ∈ 𝐴 ∧ ( 𝑤 ·ℎ 𝐵 ) ∈ ( span ‘ { 𝐵 } ) ∧ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( ( ( - 𝑤 ·ℎ ( ( projℎ ‘ 𝐴 ) ‘ 𝐵 ) ) +ℎ 𝑦 ) +ℎ ( 𝑤 ·ℎ 𝐵 ) ) ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ ( span ‘ { 𝐵 } ) ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( 𝑣 +ℎ 𝑢 ) )
95 66 69 93 94 syl3anc ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ ( span ‘ { 𝐵 } ) ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( 𝑣 +ℎ 𝑢 ) )
96 3 6 shseli ⊢ ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ ( span ‘ { 𝐵 } ) ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) = ( 𝑣 +ℎ 𝑢 ) )
97 95 96 sylibr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) → ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) )
98 oveq2 ⊢ ( 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) → ( 𝑦 +ℎ 𝑧 ) = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
99 98 eqeq2d ⊢ ( 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) )
100 99 biimpa ⊢ ( ( 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) → 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) )
101 eleq1 ⊢ ( 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ↔ ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) )
102 101 biimparc ⊢ ( ( ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ∧ 𝑥 = ( 𝑦 +ℎ ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ) ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) )
103 97 100 102 syl2an ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ ) ∧ ( 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) )
104 103 exp43 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑤 ∈ ℂ → ( 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) ) ) )
105 104 rexlimdv ⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑤 ∈ ℂ 𝑧 = ( 𝑤 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) ) )
106 58 105 biimtrid ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) ) )
107 106 rexlimdv ⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑧 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) )
108 107 rexlimiv ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) )
109 57 108 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) → 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) )
110 56 109 impbii ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ↔ 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
111 110 eqriv ⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
112 1 chssii ⊢ 𝐴 ⊆ ℋ
113 2 4 ax-mp ⊢ { 𝐵 } ⊆ ℋ
114 112 113 spanuni ⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { 𝐵 } ) )
115 spanid ⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 )
116 3 115 ax-mp ⊢ ( span ‘ 𝐴 ) = 𝐴
117 116 oveq1i ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) )
118 114 117 eqtri ⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) )
119 16 40 ax-mp ⊢ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ
120 112 119 spanuni ⊢ ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
121 116 oveq1i ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
122 120 121 eqtri ⊢ ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
123 111 118 122 3eqtr4i ⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )