Detailed syntax breakdown of Definition df-ph
Step | Hyp | Ref
| Expression |
1 | | ccphlo 28759 |
. 2
class
CPreHilOLD |
2 | | cnv 28531 |
. . 3
class
NrmCVec |
3 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
4 | 3 | cv 1541 |
. . . . . . . . . . 11
class 𝑥 |
5 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
6 | 5 | cv 1541 |
. . . . . . . . . . 11
class 𝑦 |
7 | | vg |
. . . . . . . . . . . 12
setvar 𝑔 |
8 | 7 | cv 1541 |
. . . . . . . . . . 11
class 𝑔 |
9 | 4, 6, 8 | co 7182 |
. . . . . . . . . 10
class (𝑥𝑔𝑦) |
10 | | vn |
. . . . . . . . . . 11
setvar 𝑛 |
11 | 10 | cv 1541 |
. . . . . . . . . 10
class 𝑛 |
12 | 9, 11 | cfv 6349 |
. . . . . . . . 9
class (𝑛‘(𝑥𝑔𝑦)) |
13 | | c2 11783 |
. . . . . . . . 9
class
2 |
14 | | cexp 13533 |
. . . . . . . . 9
class
↑ |
15 | 12, 13, 14 | co 7182 |
. . . . . . . 8
class ((𝑛‘(𝑥𝑔𝑦))↑2) |
16 | | c1 10628 |
. . . . . . . . . . . . 13
class
1 |
17 | 16 | cneg 10961 |
. . . . . . . . . . . 12
class
-1 |
18 | | vs |
. . . . . . . . . . . . 13
setvar 𝑠 |
19 | 18 | cv 1541 |
. . . . . . . . . . . 12
class 𝑠 |
20 | 17, 6, 19 | co 7182 |
. . . . . . . . . . 11
class (-1𝑠𝑦) |
21 | 4, 20, 8 | co 7182 |
. . . . . . . . . 10
class (𝑥𝑔(-1𝑠𝑦)) |
22 | 21, 11 | cfv 6349 |
. . . . . . . . 9
class (𝑛‘(𝑥𝑔(-1𝑠𝑦))) |
23 | 22, 13, 14 | co 7182 |
. . . . . . . 8
class ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2) |
24 | | caddc 10630 |
. . . . . . . 8
class
+ |
25 | 15, 23, 24 | co 7182 |
. . . . . . 7
class (((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) |
26 | 4, 11 | cfv 6349 |
. . . . . . . . . 10
class (𝑛‘𝑥) |
27 | 26, 13, 14 | co 7182 |
. . . . . . . . 9
class ((𝑛‘𝑥)↑2) |
28 | 6, 11 | cfv 6349 |
. . . . . . . . . 10
class (𝑛‘𝑦) |
29 | 28, 13, 14 | co 7182 |
. . . . . . . . 9
class ((𝑛‘𝑦)↑2) |
30 | 27, 29, 24 | co 7182 |
. . . . . . . 8
class (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)) |
31 | | cmul 10632 |
. . . . . . . 8
class
· |
32 | 13, 30, 31 | co 7182 |
. . . . . . 7
class (2
· (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2))) |
33 | 25, 32 | wceq 1542 |
. . . . . 6
wff (((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2))) |
34 | 8 | crn 5536 |
. . . . . 6
class ran 𝑔 |
35 | 33, 5, 34 | wral 3054 |
. . . . 5
wff
∀𝑦 ∈ ran
𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2))) |
36 | 35, 3, 34 | wral 3054 |
. . . 4
wff
∀𝑥 ∈ ran
𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2))) |
37 | 36, 7, 18, 10 | coprab 7183 |
. . 3
class
{〈〈𝑔,
𝑠〉, 𝑛〉 ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))} |
38 | 2, 37 | cin 3852 |
. 2
class (NrmCVec
∩ {〈〈𝑔, 𝑠〉, 𝑛〉 ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}) |
39 | 1, 38 | wceq 1542 |
1
wff
CPreHilOLD = (NrmCVec ∩ {〈〈𝑔, 𝑠〉, 𝑛〉 ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}) |