Step | Hyp | Ref
| Expression |
1 | | sspn.h |
. . . . 5
⊢ 𝐻 = (SubSp‘𝑈) |
2 | 1 | sspnv 27581 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
3 | | sspn.y |
. . . . 5
⊢ 𝑌 = (BaseSet‘𝑊) |
4 | | sspn.m |
. . . . 5
⊢ 𝑀 =
(normCV‘𝑊) |
5 | 3, 4 | nvf 27515 |
. . . 4
⊢ (𝑊 ∈ NrmCVec → 𝑀:𝑌⟶ℝ) |
6 | 2, 5 | syl 17 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀:𝑌⟶ℝ) |
7 | | ffn 6045 |
. . 3
⊢ (𝑀:𝑌⟶ℝ → 𝑀 Fn 𝑌) |
8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 Fn 𝑌) |
9 | | eqid 2622 |
. . . . . 6
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
10 | | sspn.n |
. . . . . 6
⊢ 𝑁 =
(normCV‘𝑈) |
11 | 9, 10 | nvf 27515 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec → 𝑁:(BaseSet‘𝑈)⟶ℝ) |
12 | | ffn 6045 |
. . . . 5
⊢ (𝑁:(BaseSet‘𝑈)⟶ℝ → 𝑁 Fn (BaseSet‘𝑈)) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑁 Fn (BaseSet‘𝑈)) |
14 | 13 | adantr 481 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑁 Fn (BaseSet‘𝑈)) |
15 | 9, 3, 1 | sspba 27582 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ (BaseSet‘𝑈)) |
16 | | fnssres 6004 |
. . 3
⊢ ((𝑁 Fn (BaseSet‘𝑈) ∧ 𝑌 ⊆ (BaseSet‘𝑈)) → (𝑁 ↾ 𝑌) Fn 𝑌) |
17 | 14, 15, 16 | syl2anc 693 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑁 ↾ 𝑌) Fn 𝑌) |
18 | | ffun 6048 |
. . . . . . 7
⊢ (𝑁:(BaseSet‘𝑈)⟶ℝ → Fun
𝑁) |
19 | 11, 18 | syl 17 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → Fun 𝑁) |
20 | | funres 5929 |
. . . . . 6
⊢ (Fun
𝑁 → Fun (𝑁 ↾ 𝑌)) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec → Fun
(𝑁 ↾ 𝑌)) |
22 | 21 | ad2antrr 762 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑌) → Fun (𝑁 ↾ 𝑌)) |
23 | | fnresdm 6000 |
. . . . . . 7
⊢ (𝑀 Fn 𝑌 → (𝑀 ↾ 𝑌) = 𝑀) |
24 | 8, 23 | syl 17 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑀 ↾ 𝑌) = 𝑀) |
25 | | eqid 2622 |
. . . . . . . . . 10
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
26 | | eqid 2622 |
. . . . . . . . . 10
⊢ (
+𝑣 ‘𝑊) = ( +𝑣 ‘𝑊) |
27 | | eqid 2622 |
. . . . . . . . . 10
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
28 | | eqid 2622 |
. . . . . . . . . 10
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
29 | 25, 26, 27, 28, 10, 4, 1 | isssp 27579 |
. . . . . . . . 9
⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ ((
+𝑣 ‘𝑊) ⊆ ( +𝑣
‘𝑈) ∧ (
·𝑠OLD ‘𝑊) ⊆ (
·𝑠OLD ‘𝑈) ∧ 𝑀 ⊆ 𝑁)))) |
30 | 29 | simplbda 654 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (( +𝑣
‘𝑊) ⊆ (
+𝑣 ‘𝑈) ∧ (
·𝑠OLD ‘𝑊) ⊆ (
·𝑠OLD ‘𝑈) ∧ 𝑀 ⊆ 𝑁)) |
31 | 30 | simp3d 1075 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 ⊆ 𝑁) |
32 | | ssres 5424 |
. . . . . . 7
⊢ (𝑀 ⊆ 𝑁 → (𝑀 ↾ 𝑌) ⊆ (𝑁 ↾ 𝑌)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑀 ↾ 𝑌) ⊆ (𝑁 ↾ 𝑌)) |
34 | 24, 33 | eqsstr3d 3640 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 ⊆ (𝑁 ↾ 𝑌)) |
35 | 34 | adantr 481 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑌) → 𝑀 ⊆ (𝑁 ↾ 𝑌)) |
36 | | fdm 6051 |
. . . . . . . 8
⊢ (𝑀:𝑌⟶ℝ → dom 𝑀 = 𝑌) |
37 | 5, 36 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ NrmCVec → dom 𝑀 = 𝑌) |
38 | 37 | eleq2d 2687 |
. . . . . 6
⊢ (𝑊 ∈ NrmCVec → (𝑥 ∈ dom 𝑀 ↔ 𝑥 ∈ 𝑌)) |
39 | 38 | biimpar 502 |
. . . . 5
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom 𝑀) |
40 | 2, 39 | sylan 488 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom 𝑀) |
41 | | funssfv 6209 |
. . . 4
⊢ ((Fun
(𝑁 ↾ 𝑌) ∧ 𝑀 ⊆ (𝑁 ↾ 𝑌) ∧ 𝑥 ∈ dom 𝑀) → ((𝑁 ↾ 𝑌)‘𝑥) = (𝑀‘𝑥)) |
42 | 22, 35, 40, 41 | syl3anc 1326 |
. . 3
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑌) → ((𝑁 ↾ 𝑌)‘𝑥) = (𝑀‘𝑥)) |
43 | 42 | eqcomd 2628 |
. 2
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑌) → (𝑀‘𝑥) = ((𝑁 ↾ 𝑌)‘𝑥)) |
44 | 8, 17, 43 | eqfnfvd 6314 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑁 ↾ 𝑌)) |