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∈Cℋ
spanunsn.2 ⊢B∈ℋ
Assertion spanunsni ⊢span⁡A∪B=span⁡A∪projℎ⁡⊥⁡A⁡B

Proof

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