Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
2 | | ssps.s |
. . . . . . . . . . 11
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
3 | 1, 2 | nvsf 27474 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ ×
(BaseSet‘𝑈))⟶(BaseSet‘𝑈)) |
4 | | ffun 6048 |
. . . . . . . . . 10
⊢ (𝑆:(ℂ ×
(BaseSet‘𝑈))⟶(BaseSet‘𝑈) → Fun 𝑆) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝑈 ∈ NrmCVec → Fun 𝑆) |
6 | | funres 5929 |
. . . . . . . . 9
⊢ (Fun
𝑆 → Fun (𝑆 ↾ (ℂ × 𝑌))) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec → Fun
(𝑆 ↾ (ℂ ×
𝑌))) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → Fun (𝑆 ↾ (ℂ × 𝑌))) |
9 | | ssps.h |
. . . . . . . . . 10
⊢ 𝐻 = (SubSp‘𝑈) |
10 | 9 | sspnv 27581 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
11 | | ssps.y |
. . . . . . . . . 10
⊢ 𝑌 = (BaseSet‘𝑊) |
12 | | ssps.r |
. . . . . . . . . 10
⊢ 𝑅 = (
·𝑠OLD ‘𝑊) |
13 | 11, 12 | nvsf 27474 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmCVec → 𝑅:(ℂ × 𝑌)⟶𝑌) |
14 | 10, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅:(ℂ × 𝑌)⟶𝑌) |
15 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑅:(ℂ × 𝑌)⟶𝑌 → 𝑅 Fn (ℂ × 𝑌)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 Fn (ℂ × 𝑌)) |
17 | | fnresdm 6000 |
. . . . . . . . 9
⊢ (𝑅 Fn (ℂ × 𝑌) → (𝑅 ↾ (ℂ × 𝑌)) = 𝑅) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑅 ↾ (ℂ × 𝑌)) = 𝑅) |
19 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
20 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (
+𝑣 ‘𝑊) = ( +𝑣 ‘𝑊) |
21 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
22 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
23 | 19, 20, 2, 12, 21, 22, 9 | isssp 27579 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ ((
+𝑣 ‘𝑊) ⊆ ( +𝑣
‘𝑈) ∧ 𝑅 ⊆ 𝑆 ∧ (normCV‘𝑊) ⊆
(normCV‘𝑈))))) |
24 | 23 | simplbda 654 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (( +𝑣
‘𝑊) ⊆ (
+𝑣 ‘𝑈) ∧ 𝑅 ⊆ 𝑆 ∧ (normCV‘𝑊) ⊆
(normCV‘𝑈))) |
25 | 24 | simp2d 1074 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 ⊆ 𝑆) |
26 | | ssres 5424 |
. . . . . . . . 9
⊢ (𝑅 ⊆ 𝑆 → (𝑅 ↾ (ℂ × 𝑌)) ⊆ (𝑆 ↾ (ℂ × 𝑌))) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑅 ↾ (ℂ × 𝑌)) ⊆ (𝑆 ↾ (ℂ × 𝑌))) |
28 | 18, 27 | eqsstr3d 3640 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 ⊆ (𝑆 ↾ (ℂ × 𝑌))) |
29 | 8, 16, 28 | 3jca 1242 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (Fun (𝑆 ↾ (ℂ × 𝑌)) ∧ 𝑅 Fn (ℂ × 𝑌) ∧ 𝑅 ⊆ (𝑆 ↾ (ℂ × 𝑌)))) |
30 | | oprssov 6803 |
. . . . . 6
⊢ (((Fun
(𝑆 ↾ (ℂ ×
𝑌)) ∧ 𝑅 Fn (ℂ × 𝑌) ∧ 𝑅 ⊆ (𝑆 ↾ (ℂ × 𝑌))) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦) = (𝑥𝑅𝑦)) |
31 | 29, 30 | sylan 488 |
. . . . 5
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦) = (𝑥𝑅𝑦)) |
32 | 31 | eqcomd 2628 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑅𝑦) = (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦)) |
33 | 32 | ralrimivva 2971 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑌 (𝑥𝑅𝑦) = (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦)) |
34 | | eqid 2622 |
. . 3
⊢ (ℂ
× 𝑌) = (ℂ
× 𝑌) |
35 | 33, 34 | jctil 560 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ((ℂ × 𝑌) = (ℂ × 𝑌) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑌 (𝑥𝑅𝑦) = (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦))) |
36 | | ffn 6045 |
. . . . . 6
⊢ (𝑆:(ℂ ×
(BaseSet‘𝑈))⟶(BaseSet‘𝑈) → 𝑆 Fn (ℂ × (BaseSet‘𝑈))) |
37 | 3, 36 | syl 17 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec → 𝑆 Fn (ℂ ×
(BaseSet‘𝑈))) |
38 | 37 | adantr 481 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑆 Fn (ℂ × (BaseSet‘𝑈))) |
39 | | ssid 3624 |
. . . . 5
⊢ ℂ
⊆ ℂ |
40 | 1, 11, 9 | sspba 27582 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ (BaseSet‘𝑈)) |
41 | | xpss12 5225 |
. . . . 5
⊢ ((ℂ
⊆ ℂ ∧ 𝑌
⊆ (BaseSet‘𝑈))
→ (ℂ × 𝑌)
⊆ (ℂ × (BaseSet‘𝑈))) |
42 | 39, 40, 41 | sylancr 695 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (ℂ × 𝑌) ⊆ (ℂ ×
(BaseSet‘𝑈))) |
43 | | fnssres 6004 |
. . . 4
⊢ ((𝑆 Fn (ℂ ×
(BaseSet‘𝑈)) ∧
(ℂ × 𝑌) ⊆
(ℂ × (BaseSet‘𝑈))) → (𝑆 ↾ (ℂ × 𝑌)) Fn (ℂ × 𝑌)) |
44 | 38, 42, 43 | syl2anc 693 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑆 ↾ (ℂ × 𝑌)) Fn (ℂ × 𝑌)) |
45 | | eqfnov 6766 |
. . 3
⊢ ((𝑅 Fn (ℂ × 𝑌) ∧ (𝑆 ↾ (ℂ × 𝑌)) Fn (ℂ × 𝑌)) → (𝑅 = (𝑆 ↾ (ℂ × 𝑌)) ↔ ((ℂ × 𝑌) = (ℂ × 𝑌) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑌 (𝑥𝑅𝑦) = (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦)))) |
46 | 16, 44, 45 | syl2anc 693 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑅 = (𝑆 ↾ (ℂ × 𝑌)) ↔ ((ℂ × 𝑌) = (ℂ × 𝑌) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑌 (𝑥𝑅𝑦) = (𝑥(𝑆 ↾ (ℂ × 𝑌))𝑦)))) |
47 | 35, 46 | mpbird 247 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 = (𝑆 ↾ (ℂ × 𝑌))) |