Step |
Hyp |
Ref |
Expression |
0 |
|
ccphlo |
⊢ CPreHilOLD |
1 |
|
cnv |
⊢ NrmCVec |
2 |
|
vg |
⊢ 𝑔 |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
vn |
⊢ 𝑛 |
5 |
|
vx |
⊢ 𝑥 |
6 |
2
|
cv |
⊢ 𝑔 |
7 |
6
|
crn |
⊢ ran 𝑔 |
8 |
|
vy |
⊢ 𝑦 |
9 |
4
|
cv |
⊢ 𝑛 |
10 |
5
|
cv |
⊢ 𝑥 |
11 |
8
|
cv |
⊢ 𝑦 |
12 |
10 11 6
|
co |
⊢ ( 𝑥 𝑔 𝑦 ) |
13 |
12 9
|
cfv |
⊢ ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) |
14 |
|
cexp |
⊢ ↑ |
15 |
|
c2 |
⊢ 2 |
16 |
13 15 14
|
co |
⊢ ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) |
17 |
|
caddc |
⊢ + |
18 |
|
c1 |
⊢ 1 |
19 |
18
|
cneg |
⊢ - 1 |
20 |
3
|
cv |
⊢ 𝑠 |
21 |
19 11 20
|
co |
⊢ ( - 1 𝑠 𝑦 ) |
22 |
10 21 6
|
co |
⊢ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) |
23 |
22 9
|
cfv |
⊢ ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) |
24 |
23 15 14
|
co |
⊢ ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) |
25 |
16 24 17
|
co |
⊢ ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) |
26 |
|
cmul |
⊢ · |
27 |
10 9
|
cfv |
⊢ ( 𝑛 ‘ 𝑥 ) |
28 |
27 15 14
|
co |
⊢ ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) |
29 |
11 9
|
cfv |
⊢ ( 𝑛 ‘ 𝑦 ) |
30 |
29 15 14
|
co |
⊢ ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) |
31 |
28 30 17
|
co |
⊢ ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) |
32 |
15 31 26
|
co |
⊢ ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) |
33 |
25 32
|
wceq |
⊢ ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) |
34 |
33 8 7
|
wral |
⊢ ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) |
35 |
34 5 7
|
wral |
⊢ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) |
36 |
35 2 3 4
|
coprab |
⊢ { 〈 〈 𝑔 , 𝑠 〉 , 𝑛 〉 ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } |
37 |
1 36
|
cin |
⊢ ( NrmCVec ∩ { 〈 〈 𝑔 , 𝑠 〉 , 𝑛 〉 ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } ) |
38 |
0 37
|
wceq |
⊢ CPreHilOLD = ( NrmCVec ∩ { 〈 〈 𝑔 , 𝑠 〉 , 𝑛 〉 ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } ) |