Step | Hyp | Ref
| Expression |
1 | | spanunsn.1 |
. . . . . . 7
⊢ 𝐴 ∈
Cℋ |
2 | 1 | chshii 29162 |
. . . . . 6
⊢ 𝐴 ∈
Sℋ |
3 | | spanunsn.2 |
. . . . . . 7
⊢ 𝐵 ∈ ℋ |
4 | | snssi 4696 |
. . . . . . 7
⊢ (𝐵 ∈ ℋ → {𝐵} ⊆
ℋ) |
5 | | spancl 29271 |
. . . . . . 7
⊢ ({𝐵} ⊆ ℋ →
(span‘{𝐵}) ∈
Sℋ ) |
6 | 3, 4, 5 | mp2b 10 |
. . . . . 6
⊢
(span‘{𝐵})
∈ Sℋ |
7 | 2, 6 | shseli 29251 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 +ℋ (span‘{𝐵})) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ (span‘{𝐵})𝑥 = (𝑦 +ℎ 𝑧)) |
8 | 3 | elspansni 29493 |
. . . . . . . 8
⊢ (𝑧 ∈ (span‘{𝐵}) ↔ ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝐵)) |
9 | 1, 3 | pjclii 29356 |
. . . . . . . . . . . . . . . 16
⊢
((projℎ‘𝐴)‘𝐵) ∈ 𝐴 |
10 | | shmulcl 29153 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Sℋ ∧ 𝑤 ∈ ℂ ∧
((projℎ‘𝐴)‘𝐵) ∈ 𝐴) → (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ 𝐴) |
11 | 2, 9, 10 | mp3an13 1453 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ 𝐴) |
12 | | shaddcl 29152 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Sℋ ∧ 𝑦 ∈ 𝐴 ∧ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ 𝐴) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) ∈ 𝐴) |
13 | 11, 12 | syl3an3 1166 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Sℋ ∧ 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) ∈ 𝐴) |
14 | 2, 13 | mp3an1 1449 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) ∈ 𝐴) |
15 | 1 | choccli 29242 |
. . . . . . . . . . . . . . . 16
⊢
(⊥‘𝐴)
∈ Cℋ |
16 | 15, 3 | pjhclii 29357 |
. . . . . . . . . . . . . . 15
⊢
((projℎ‘(⊥‘𝐴))‘𝐵) ∈ ℋ |
17 | | spansnmul 29499 |
. . . . . . . . . . . . . . 15
⊢
((((projℎ‘(⊥‘𝐴))‘𝐵) ∈ ℋ ∧ 𝑤 ∈ ℂ) → (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
18 | 16, 17 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
19 | 18 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
20 | 1, 3 | pjpji 29359 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 =
(((projℎ‘𝐴)‘𝐵) +ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) |
21 | 20 | oveq2i 7181 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤
·ℎ 𝐵) = (𝑤 ·ℎ
(((projℎ‘𝐴)‘𝐵) +ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) |
22 | 1, 3 | pjhclii 29357 |
. . . . . . . . . . . . . . . . . 18
⊢
((projℎ‘𝐴)‘𝐵) ∈ ℋ |
23 | | ax-hvdistr1 28943 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℂ ∧
((projℎ‘𝐴)‘𝐵) ∈ ℋ ∧
((projℎ‘(⊥‘𝐴))‘𝐵) ∈ ℋ) → (𝑤 ·ℎ
(((projℎ‘𝐴)‘𝐵) +ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
24 | 22, 16, 23 | mp3an23 1454 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ (((projℎ‘𝐴)‘𝐵) +ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
25 | 21, 24 | syl5eq 2785 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ 𝐵) = ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
26 | 25 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑤 ·ℎ 𝐵) = ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
27 | 26 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ 𝐵)) = (𝑦 +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
28 | 1 | cheli 29167 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ) |
29 | | hvmulcl 28948 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℂ ∧
((projℎ‘𝐴)‘𝐵) ∈ ℋ) → (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ ℋ) |
30 | 22, 29 | mpan2 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ) |
31 | | hvmulcl 28948 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℂ ∧
((projℎ‘(⊥‘𝐴))‘𝐵) ∈ ℋ) → (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ) |
32 | 16, 31 | mpan2 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ) |
33 | 30, 32 | jca 515 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ → ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)) |
34 | | ax-hvass 28937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℋ ∧ (𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ) → ((𝑦 +ℎ (𝑤
·ℎ ((projℎ‘𝐴)‘𝐵))) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (𝑦 +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
35 | 34 | 3expb 1121 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)) → ((𝑦 +ℎ (𝑤
·ℎ ((projℎ‘𝐴)‘𝐵))) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (𝑦 +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
36 | 28, 33, 35 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → ((𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (𝑦 +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
37 | 27, 36 | eqtr4d 2776 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ 𝐵)) = ((𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
38 | | rspceov 7217 |
. . . . . . . . . . . . 13
⊢ (((𝑦 +ℎ (𝑤
·ℎ ((projℎ‘𝐴)‘𝐵))) ∈ 𝐴 ∧ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}) ∧ (𝑦 +ℎ (𝑤 ·ℎ 𝐵)) = ((𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) → ∃𝑣 ∈ 𝐴 ∃𝑢 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})(𝑦 +ℎ (𝑤 ·ℎ 𝐵)) = (𝑣 +ℎ 𝑢)) |
39 | 14, 19, 37, 38 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → ∃𝑣 ∈ 𝐴 ∃𝑢 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})(𝑦 +ℎ (𝑤 ·ℎ 𝐵)) = (𝑣 +ℎ 𝑢)) |
40 | | snssi 4696 |
. . . . . . . . . . . . . 14
⊢
(((projℎ‘(⊥‘𝐴))‘𝐵) ∈ ℋ →
{((projℎ‘(⊥‘𝐴))‘𝐵)} ⊆ ℋ) |
41 | | spancl 29271 |
. . . . . . . . . . . . . 14
⊢
({((projℎ‘(⊥‘𝐴))‘𝐵)} ⊆ ℋ →
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}) ∈ Sℋ
) |
42 | 16, 40, 41 | mp2b 10 |
. . . . . . . . . . . . 13
⊢
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}) ∈
Sℋ |
43 | 2, 42 | shseli 29251 |
. . . . . . . . . . . 12
⊢ ((𝑦 +ℎ (𝑤
·ℎ 𝐵)) ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) ↔ ∃𝑣 ∈ 𝐴 ∃𝑢 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})(𝑦 +ℎ (𝑤 ·ℎ 𝐵)) = (𝑣 +ℎ 𝑢)) |
44 | 39, 43 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ 𝐵)) ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))) |
45 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑤 ·ℎ 𝐵) → (𝑦 +ℎ 𝑧) = (𝑦 +ℎ (𝑤 ·ℎ 𝐵))) |
46 | 45 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 ·ℎ 𝐵) → (𝑥 = (𝑦 +ℎ 𝑧) ↔ 𝑥 = (𝑦 +ℎ (𝑤 ·ℎ 𝐵)))) |
47 | 46 | biimpa 480 |
. . . . . . . . . . 11
⊢ ((𝑧 = (𝑤 ·ℎ 𝐵) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) → 𝑥 = (𝑦 +ℎ (𝑤 ·ℎ 𝐵))) |
48 | | eleq1 2820 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 +ℎ (𝑤 ·ℎ 𝐵)) → (𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) ↔ (𝑦 +ℎ (𝑤 ·ℎ 𝐵)) ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})))) |
49 | 48 | biimparc 483 |
. . . . . . . . . . 11
⊢ (((𝑦 +ℎ (𝑤
·ℎ 𝐵)) ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) ∧ 𝑥 = (𝑦 +ℎ (𝑤 ·ℎ 𝐵))) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))) |
50 | 44, 47, 49 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) ∧ (𝑧 = (𝑤 ·ℎ 𝐵) ∧ 𝑥 = (𝑦 +ℎ 𝑧))) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))) |
51 | 50 | exp43 440 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → (𝑤 ∈ ℂ → (𝑧 = (𝑤 ·ℎ 𝐵) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})))))) |
52 | 51 | rexlimdv 3193 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝐵) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))))) |
53 | 8, 52 | syl5bi 245 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (𝑧 ∈ (span‘{𝐵}) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))))) |
54 | 53 | rexlimdv 3193 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → (∃𝑧 ∈ (span‘{𝐵})𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})))) |
55 | 54 | rexlimiv 3190 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 ∃𝑧 ∈ (span‘{𝐵})𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))) |
56 | 7, 55 | sylbi 220 |
. . . 4
⊢ (𝑥 ∈ (𝐴 +ℋ (span‘{𝐵})) → 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))) |
57 | 2, 42 | shseli 29251 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})𝑥 = (𝑦 +ℎ 𝑧)) |
58 | 16 | elspansni 29493 |
. . . . . . . 8
⊢ (𝑧 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}) ↔ ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) |
59 | | negcl 10964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → -𝑤 ∈
ℂ) |
60 | | shmulcl 29153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Sℋ ∧ -𝑤 ∈ ℂ ∧
((projℎ‘𝐴)‘𝐵) ∈ 𝐴) → (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ 𝐴) |
61 | 2, 9, 60 | mp3an13 1453 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝑤 ∈ ℂ → (-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ 𝐴) |
62 | 59, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ → (-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ 𝐴) |
63 | | shaddcl 29152 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Sℋ ∧ (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) ∈ 𝐴) |
64 | 62, 63 | syl3an2 1165 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Sℋ ∧ 𝑤 ∈ ℂ ∧ 𝑦 ∈ 𝐴) → ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) ∈ 𝐴) |
65 | 2, 64 | mp3an1 1449 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℂ ∧ 𝑦 ∈ 𝐴) → ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) ∈ 𝐴) |
66 | 65 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) ∈ 𝐴) |
67 | | spansnmul 29499 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℋ ∧ 𝑤 ∈ ℂ) → (𝑤
·ℎ 𝐵) ∈ (span‘{𝐵})) |
68 | 3, 67 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ → (𝑤
·ℎ 𝐵) ∈ (span‘{𝐵})) |
69 | 68 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑤 ·ℎ 𝐵) ∈ (span‘{𝐵})) |
70 | | hvm1neg 28967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℂ ∧
((projℎ‘𝐴)‘𝐵) ∈ ℋ) → (-1
·ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) = (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) |
71 | 22, 70 | mpan2 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ℂ → (-1
·ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) = (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) |
72 | 71 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ → ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (-1
·ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) = ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) |
73 | | hvnegid 28962 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ → ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (-1
·ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) =
0ℎ) |
74 | 30, 73 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ → ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (-1
·ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) =
0ℎ) |
75 | | hvmulcl 28948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((-𝑤 ∈ ℂ ∧
((projℎ‘𝐴)‘𝐵) ∈ ℋ) → (-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ) |
76 | 59, 22, 75 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ℂ → (-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ) |
77 | | ax-hvcom 28936 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ ℋ) → ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) = ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) |
78 | 30, 76, 77 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ → ((𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) = ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) |
79 | 72, 74, 78 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ →
0ℎ = ((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) |
80 | 79 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → 0ℎ
= ((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)))) |
81 | 80 | oveq1d 7185 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (0ℎ
+ℎ (𝑦
+ℎ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) +ℎ (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
82 | | hvaddcl 28947 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ) → (𝑦 +ℎ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ ℋ) |
83 | 28, 32, 82 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ ℋ) |
84 | | hvaddid2 28958 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 +ℎ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ ℋ →
(0ℎ +ℎ (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (0ℎ
+ℎ (𝑦
+ℎ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
86 | 76, 30 | jca 515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → ((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ ℋ)) |
87 | 86 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → ((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ ℋ)) |
88 | 28, 32 | anim12i 616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)) |
89 | | hvadd4 28971 |
. . . . . . . . . . . . . . . 16
⊢
((((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) ∈ ℋ) ∧ (𝑦 ∈ ℋ ∧ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)) → (((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) +ℎ (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
90 | 87, 88, 89 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵))) +ℎ (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
91 | 81, 85, 90 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
92 | 26 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ (𝑤 ·ℎ 𝐵)) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ ((𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
93 | 91, 92 | eqtr4d 2776 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ (𝑤 ·ℎ 𝐵))) |
94 | | rspceov 7217 |
. . . . . . . . . . . . 13
⊢
((((-𝑤
·ℎ ((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) ∈ 𝐴 ∧ (𝑤 ·ℎ 𝐵) ∈ (span‘{𝐵}) ∧ (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (((-𝑤 ·ℎ
((projℎ‘𝐴)‘𝐵)) +ℎ 𝑦) +ℎ (𝑤 ·ℎ 𝐵))) → ∃𝑣 ∈ 𝐴 ∃𝑢 ∈ (span‘{𝐵})(𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (𝑣 +ℎ 𝑢)) |
95 | 66, 69, 93, 94 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → ∃𝑣 ∈ 𝐴 ∃𝑢 ∈ (span‘{𝐵})(𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (𝑣 +ℎ 𝑢)) |
96 | 2, 6 | shseli 29251 |
. . . . . . . . . . . 12
⊢ ((𝑦 +ℎ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 +ℋ (span‘{𝐵})) ↔ ∃𝑣 ∈ 𝐴 ∃𝑢 ∈ (span‘{𝐵})(𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) = (𝑣 +ℎ 𝑢)) |
97 | 95, 96 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) → (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 +ℋ (span‘{𝐵}))) |
98 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) → (𝑦 +ℎ 𝑧) = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
99 | 98 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) → (𝑥 = (𝑦 +ℎ 𝑧) ↔ 𝑥 = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))))) |
100 | 99 | biimpa 480 |
. . . . . . . . . . 11
⊢ ((𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) → 𝑥 = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) |
101 | | eleq1 2820 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) → (𝑥 ∈ (𝐴 +ℋ (span‘{𝐵})) ↔ (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 +ℋ (span‘{𝐵})))) |
102 | 101 | biimparc 483 |
. . . . . . . . . . 11
⊢ (((𝑦 +ℎ (𝑤
·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 +ℋ (span‘{𝐵})) ∧ 𝑥 = (𝑦 +ℎ (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)))) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵}))) |
103 | 97, 100, 102 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐴 ∧ 𝑤 ∈ ℂ) ∧ (𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) ∧ 𝑥 = (𝑦 +ℎ 𝑧))) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵}))) |
104 | 103 | exp43 440 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → (𝑤 ∈ ℂ → (𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵})))))) |
105 | 104 | rexlimdv 3193 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ
((projℎ‘(⊥‘𝐴))‘𝐵)) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵}))))) |
106 | 58, 105 | syl5bi 245 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (𝑧 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵}))))) |
107 | 106 | rexlimdv 3193 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → (∃𝑧 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵})))) |
108 | 107 | rexlimiv 3190 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 ∃𝑧 ∈
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵}))) |
109 | 57, 108 | sylbi 220 |
. . . 4
⊢ (𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) → 𝑥 ∈ (𝐴 +ℋ (span‘{𝐵}))) |
110 | 56, 109 | impbii 212 |
. . 3
⊢ (𝑥 ∈ (𝐴 +ℋ (span‘{𝐵})) ↔ 𝑥 ∈ (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))) |
111 | 110 | eqriv 2735 |
. 2
⊢ (𝐴 +ℋ
(span‘{𝐵})) = (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
112 | 1 | chssii 29166 |
. . . 4
⊢ 𝐴 ⊆
ℋ |
113 | 3, 4 | ax-mp 5 |
. . . 4
⊢ {𝐵} ⊆
ℋ |
114 | 112, 113 | spanuni 29479 |
. . 3
⊢
(span‘(𝐴 ∪
{𝐵})) = ((span‘𝐴) +ℋ
(span‘{𝐵})) |
115 | | spanid 29282 |
. . . . 5
⊢ (𝐴 ∈
Sℋ → (span‘𝐴) = 𝐴) |
116 | 2, 115 | ax-mp 5 |
. . . 4
⊢
(span‘𝐴) =
𝐴 |
117 | 116 | oveq1i 7180 |
. . 3
⊢
((span‘𝐴)
+ℋ (span‘{𝐵})) = (𝐴 +ℋ (span‘{𝐵})) |
118 | 114, 117 | eqtri 2761 |
. 2
⊢
(span‘(𝐴 ∪
{𝐵})) = (𝐴 +ℋ (span‘{𝐵})) |
119 | 16, 40 | ax-mp 5 |
. . . 4
⊢
{((projℎ‘(⊥‘𝐴))‘𝐵)} ⊆ ℋ |
120 | 112, 119 | spanuni 29479 |
. . 3
⊢
(span‘(𝐴 ∪
{((projℎ‘(⊥‘𝐴))‘𝐵)})) = ((span‘𝐴) +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
121 | 116 | oveq1i 7180 |
. . 3
⊢
((span‘𝐴)
+ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) = (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
122 | 120, 121 | eqtri 2761 |
. 2
⊢
(span‘(𝐴 ∪
{((projℎ‘(⊥‘𝐴))‘𝐵)})) = (𝐴 +ℋ
(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) |
123 | 111, 118,
122 | 3eqtr4i 2771 |
1
⊢
(span‘(𝐴 ∪
{𝐵})) = (span‘(𝐴 ∪
{((projℎ‘(⊥‘𝐴))‘𝐵)})) |