Proof of Theorem isph
| Step | Hyp | Ref
| Expression |
| 1 | | phnv 30833 |
. 2
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
| 2 | | isph.2 |
. . . . 5
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 3 | | eqid 2737 |
. . . . 5
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
| 4 | | isph.6 |
. . . . 5
⊢ 𝑁 =
(normCV‘𝑈) |
| 5 | 2, 3, 4 | nvop 30695 |
. . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉) |
| 6 | | eleq1 2829 |
. . . . 5
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (𝑈 ∈ CPreHilOLD ↔
〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈
CPreHilOLD)) |
| 7 | 2 | fvexi 6920 |
. . . . . . 7
⊢ 𝐺 ∈ V |
| 8 | | fvex 6919 |
. . . . . . 7
⊢ (
·𝑠OLD ‘𝑈) ∈ V |
| 9 | 4 | fvexi 6920 |
. . . . . . 7
⊢ 𝑁 ∈ V |
| 10 | | isph.1 |
. . . . . . . . 9
⊢ 𝑋 = (BaseSet‘𝑈) |
| 11 | 10, 2 | bafval 30623 |
. . . . . . . 8
⊢ 𝑋 = ran 𝐺 |
| 12 | 11 | isphg 30836 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ (
·𝑠OLD ‘𝑈) ∈ V ∧ 𝑁 ∈ V) → (〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ CPreHilOLD ↔
(〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
| 13 | 7, 8, 9, 12 | mp3an 1463 |
. . . . . 6
⊢
(〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ CPreHilOLD ↔
(〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
| 14 | | isph.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = ( −𝑣
‘𝑈) |
| 15 | 10, 2, 3, 14 | nvmval 30661 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑀𝑦) = (𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦))) |
| 16 | 15 | 3expa 1119 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑀𝑦) = (𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦))) |
| 17 | 16 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑥𝑀𝑦)) = (𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))) |
| 18 | 17 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑁‘(𝑥𝑀𝑦))↑2) = ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) |
| 19 | 18 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2))) |
| 20 | 19 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
| 21 | 20 | ralbidva 3176 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
| 22 | 21 | ralbidva 3176 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
| 23 | 22 | pm5.32i 574 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) ↔ (𝑈 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
| 24 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (𝑈 ∈ NrmCVec ↔ 〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec)) |
| 25 | 24 | anbi1d 631 |
. . . . . . 7
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → ((𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) ↔ (〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
| 26 | 23, 25 | bitr2id 284 |
. . . . . 6
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 →
((〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1( ·𝑠OLD
‘𝑈)𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) ↔ (𝑈 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
| 27 | 13, 26 | bitrid 283 |
. . . . 5
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (〈〈𝐺, (
·𝑠OLD ‘𝑈)〉, 𝑁〉 ∈ CPreHilOLD ↔
(𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
| 28 | 6, 27 | bitrd 279 |
. . . 4
⊢ (𝑈 = 〈〈𝐺, ( ·𝑠OLD
‘𝑈)〉, 𝑁〉 → (𝑈 ∈ CPreHilOLD ↔ (𝑈 ∈ NrmCVec ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
| 29 | 5, 28 | syl 17 |
. . 3
⊢ (𝑈 ∈ NrmCVec → (𝑈 ∈ CPreHilOLD
↔ (𝑈 ∈ NrmCVec
∧ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
| 30 | 29 | bianabs 541 |
. 2
⊢ (𝑈 ∈ NrmCVec → (𝑈 ∈ CPreHilOLD
↔ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |
| 31 | 1, 30 | biadanii 822 |
1
⊢ (𝑈 ∈ CPreHilOLD
↔ (𝑈 ∈ NrmCVec
∧ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) |