Step | Hyp | Ref
| Expression |
1 | | phpar.2 |
. . . . . . 7
⊢ 𝐺 = ( +𝑣
‘𝑈) |
2 | 1 | vafval 27458 |
. . . . . 6
⊢ 𝐺 = (1st
‘(1st ‘𝑈)) |
3 | | fvex 6201 |
. . . . . 6
⊢
(1st ‘(1st ‘𝑈)) ∈ V |
4 | 2, 3 | eqeltri 2697 |
. . . . 5
⊢ 𝐺 ∈ V |
5 | | phpar.4 |
. . . . . . 7
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
6 | 5 | smfval 27460 |
. . . . . 6
⊢ 𝑆 = (2nd
‘(1st ‘𝑈)) |
7 | | fvex 6201 |
. . . . . 6
⊢
(2nd ‘(1st ‘𝑈)) ∈ V |
8 | 6, 7 | eqeltri 2697 |
. . . . 5
⊢ 𝑆 ∈ V |
9 | | phpar.6 |
. . . . . . 7
⊢ 𝑁 =
(normCV‘𝑈) |
10 | 9 | nmcvfval 27462 |
. . . . . 6
⊢ 𝑁 = (2nd ‘𝑈) |
11 | | fvex 6201 |
. . . . . 6
⊢
(2nd ‘𝑈) ∈ V |
12 | 10, 11 | eqeltri 2697 |
. . . . 5
⊢ 𝑁 ∈ V |
13 | 4, 8, 12 | 3pm3.2i 1239 |
. . . 4
⊢ (𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) |
14 | 1, 5, 9 | phop 27673 |
. . . . . 6
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 =
〈〈𝐺, 𝑆〉, 𝑁〉) |
15 | 14 | eleq1d 2686 |
. . . . 5
⊢ (𝑈 ∈ CPreHilOLD
→ (𝑈 ∈
CPreHilOLD ↔ 〈〈𝐺, 𝑆〉, 𝑁〉 ∈
CPreHilOLD)) |
16 | 15 | ibi 256 |
. . . 4
⊢ (𝑈 ∈ CPreHilOLD
→ 〈〈𝐺, 𝑆〉, 𝑁〉 ∈
CPreHilOLD) |
17 | | phpar.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
18 | 17, 1 | bafval 27459 |
. . . . . 6
⊢ 𝑋 = ran 𝐺 |
19 | 18 | isphg 27672 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) →
(〈〈𝐺, 𝑆〉, 𝑁〉 ∈ CPreHilOLD ↔
(〈〈𝐺, 𝑆〉, 𝑁〉 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) |
20 | 19 | simplbda 654 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) ∧
〈〈𝐺, 𝑆〉, 𝑁〉 ∈ CPreHilOLD) →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) |
21 | 13, 16, 20 | sylancr 695 |
. . 3
⊢ (𝑈 ∈ CPreHilOLD
→ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) |
22 | 21 | 3ad2ant1 1082 |
. 2
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))) |
23 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥𝐺𝑦) = (𝐴𝐺𝑦)) |
24 | 23 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑁‘(𝑥𝐺𝑦)) = (𝑁‘(𝐴𝐺𝑦))) |
25 | 24 | oveq1d 6665 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑁‘(𝑥𝐺𝑦))↑2) = ((𝑁‘(𝐴𝐺𝑦))↑2)) |
26 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥𝐺(-1𝑆𝑦)) = (𝐴𝐺(-1𝑆𝑦))) |
27 | 26 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑁‘(𝑥𝐺(-1𝑆𝑦))) = (𝑁‘(𝐴𝐺(-1𝑆𝑦)))) |
28 | 27 | oveq1d 6665 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2) = ((𝑁‘(𝐴𝐺(-1𝑆𝑦)))↑2)) |
29 | 25, 28 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (((𝑁‘(𝐴𝐺𝑦))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝑦)))↑2))) |
30 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑁‘𝑥) = (𝑁‘𝐴)) |
31 | 30 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑁‘𝑥)↑2) = ((𝑁‘𝐴)↑2)) |
32 | 31 | oveq1d 6665 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝑦)↑2))) |
33 | 32 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝐴 → (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝑦)↑2)))) |
34 | 29, 33 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝐴 → ((((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) ↔ (((𝑁‘(𝐴𝐺𝑦))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝑦)↑2))))) |
35 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴𝐺𝑦) = (𝐴𝐺𝐵)) |
36 | 35 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑁‘(𝐴𝐺𝑦)) = (𝑁‘(𝐴𝐺𝐵))) |
37 | 36 | oveq1d 6665 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑁‘(𝐴𝐺𝑦))↑2) = ((𝑁‘(𝐴𝐺𝐵))↑2)) |
38 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (-1𝑆𝑦) = (-1𝑆𝐵)) |
39 | 38 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴𝐺(-1𝑆𝑦)) = (𝐴𝐺(-1𝑆𝐵))) |
40 | 39 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑁‘(𝐴𝐺(-1𝑆𝑦))) = (𝑁‘(𝐴𝐺(-1𝑆𝐵)))) |
41 | 40 | oveq1d 6665 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑁‘(𝐴𝐺(-1𝑆𝑦)))↑2) = ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) |
42 | 37, 41 | oveq12d 6668 |
. . . . 5
⊢ (𝑦 = 𝐵 → (((𝑁‘(𝐴𝐺𝑦))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝑦)))↑2)) = (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2))) |
43 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑁‘𝑦) = (𝑁‘𝐵)) |
44 | 43 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝑁‘𝑦)↑2) = ((𝑁‘𝐵)↑2)) |
45 | 44 | oveq2d 6666 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (((𝑁‘𝐴)↑2) + ((𝑁‘𝑦)↑2)) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))) |
46 | 45 | oveq2d 6666 |
. . . . 5
⊢ (𝑦 = 𝐵 → (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝑦)↑2))) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) |
47 | 42, 46 | eqeq12d 2637 |
. . . 4
⊢ (𝑦 = 𝐵 → ((((𝑁‘(𝐴𝐺𝑦))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝑦)↑2))) ↔ (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))) |
48 | 34, 47 | rspc2v 3322 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))) |
49 | 48 | 3adant1 1079 |
. 2
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))) |
50 | 22, 49 | mpd 15 |
1
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) |