Step | Hyp | Ref
| Expression |
1 | | cmg 12982 |
. 2
class
.g |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 2737 |
. . 3
class
V |
4 | | vn |
. . . 4
setvar 𝑛 |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | | cz 9252 |
. . . 4
class
ℤ |
7 | 2 | cv 1352 |
. . . . 5
class 𝑔 |
8 | | cbs 12461 |
. . . . 5
class
Base |
9 | 7, 8 | cfv 5216 |
. . . 4
class
(Base‘𝑔) |
10 | 4 | cv 1352 |
. . . . . 6
class 𝑛 |
11 | | cc0 7810 |
. . . . . 6
class
0 |
12 | 10, 11 | wceq 1353 |
. . . . 5
wff 𝑛 = 0 |
13 | | c0g 12704 |
. . . . . 6
class
0g |
14 | 7, 13 | cfv 5216 |
. . . . 5
class
(0g‘𝑔) |
15 | | vs |
. . . . . 6
setvar 𝑠 |
16 | | cplusg 12535 |
. . . . . . . 8
class
+g |
17 | 7, 16 | cfv 5216 |
. . . . . . 7
class
(+g‘𝑔) |
18 | | cn 8918 |
. . . . . . . 8
class
ℕ |
19 | 5 | cv 1352 |
. . . . . . . . 9
class 𝑥 |
20 | 19 | csn 3592 |
. . . . . . . 8
class {𝑥} |
21 | 18, 20 | cxp 4624 |
. . . . . . 7
class (ℕ
× {𝑥}) |
22 | | c1 7811 |
. . . . . . 7
class
1 |
23 | 17, 21, 22 | cseq 10444 |
. . . . . 6
class
seq1((+g‘𝑔), (ℕ × {𝑥})) |
24 | | clt 7991 |
. . . . . . . 8
class
< |
25 | 11, 10, 24 | wbr 4003 |
. . . . . . 7
wff 0 <
𝑛 |
26 | 15 | cv 1352 |
. . . . . . . 8
class 𝑠 |
27 | 10, 26 | cfv 5216 |
. . . . . . 7
class (𝑠‘𝑛) |
28 | 10 | cneg 8128 |
. . . . . . . . 9
class -𝑛 |
29 | 28, 26 | cfv 5216 |
. . . . . . . 8
class (𝑠‘-𝑛) |
30 | | cminusg 12877 |
. . . . . . . . 9
class
invg |
31 | 7, 30 | cfv 5216 |
. . . . . . . 8
class
(invg‘𝑔) |
32 | 29, 31 | cfv 5216 |
. . . . . . 7
class
((invg‘𝑔)‘(𝑠‘-𝑛)) |
33 | 25, 27, 32 | cif 3534 |
. . . . . 6
class if(0 <
𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))) |
34 | 15, 23, 33 | csb 3057 |
. . . . 5
class
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))) |
35 | 12, 14, 34 | cif 3534 |
. . . 4
class if(𝑛 = 0, (0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))) |
36 | 4, 5, 6, 9, 35 | cmpo 5876 |
. . 3
class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))) |
37 | 2, 3, 36 | cmpt 4064 |
. 2
class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))) |
38 | 1, 37 | wceq 1353 |
1
wff
.g = (𝑔
∈ V ↦ (𝑛 ∈
ℤ, 𝑥 ∈
(Base‘𝑔) ↦
if(𝑛 = 0,
(0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))) |