Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
2 | | sspg.g |
. . . . . . . . . . 11
⊢ 𝐺 = ( +𝑣
‘𝑈) |
3 | 1, 2 | nvgf 27473 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶(BaseSet‘𝑈)) |
4 | | ffun 6048 |
. . . . . . . . . 10
⊢ (𝐺:((BaseSet‘𝑈) × (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 | | sspg.h |
. . . . . . . . . 10
⊢ 𝐻 = (SubSp‘𝑈) |
10 | 9 | sspnv 27581 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
11 | | sspg.y |
. . . . . . . . . 10
⊢ 𝑌 = (BaseSet‘𝑊) |
12 | | sspg.f |
. . . . . . . . . 10
⊢ 𝐹 = ( +𝑣
‘𝑊) |
13 | 11, 12 | nvgf 27473 |
. . . . . . . . 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
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
20 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
21 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
22 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
23 | 2, 12, 19, 20, 21, 22, 9 | isssp 27579 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑊) ⊆ (
·𝑠OLD ‘𝑈) ∧ (normCV‘𝑊) ⊆
(normCV‘𝑈))))) |
24 | 23 | simplbda 654 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑊) ⊆ (
·𝑠OLD ‘𝑈) ∧ (normCV‘𝑊) ⊆
(normCV‘𝑈))) |
25 | 24 | simp1d 1073 |
. . . . . . . . 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‘𝑈))⟶(BaseSet‘𝑈) → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
37 | 3, 36 | syl 17 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
38 | 37 | adantr 481 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
39 | 1, 11, 9 | sspba 27582 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ (BaseSet‘𝑈)) |
40 | | xpss12 5225 |
. . . . 5
⊢ ((𝑌 ⊆ (BaseSet‘𝑈) ∧ 𝑌 ⊆ (BaseSet‘𝑈)) → (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
41 | 39, 39, 40 | syl2anc 693 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
42 | | fnssres 6004 |
. . . 4
⊢ ((𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈)) ∧ (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) → (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) |
43 | 38, 41, 42 | syl2anc 693 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) |
44 | | eqfnov 6766 |
. . 3
⊢ ((𝐹 Fn (𝑌 × 𝑌) ∧ (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) → (𝐹 = (𝐺 ↾ (𝑌 × 𝑌)) ↔ ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)))) |
45 | 16, 43, 44 | syl2anc 693 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 = (𝐺 ↾ (𝑌 × 𝑌)) ↔ ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)))) |
46 | 35, 45 | mpbird 247 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) |