Step | Hyp | Ref
| Expression |
1 | | eqid 2821 |
. . . . . . . . . . 11
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
2 | | sspg.g |
. . . . . . . . . . 11
⊢ 𝐺 = ( +𝑣
‘𝑈) |
3 | 1, 2 | nvgf 28323 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶(BaseSet‘𝑈)) |
4 | 3 | ffund 6512 |
. . . . . . . . 9
⊢ (𝑈 ∈ NrmCVec → Fun 𝐺) |
5 | | funres 6391 |
. . . . . . . . 9
⊢ (Fun
𝐺 → Fun (𝐺 ↾ (𝑌 × 𝑌))) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec → Fun
(𝐺 ↾ (𝑌 × 𝑌))) |
7 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → Fun (𝐺 ↾ (𝑌 × 𝑌))) |
8 | | sspg.h |
. . . . . . . . . 10
⊢ 𝐻 = (SubSp‘𝑈) |
9 | 8 | sspnv 28431 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
10 | | sspg.y |
. . . . . . . . . 10
⊢ 𝑌 = (BaseSet‘𝑊) |
11 | | sspg.f |
. . . . . . . . . 10
⊢ 𝐹 = ( +𝑣
‘𝑊) |
12 | 10, 11 | nvgf 28323 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑌) |
13 | 9, 12 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹:(𝑌 × 𝑌)⟶𝑌) |
14 | 13 | ffnd 6509 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 Fn (𝑌 × 𝑌)) |
15 | | fnresdm 6460 |
. . . . . . . . 9
⊢ (𝐹 Fn (𝑌 × 𝑌) → (𝐹 ↾ (𝑌 × 𝑌)) = 𝐹) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 ↾ (𝑌 × 𝑌)) = 𝐹) |
17 | | eqid 2821 |
. . . . . . . . . . . 12
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
18 | | eqid 2821 |
. . . . . . . . . . . 12
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
19 | | eqid 2821 |
. . . . . . . . . . . 12
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
20 | | eqid 2821 |
. . . . . . . . . . . 12
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
21 | 2, 11, 17, 18, 19, 20, 8 | isssp 28429 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑊) ⊆ (
·𝑠OLD ‘𝑈) ∧ (normCV‘𝑊) ⊆
(normCV‘𝑈))))) |
22 | 21 | simplbda 500 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑊) ⊆ (
·𝑠OLD ‘𝑈) ∧ (normCV‘𝑊) ⊆
(normCV‘𝑈))) |
23 | 22 | simp1d 1134 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 ⊆ 𝐺) |
24 | | ssres 5874 |
. . . . . . . . 9
⊢ (𝐹 ⊆ 𝐺 → (𝐹 ↾ (𝑌 × 𝑌)) ⊆ (𝐺 ↾ (𝑌 × 𝑌))) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 ↾ (𝑌 × 𝑌)) ⊆ (𝐺 ↾ (𝑌 × 𝑌))) |
26 | 16, 25 | eqsstrrd 4005 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 ⊆ (𝐺 ↾ (𝑌 × 𝑌))) |
27 | 7, 14, 26 | 3jca 1120 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (Fun (𝐺 ↾ (𝑌 × 𝑌)) ∧ 𝐹 Fn (𝑌 × 𝑌) ∧ 𝐹 ⊆ (𝐺 ↾ (𝑌 × 𝑌)))) |
28 | | oprssov 7306 |
. . . . . 6
⊢ (((Fun
(𝐺 ↾ (𝑌 × 𝑌)) ∧ 𝐹 Fn (𝑌 × 𝑌) ∧ 𝐹 ⊆ (𝐺 ↾ (𝑌 × 𝑌))) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦) = (𝑥𝐹𝑦)) |
29 | 27, 28 | sylan 580 |
. . . . 5
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦) = (𝑥𝐹𝑦)) |
30 | 29 | eqcomd 2827 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)) |
31 | 30 | ralrimivva 3191 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)) |
32 | | eqid 2821 |
. . 3
⊢ (𝑌 × 𝑌) = (𝑌 × 𝑌) |
33 | 31, 32 | jctil 520 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦))) |
34 | 3 | ffnd 6509 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
35 | 34 | adantr 481 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
36 | 1, 10, 8 | sspba 28432 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ (BaseSet‘𝑈)) |
37 | | xpss12 5564 |
. . . . 5
⊢ ((𝑌 ⊆ (BaseSet‘𝑈) ∧ 𝑌 ⊆ (BaseSet‘𝑈)) → (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
38 | 36, 36, 37 | syl2anc 584 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
39 | | fnssres 6464 |
. . . 4
⊢ ((𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈)) ∧ (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) → (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) |
40 | 35, 38, 39 | syl2anc 584 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) |
41 | | eqfnov 7269 |
. . 3
⊢ ((𝐹 Fn (𝑌 × 𝑌) ∧ (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) → (𝐹 = (𝐺 ↾ (𝑌 × 𝑌)) ↔ ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)))) |
42 | 14, 40, 41 | syl2anc 584 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 = (𝐺 ↾ (𝑌 × 𝑌)) ↔ ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)))) |
43 | 33, 42 | mpbird 258 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) |