Step | Hyp | Ref
| Expression |
1 | | phnv 27053 |
. . 3
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
2 | | sspph.h |
. . . 4
⊢ 𝐻 = (SubSp‘𝑈) |
3 | 2 | sspnv 26965 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
4 | 1, 3 | sylan 487 |
. 2
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
5 | | eqid 2610 |
. . . . . . . . . 10
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
6 | | eqid 2610 |
. . . . . . . . . 10
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
7 | 5, 6, 2 | sspba 26966 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (BaseSet‘𝑊) ⊆ (BaseSet‘𝑈)) |
8 | 7 | sseld 3567 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑥 ∈ (BaseSet‘𝑊) → 𝑥 ∈ (BaseSet‘𝑈))) |
9 | 7 | sseld 3567 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑦 ∈ (BaseSet‘𝑊) → 𝑦 ∈ (BaseSet‘𝑈))) |
10 | 8, 9 | anim12d 584 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ((𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)))) |
11 | 1, 10 | sylan 487 |
. . . . . 6
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) → ((𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)))) |
12 | 11 | imp 444 |
. . . . 5
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈))) |
13 | | eqid 2610 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
14 | | eqid 2610 |
. . . . . . . 8
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) |
15 | | eqid 2610 |
. . . . . . . 8
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
16 | 5, 13, 14, 15 | phpar2 27062 |
. . . . . . 7
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑥 ∈
(BaseSet‘𝑈) ∧
𝑦 ∈
(BaseSet‘𝑈)) →
((((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2) + (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2)) = (2 ·
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2)))) |
17 | 16 | 3expb 1258 |
. . . . . 6
⊢ ((𝑈 ∈ CPreHilOLD
∧ (𝑥 ∈
(BaseSet‘𝑈) ∧
𝑦 ∈
(BaseSet‘𝑈))) →
((((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2) + (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2)) = (2 ·
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2)))) |
18 | 17 | adantlr 747 |
. . . . 5
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈))) → ((((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2) + (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2)) = (2 ·
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2)))) |
19 | 12, 18 | syldan 486 |
. . . 4
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2) + (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2)) = (2 ·
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2)))) |
20 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (
+𝑣 ‘𝑊) = ( +𝑣 ‘𝑊) |
21 | 6, 20 | nvgcl 26859 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑥( +𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) |
22 | 21 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥( +𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) |
23 | 3, 22 | sylan 487 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥( +𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) |
24 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
25 | 6, 15, 24, 2 | sspnval 26976 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ (𝑥( +𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑊)𝑦))) |
26 | 25 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥( +𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑊)𝑦))) |
27 | 23, 26 | syldan 486 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑊)𝑦))) |
28 | 27 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) = (((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2)) |
29 | 6, 13, 20, 2 | sspgval 26968 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥( +𝑣 ‘𝑊)𝑦) = (𝑥( +𝑣 ‘𝑈)𝑦)) |
30 | 29 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))) |
31 | 30 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) = (((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2)) |
32 | 28, 31 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) = (((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2)) |
33 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) |
34 | 6, 33 | nvmcl 26885 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑥( −𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) |
35 | 34 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥( −𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) |
36 | 3, 35 | sylan 487 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥( −𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) |
37 | 6, 15, 24, 2 | sspnval 26976 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ (𝑥( −𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑊)𝑦))) |
38 | 37 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥( −𝑣 ‘𝑊)𝑦) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑊)𝑦))) |
39 | 36, 38 | syldan 486 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑊)𝑦))) |
40 | 6, 14, 33, 2 | sspmval 26972 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (𝑥( −𝑣 ‘𝑊)𝑦) = (𝑥( −𝑣 ‘𝑈)𝑦)) |
41 | 40 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))) |
42 | 39, 41 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦)) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))) |
43 | 42 | oveq1d 6564 |
. . . . . 6
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦))↑2) = (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2)) |
44 | 32, 43 | oveq12d 6567 |
. . . . 5
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) + (((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦))↑2)) =
((((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2) + (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2))) |
45 | 1, 44 | sylanl1 680 |
. . . 4
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) + (((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦))↑2)) =
((((normCV‘𝑈)‘(𝑥( +𝑣 ‘𝑈)𝑦))↑2) + (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑦))↑2))) |
46 | 6, 15, 24, 2 | sspnval 26976 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝑥 ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘𝑥) = ((normCV‘𝑈)‘𝑥)) |
47 | 46 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘𝑥) = ((normCV‘𝑈)‘𝑥)) |
48 | 47 | adantrr 749 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑊)‘𝑥) = ((normCV‘𝑈)‘𝑥)) |
49 | 48 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (((normCV‘𝑊)‘𝑥)↑2) = (((normCV‘𝑈)‘𝑥)↑2)) |
50 | 6, 15, 24, 2 | sspnval 26976 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘𝑦) = ((normCV‘𝑈)‘𝑦)) |
51 | 50 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘𝑦) = ((normCV‘𝑈)‘𝑦)) |
52 | 51 | adantrl 748 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((normCV‘𝑊)‘𝑦) = ((normCV‘𝑈)‘𝑦)) |
53 | 52 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (((normCV‘𝑊)‘𝑦)↑2) = (((normCV‘𝑈)‘𝑦)↑2)) |
54 | 49, 53 | oveq12d 6567 |
. . . . . 6
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((((normCV‘𝑊)‘𝑥)↑2) + (((normCV‘𝑊)‘𝑦)↑2)) =
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2))) |
55 | 1, 54 | sylanl1 680 |
. . . . 5
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((((normCV‘𝑊)‘𝑥)↑2) + (((normCV‘𝑊)‘𝑦)↑2)) =
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2))) |
56 | 55 | oveq2d 6565 |
. . . 4
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → (2 ·
((((normCV‘𝑊)‘𝑥)↑2) + (((normCV‘𝑊)‘𝑦)↑2))) = (2 ·
((((normCV‘𝑈)‘𝑥)↑2) + (((normCV‘𝑈)‘𝑦)↑2)))) |
57 | 19, 45, 56 | 3eqtr4d 2654 |
. . 3
⊢ (((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊))) → ((((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) + (((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦))↑2)) = (2 ·
((((normCV‘𝑊)‘𝑥)↑2) + (((normCV‘𝑊)‘𝑦)↑2)))) |
58 | 57 | ralrimivva 2954 |
. 2
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) → ∀𝑥 ∈ (BaseSet‘𝑊)∀𝑦 ∈ (BaseSet‘𝑊)((((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) + (((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦))↑2)) = (2 ·
((((normCV‘𝑊)‘𝑥)↑2) + (((normCV‘𝑊)‘𝑦)↑2)))) |
59 | 6, 20, 33, 24 | isph 27061 |
. 2
⊢ (𝑊 ∈ CPreHilOLD
↔ (𝑊 ∈ NrmCVec
∧ ∀𝑥 ∈
(BaseSet‘𝑊)∀𝑦 ∈ (BaseSet‘𝑊)((((normCV‘𝑊)‘(𝑥( +𝑣 ‘𝑊)𝑦))↑2) + (((normCV‘𝑊)‘(𝑥( −𝑣 ‘𝑊)𝑦))↑2)) = (2 ·
((((normCV‘𝑊)‘𝑥)↑2) + (((normCV‘𝑊)‘𝑦)↑2))))) |
60 | 4, 58, 59 | sylanbrc 695 |
1
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ 𝐻) → 𝑊 ∈
CPreHilOLD) |