Proof of Theorem isph
Step | Hyp | Ref
| Expression |
1 | | phnv 27053 |
. 2
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
2 | | isph.2 |
. . . . 5
⊢ 𝐺 = ( +𝑣
‘𝑈) |
3 | | eqid 2610 |
. . . . 5
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
4 | | isph.6 |
. . . . 5
⊢ 𝑁 =
(normCV‘𝑈) |
5 | 2, 3, 4 | nvop 26915 |
. . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉) |
6 | | eleq1 2676 |
. . . . 5
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (𝑈 ∈ CPreHilOLD ↔
〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈
CPreHilOLD)) |
7 | | fvex 6113 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑈) ∈ V |
8 | 2, 7 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐺 ∈ V |
9 | | fvex 6113 |
. . . . . . 7
⊢ (
·𝑠OLD ‘𝑈) ∈ V |
10 | | fvex 6113 |
. . . . . . . 8
⊢
(normCV‘𝑈) ∈ V |
11 | 4, 10 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑁 ∈ V |
12 | | isph.1 |
. . . . . . . . 9
⊢ 𝑋 = (BaseSet‘𝑈) |
13 | 12, 2 | bafval 26843 |
. . . . . . . 8
⊢ 𝑋 = ran 𝐺 |
14 | 13 | isphg 27056 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ (
·𝑠OLD ‘𝑈) ∈ V ∧ 𝑁 ∈ V) → (〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ CPreHilOLD ↔
(〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
15 | 8, 9, 11, 14 | mp3an 1416 |
. . . . . 6
⊢
(〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ CPreHilOLD ↔
(〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
16 | | isph.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = ( −𝑣
‘𝑈) |
17 | 12, 2, 3, 16 | nvmval 26881 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑀𝑦) = (𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦))) |
18 | 17 | 3expa 1257 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑀𝑦) = (𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦))) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑥𝑀𝑦)) = (𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))) |
20 | 19 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑁‘(𝑥𝑀𝑦))↑2) = ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) |
21 | 20 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2))) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
23 | 22 | ralbidva 2968 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
24 | 23 | ralbidva 2968 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
25 | 24 | pm5.32i 667 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) ↔ (𝑈 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
26 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (𝑈 ∈ NrmCVec ↔ 〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec)) |
27 | 26 | anbi1d 737 |
. . . . . . 7
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → ((𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) ↔ (〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
28 | 25, 27 | syl5rbb 272 |
. . . . . 6
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 →
((〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) ↔ (𝑈 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
29 | 15, 28 | syl5bb 271 |
. . . . 5
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ CPreHilOLD ↔
(𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
30 | 6, 29 | bitrd 267 |
. . . 4
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (𝑈 ∈ CPreHilOLD ↔ (𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
31 | 5, 30 | syl 17 |
. . 3
⊢ (𝑈 ∈ NrmCVec → (𝑈 ∈ CPreHilOLD
↔ (𝑈 ∈ NrmCVec
∧ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
32 | 31 | bianabs 920 |
. 2
⊢ (𝑈 ∈ NrmCVec → (𝑈 ∈ CPreHilOLD
↔ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
33 | 1, 32 | biadan2 672 |
1
⊢ (𝑈 ∈ CPreHilOLD
↔ (𝑈 ∈ NrmCVec
∧ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |