HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  spanunsni Structured version   Visualization version   GIF version

Theorem spanunsni 27625
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.)
Hypotheses
Ref Expression
spanunsn.1 𝐴C
spanunsn.2 𝐵 ∈ ℋ
Assertion
Ref Expression
spanunsni (span‘(𝐴 ∪ {𝐵})) = (span‘(𝐴 ∪ {((proj‘(⊥‘𝐴))‘𝐵)}))

Proof of Theorem spanunsni
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 spanunsn.1 . . . . . . 7 𝐴C
21chshii 27271 . . . . . 6 𝐴S
3 spanunsn.2 . . . . . . 7 𝐵 ∈ ℋ
4 snssi 4276 . . . . . . 7 (𝐵 ∈ ℋ → {𝐵} ⊆ ℋ)
5 spancl 27382 . . . . . . 7 ({𝐵} ⊆ ℋ → (span‘{𝐵}) ∈ S )
63, 4, 5mp2b 10 . . . . . 6 (span‘{𝐵}) ∈ S
72, 6shseli 27362 . . . . 5 (𝑥 ∈ (𝐴 + (span‘{𝐵})) ↔ ∃𝑦𝐴𝑧 ∈ (span‘{𝐵})𝑥 = (𝑦 + 𝑧))
83elspansni 27604 . . . . . . . 8 (𝑧 ∈ (span‘{𝐵}) ↔ ∃𝑤 ∈ ℂ 𝑧 = (𝑤 · 𝐵))
91, 3pjclii 27467 . . . . . . . . . . . . . . . 16 ((proj𝐴)‘𝐵) ∈ 𝐴
10 shmulcl 27262 . . . . . . . . . . . . . . . 16 ((𝐴S𝑤 ∈ ℂ ∧ ((proj𝐴)‘𝐵) ∈ 𝐴) → (𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴)
112, 9, 10mp3an13 1406 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ → (𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴)
12 shaddcl 27261 . . . . . . . . . . . . . . 15 ((𝐴S𝑦𝐴 ∧ (𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴) → (𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) ∈ 𝐴)
1311, 12syl3an3 1352 . . . . . . . . . . . . . 14 ((𝐴S𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) ∈ 𝐴)
142, 13mp3an1 1402 . . . . . . . . . . . . 13 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) ∈ 𝐴)
151choccli 27353 . . . . . . . . . . . . . . . 16 (⊥‘𝐴) ∈ C
1615, 3pjhclii 27468 . . . . . . . . . . . . . . 15 ((proj‘(⊥‘𝐴))‘𝐵) ∈ ℋ
17 spansnmul 27610 . . . . . . . . . . . . . . 15 ((((proj‘(⊥‘𝐴))‘𝐵) ∈ ℋ ∧ 𝑤 ∈ ℂ) → (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
1816, 17mpan 701 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ → (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
1918adantl 480 . . . . . . . . . . . . 13 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
201, 3pjpji 27470 . . . . . . . . . . . . . . . . . 18 𝐵 = (((proj𝐴)‘𝐵) + ((proj‘(⊥‘𝐴))‘𝐵))
2120oveq2i 6535 . . . . . . . . . . . . . . . . 17 (𝑤 · 𝐵) = (𝑤 · (((proj𝐴)‘𝐵) + ((proj‘(⊥‘𝐴))‘𝐵)))
221, 3pjhclii 27468 . . . . . . . . . . . . . . . . . 18 ((proj𝐴)‘𝐵) ∈ ℋ
23 ax-hvdistr1 27052 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℂ ∧ ((proj𝐴)‘𝐵) ∈ ℋ ∧ ((proj‘(⊥‘𝐴))‘𝐵) ∈ ℋ) → (𝑤 · (((proj𝐴)‘𝐵) + ((proj‘(⊥‘𝐴))‘𝐵))) = ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
2422, 16, 23mp3an23 1407 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → (𝑤 · (((proj𝐴)‘𝐵) + ((proj‘(⊥‘𝐴))‘𝐵))) = ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
2521, 24syl5eq 2652 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (𝑤 · 𝐵) = ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
2625adantl 480 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑤 · 𝐵) = ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
2726oveq2d 6540 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · 𝐵)) = (𝑦 + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
281cheli 27276 . . . . . . . . . . . . . . 15 (𝑦𝐴𝑦 ∈ ℋ)
29 hvmulcl 27057 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℂ ∧ ((proj𝐴)‘𝐵) ∈ ℋ) → (𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ)
3022, 29mpan2 702 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ)
31 hvmulcl 27057 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℂ ∧ ((proj‘(⊥‘𝐴))‘𝐵) ∈ ℋ) → (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)
3216, 31mpan2 702 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)
3330, 32jca 552 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ → ((𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ))
34 ax-hvass 27046 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℋ ∧ (𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ) → ((𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (𝑦 + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
35343expb 1257 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℋ ∧ ((𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)) → ((𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (𝑦 + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
3628, 33, 35syl2an 492 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑤 ∈ ℂ) → ((𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (𝑦 + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
3727, 36eqtr4d 2643 . . . . . . . . . . . . 13 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · 𝐵)) = ((𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
38 rspceov 6565 . . . . . . . . . . . . 13 (((𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) ∈ 𝐴 ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)}) ∧ (𝑦 + (𝑤 · 𝐵)) = ((𝑦 + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) → ∃𝑣𝐴𝑢 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)})(𝑦 + (𝑤 · 𝐵)) = (𝑣 + 𝑢))
3914, 19, 37, 38syl3anc 1317 . . . . . . . . . . . 12 ((𝑦𝐴𝑤 ∈ ℂ) → ∃𝑣𝐴𝑢 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)})(𝑦 + (𝑤 · 𝐵)) = (𝑣 + 𝑢))
40 snssi 4276 . . . . . . . . . . . . . 14 (((proj‘(⊥‘𝐴))‘𝐵) ∈ ℋ → {((proj‘(⊥‘𝐴))‘𝐵)} ⊆ ℋ)
41 spancl 27382 . . . . . . . . . . . . . 14 ({((proj‘(⊥‘𝐴))‘𝐵)} ⊆ ℋ → (span‘{((proj‘(⊥‘𝐴))‘𝐵)}) ∈ S )
4216, 40, 41mp2b 10 . . . . . . . . . . . . 13 (span‘{((proj‘(⊥‘𝐴))‘𝐵)}) ∈ S
432, 42shseli 27362 . . . . . . . . . . . 12 ((𝑦 + (𝑤 · 𝐵)) ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})) ↔ ∃𝑣𝐴𝑢 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)})(𝑦 + (𝑤 · 𝐵)) = (𝑣 + 𝑢))
4439, 43sylibr 222 . . . . . . . . . . 11 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · 𝐵)) ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))
45 oveq2 6532 . . . . . . . . . . . . 13 (𝑧 = (𝑤 · 𝐵) → (𝑦 + 𝑧) = (𝑦 + (𝑤 · 𝐵)))
4645eqeq2d 2616 . . . . . . . . . . . 12 (𝑧 = (𝑤 · 𝐵) → (𝑥 = (𝑦 + 𝑧) ↔ 𝑥 = (𝑦 + (𝑤 · 𝐵))))
4746biimpa 499 . . . . . . . . . . 11 ((𝑧 = (𝑤 · 𝐵) ∧ 𝑥 = (𝑦 + 𝑧)) → 𝑥 = (𝑦 + (𝑤 · 𝐵)))
48 eleq1 2672 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑤 · 𝐵)) → (𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})) ↔ (𝑦 + (𝑤 · 𝐵)) ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))))
4948biimparc 502 . . . . . . . . . . 11 (((𝑦 + (𝑤 · 𝐵)) ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})) ∧ 𝑥 = (𝑦 + (𝑤 · 𝐵))) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))
5044, 47, 49syl2an 492 . . . . . . . . . 10 (((𝑦𝐴𝑤 ∈ ℂ) ∧ (𝑧 = (𝑤 · 𝐵) ∧ 𝑥 = (𝑦 + 𝑧))) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))
5150exp43 637 . . . . . . . . 9 (𝑦𝐴 → (𝑤 ∈ ℂ → (𝑧 = (𝑤 · 𝐵) → (𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))))))
5251rexlimdv 3008 . . . . . . . 8 (𝑦𝐴 → (∃𝑤 ∈ ℂ 𝑧 = (𝑤 · 𝐵) → (𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))))
538, 52syl5bi 230 . . . . . . 7 (𝑦𝐴 → (𝑧 ∈ (span‘{𝐵}) → (𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))))
5453rexlimdv 3008 . . . . . 6 (𝑦𝐴 → (∃𝑧 ∈ (span‘{𝐵})𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))))
5554rexlimiv 3005 . . . . 5 (∃𝑦𝐴𝑧 ∈ (span‘{𝐵})𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))
567, 55sylbi 205 . . . 4 (𝑥 ∈ (𝐴 + (span‘{𝐵})) → 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))
572, 42shseli 27362 . . . . 5 (𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})) ↔ ∃𝑦𝐴𝑧 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)})𝑥 = (𝑦 + 𝑧))
5816elspansni 27604 . . . . . . . 8 (𝑧 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)}) ↔ ∃𝑤 ∈ ℂ 𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))
59 negcl 10129 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → -𝑤 ∈ ℂ)
60 shmulcl 27262 . . . . . . . . . . . . . . . . . 18 ((𝐴S ∧ -𝑤 ∈ ℂ ∧ ((proj𝐴)‘𝐵) ∈ 𝐴) → (-𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴)
612, 9, 60mp3an13 1406 . . . . . . . . . . . . . . . . 17 (-𝑤 ∈ ℂ → (-𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴)
6259, 61syl 17 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (-𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴)
63 shaddcl 27261 . . . . . . . . . . . . . . . 16 ((𝐴S ∧ (-𝑤 · ((proj𝐴)‘𝐵)) ∈ 𝐴𝑦𝐴) → ((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) ∈ 𝐴)
6462, 63syl3an2 1351 . . . . . . . . . . . . . . 15 ((𝐴S𝑤 ∈ ℂ ∧ 𝑦𝐴) → ((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) ∈ 𝐴)
652, 64mp3an1 1402 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℂ ∧ 𝑦𝐴) → ((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) ∈ 𝐴)
6665ancoms 467 . . . . . . . . . . . . 13 ((𝑦𝐴𝑤 ∈ ℂ) → ((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) ∈ 𝐴)
67 spansnmul 27610 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℋ ∧ 𝑤 ∈ ℂ) → (𝑤 · 𝐵) ∈ (span‘{𝐵}))
683, 67mpan 701 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ → (𝑤 · 𝐵) ∈ (span‘{𝐵}))
6968adantl 480 . . . . . . . . . . . . 13 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑤 · 𝐵) ∈ (span‘{𝐵}))
70 hvm1neg 27076 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 ∈ ℂ ∧ ((proj𝐴)‘𝐵) ∈ ℋ) → (-1 · (𝑤 · ((proj𝐴)‘𝐵))) = (-𝑤 · ((proj𝐴)‘𝐵)))
7122, 70mpan2 702 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℂ → (-1 · (𝑤 · ((proj𝐴)‘𝐵))) = (-𝑤 · ((proj𝐴)‘𝐵)))
7271oveq2d 6540 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℂ → ((𝑤 · ((proj𝐴)‘𝐵)) + (-1 · (𝑤 · ((proj𝐴)‘𝐵)))) = ((𝑤 · ((proj𝐴)‘𝐵)) + (-𝑤 · ((proj𝐴)‘𝐵))))
73 hvnegid 27071 . . . . . . . . . . . . . . . . . . 19 ((𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ → ((𝑤 · ((proj𝐴)‘𝐵)) + (-1 · (𝑤 · ((proj𝐴)‘𝐵)))) = 0)
7430, 73syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℂ → ((𝑤 · ((proj𝐴)‘𝐵)) + (-1 · (𝑤 · ((proj𝐴)‘𝐵)))) = 0)
75 hvmulcl 27057 . . . . . . . . . . . . . . . . . . . 20 ((-𝑤 ∈ ℂ ∧ ((proj𝐴)‘𝐵) ∈ ℋ) → (-𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ)
7659, 22, 75sylancl 692 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℂ → (-𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ)
77 ax-hvcom 27045 . . . . . . . . . . . . . . . . . . 19 (((𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (-𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ) → ((𝑤 · ((proj𝐴)‘𝐵)) + (-𝑤 · ((proj𝐴)‘𝐵))) = ((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))))
7830, 76, 77syl2anc 690 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℂ → ((𝑤 · ((proj𝐴)‘𝐵)) + (-𝑤 · ((proj𝐴)‘𝐵))) = ((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))))
7972, 74, 783eqtr3d 2648 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 0 = ((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))))
8079adantl 480 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑤 ∈ ℂ) → 0 = ((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))))
8180oveq1d 6539 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑤 ∈ ℂ) → (0 + (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) = (((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
82 hvaddcl 27056 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℋ ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ) → (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ ℋ)
8328, 32, 82syl2an 492 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ ℋ)
84 hvaddid2 27067 . . . . . . . . . . . . . . . 16 ((𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ ℋ → (0 + (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
8583, 84syl 17 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑤 ∈ ℂ) → (0 + (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
8676, 30jca 552 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → ((-𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ))
8786adantl 480 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑤 ∈ ℂ) → ((-𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ))
8828, 32anim12i 587 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 ∈ ℋ ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ))
89 hvadd4 27080 . . . . . . . . . . . . . . . 16 ((((-𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ ∧ (𝑤 · ((proj𝐴)‘𝐵)) ∈ ℋ) ∧ (𝑦 ∈ ℋ ∧ (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∈ ℋ)) → (((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) = (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
9087, 88, 89syl2anc 690 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑤 ∈ ℂ) → (((-𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj𝐴)‘𝐵))) + (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) = (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
9181, 85, 903eqtr3d 2648 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
9226oveq2d 6540 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑤 ∈ ℂ) → (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + (𝑤 · 𝐵)) = (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + ((𝑤 · ((proj𝐴)‘𝐵)) + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
9391, 92eqtr4d 2643 . . . . . . . . . . . . 13 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + (𝑤 · 𝐵)))
94 rspceov 6565 . . . . . . . . . . . . 13 ((((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) ∈ 𝐴 ∧ (𝑤 · 𝐵) ∈ (span‘{𝐵}) ∧ (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (((-𝑤 · ((proj𝐴)‘𝐵)) + 𝑦) + (𝑤 · 𝐵))) → ∃𝑣𝐴𝑢 ∈ (span‘{𝐵})(𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (𝑣 + 𝑢))
9566, 69, 93, 94syl3anc 1317 . . . . . . . . . . . 12 ((𝑦𝐴𝑤 ∈ ℂ) → ∃𝑣𝐴𝑢 ∈ (span‘{𝐵})(𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (𝑣 + 𝑢))
962, 6shseli 27362 . . . . . . . . . . . 12 ((𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 + (span‘{𝐵})) ↔ ∃𝑣𝐴𝑢 ∈ (span‘{𝐵})(𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) = (𝑣 + 𝑢))
9795, 96sylibr 222 . . . . . . . . . . 11 ((𝑦𝐴𝑤 ∈ ℂ) → (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 + (span‘{𝐵})))
98 oveq2 6532 . . . . . . . . . . . . 13 (𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) → (𝑦 + 𝑧) = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
9998eqeq2d 2616 . . . . . . . . . . . 12 (𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) → (𝑥 = (𝑦 + 𝑧) ↔ 𝑥 = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))))
10099biimpa 499 . . . . . . . . . . 11 ((𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∧ 𝑥 = (𝑦 + 𝑧)) → 𝑥 = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))))
101 eleq1 2672 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) → (𝑥 ∈ (𝐴 + (span‘{𝐵})) ↔ (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 + (span‘{𝐵}))))
102101biimparc 502 . . . . . . . . . . 11 (((𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵))) ∈ (𝐴 + (span‘{𝐵})) ∧ 𝑥 = (𝑦 + (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)))) → 𝑥 ∈ (𝐴 + (span‘{𝐵})))
10397, 100, 102syl2an 492 . . . . . . . . . 10 (((𝑦𝐴𝑤 ∈ ℂ) ∧ (𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) ∧ 𝑥 = (𝑦 + 𝑧))) → 𝑥 ∈ (𝐴 + (span‘{𝐵})))
104103exp43 637 . . . . . . . . 9 (𝑦𝐴 → (𝑤 ∈ ℂ → (𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) → (𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{𝐵}))))))
105104rexlimdv 3008 . . . . . . . 8 (𝑦𝐴 → (∃𝑤 ∈ ℂ 𝑧 = (𝑤 · ((proj‘(⊥‘𝐴))‘𝐵)) → (𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{𝐵})))))
10658, 105syl5bi 230 . . . . . . 7 (𝑦𝐴 → (𝑧 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)}) → (𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{𝐵})))))
107106rexlimdv 3008 . . . . . 6 (𝑦𝐴 → (∃𝑧 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)})𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{𝐵}))))
108107rexlimiv 3005 . . . . 5 (∃𝑦𝐴𝑧 ∈ (span‘{((proj‘(⊥‘𝐴))‘𝐵)})𝑥 = (𝑦 + 𝑧) → 𝑥 ∈ (𝐴 + (span‘{𝐵})))
10957, 108sylbi 205 . . . 4 (𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})) → 𝑥 ∈ (𝐴 + (span‘{𝐵})))
11056, 109impbii 197 . . 3 (𝑥 ∈ (𝐴 + (span‘{𝐵})) ↔ 𝑥 ∈ (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})))
111110eqriv 2603 . 2 (𝐴 + (span‘{𝐵})) = (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
1121chssii 27275 . . . 4 𝐴 ⊆ ℋ
1133, 4ax-mp 5 . . . 4 {𝐵} ⊆ ℋ
114112, 113spanuni 27590 . . 3 (span‘(𝐴 ∪ {𝐵})) = ((span‘𝐴) + (span‘{𝐵}))
115 spanid 27393 . . . . 5 (𝐴S → (span‘𝐴) = 𝐴)
1162, 115ax-mp 5 . . . 4 (span‘𝐴) = 𝐴
117116oveq1i 6534 . . 3 ((span‘𝐴) + (span‘{𝐵})) = (𝐴 + (span‘{𝐵}))
118114, 117eqtri 2628 . 2 (span‘(𝐴 ∪ {𝐵})) = (𝐴 + (span‘{𝐵}))
11916, 40ax-mp 5 . . . 4 {((proj‘(⊥‘𝐴))‘𝐵)} ⊆ ℋ
120112, 119spanuni 27590 . . 3 (span‘(𝐴 ∪ {((proj‘(⊥‘𝐴))‘𝐵)})) = ((span‘𝐴) + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
121116oveq1i 6534 . . 3 ((span‘𝐴) + (span‘{((proj‘(⊥‘𝐴))‘𝐵)})) = (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
122120, 121eqtri 2628 . 2 (span‘(𝐴 ∪ {((proj‘(⊥‘𝐴))‘𝐵)})) = (𝐴 + (span‘{((proj‘(⊥‘𝐴))‘𝐵)}))
123111, 118, 1223eqtr4i 2638 1 (span‘(𝐴 ∪ {𝐵})) = (span‘(𝐴 ∪ {((proj‘(⊥‘𝐴))‘𝐵)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  wrex 2893  cun 3534  wss 3536  {csn 4121  cfv 5787  (class class class)co 6524  cc 9787  1c1 9790  -cneg 10115  chil 26963   + cva 26964   · csm 26965  0c0v 26968   S csh 26972   C cch 26973  cort 26974   + cph 26975  spancspn 26976  projcpjh 26981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cc 9114  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869  ax-hilex 27043  ax-hfvadd 27044  ax-hvcom 27045  ax-hvass 27046  ax-hv0cl 27047  ax-hvaddid 27048  ax-hfvmul 27049  ax-hvmulid 27050  ax-hvmulass 27051  ax-hvdistr1 27052  ax-hvdistr2 27053  ax-hvmul0 27054  ax-hfi 27123  ax-his1 27126  ax-his2 27127  ax-his3 27128  ax-his4 27129  ax-hcompl 27246
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-supp 7157  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-omul 7426  df-er 7603  df-map 7720  df-pm 7721  df-ixp 7769  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fsupp 8133  df-fi 8174  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-acn 8625  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-ioo 12003  df-ico 12005  df-icc 12006  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-sum 14208  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-sets 15644  df-ress 15645  df-plusg 15724  df-mulr 15725  df-starv 15726  df-sca 15727  df-vsca 15728  df-ip 15729  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-hom 15736  df-cco 15737  df-rest 15849  df-topn 15850  df-0g 15868  df-gsum 15869  df-topgen 15870  df-pt 15871  df-prds 15874  df-xrs 15928  df-qtop 15933  df-imas 15934  df-xps 15936  df-mre 16012  df-mrc 16013  df-acs 16015  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-submnd 17102  df-mulg 17307  df-cntz 17516  df-cmn 17961  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-fbas 19507  df-fg 19508  df-cnfld 19511  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-cld 20572  df-ntr 20573  df-cls 20574  df-nei 20651  df-cn 20780  df-cnp 20781  df-lm 20782  df-haus 20868  df-tx 21114  df-hmeo 21307  df-fil 21399  df-fm 21491  df-flim 21492  df-flf 21493  df-xms 21873  df-ms 21874  df-tms 21875  df-cfil 22776  df-cau 22777  df-cmet 22778  df-grpo 26494  df-gid 26495  df-ginv 26496  df-gdiv 26497  df-ablo 26549  df-vc 26564  df-nv 26612  df-va 26615  df-ba 26616  df-sm 26617  df-0v 26618  df-vs 26619  df-nmcv 26620  df-ims 26621  df-dip 26738  df-ssp 26762  df-ph 26855  df-cbn 26906  df-hnorm 27012  df-hba 27013  df-hvsub 27015  df-hlim 27016  df-hcau 27017  df-sh 27251  df-ch 27265  df-oc 27296  df-ch0 27297  df-shs 27354  df-span 27355  df-pjh 27441
This theorem is referenced by:  spansnji  27692
  Copyright terms: Public domain W3C validator