Detailed syntax breakdown of Definition df-mulg
Step | Hyp | Ref
| Expression |
1 | | cmg 18488 |
. 2
class
.g |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vn |
. . . 4
setvar 𝑛 |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | | cz 12176 |
. . . 4
class
ℤ |
7 | 2 | cv 1542 |
. . . . 5
class 𝑔 |
8 | | cbs 16760 |
. . . . 5
class
Base |
9 | 7, 8 | cfv 6380 |
. . . 4
class
(Base‘𝑔) |
10 | 4 | cv 1542 |
. . . . . 6
class 𝑛 |
11 | | cc0 10729 |
. . . . . 6
class
0 |
12 | 10, 11 | wceq 1543 |
. . . . 5
wff 𝑛 = 0 |
13 | | c0g 16944 |
. . . . . 6
class
0g |
14 | 7, 13 | cfv 6380 |
. . . . 5
class
(0g‘𝑔) |
15 | | vs |
. . . . . 6
setvar 𝑠 |
16 | | cplusg 16802 |
. . . . . . . 8
class
+g |
17 | 7, 16 | cfv 6380 |
. . . . . . 7
class
(+g‘𝑔) |
18 | | cn 11830 |
. . . . . . . 8
class
ℕ |
19 | 5 | cv 1542 |
. . . . . . . . 9
class 𝑥 |
20 | 19 | csn 4541 |
. . . . . . . 8
class {𝑥} |
21 | 18, 20 | cxp 5549 |
. . . . . . 7
class (ℕ
× {𝑥}) |
22 | | c1 10730 |
. . . . . . 7
class
1 |
23 | 17, 21, 22 | cseq 13574 |
. . . . . 6
class
seq1((+g‘𝑔), (ℕ × {𝑥})) |
24 | | clt 10867 |
. . . . . . . 8
class
< |
25 | 11, 10, 24 | wbr 5053 |
. . . . . . 7
wff 0 <
𝑛 |
26 | 15 | cv 1542 |
. . . . . . . 8
class 𝑠 |
27 | 10, 26 | cfv 6380 |
. . . . . . 7
class (𝑠‘𝑛) |
28 | 10 | cneg 11063 |
. . . . . . . . 9
class -𝑛 |
29 | 28, 26 | cfv 6380 |
. . . . . . . 8
class (𝑠‘-𝑛) |
30 | | cminusg 18366 |
. . . . . . . . 9
class
invg |
31 | 7, 30 | cfv 6380 |
. . . . . . . 8
class
(invg‘𝑔) |
32 | 29, 31 | cfv 6380 |
. . . . . . 7
class
((invg‘𝑔)‘(𝑠‘-𝑛)) |
33 | 25, 27, 32 | cif 4439 |
. . . . . 6
class if(0 <
𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))) |
34 | 15, 23, 33 | csb 3811 |
. . . . 5
class
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))) |
35 | 12, 14, 34 | cif 4439 |
. . . 4
class if(𝑛 = 0, (0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))) |
36 | 4, 5, 6, 9, 35 | cmpo 7215 |
. . 3
class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))) |
37 | 2, 3, 36 | cmpt 5135 |
. 2
class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))) |
38 | 1, 37 | wceq 1543 |
1
wff
.g = (𝑔
∈ V ↦ (𝑛 ∈
ℤ, 𝑥 ∈
(Base‘𝑔) ↦
if(𝑛 = 0,
(0g‘𝑔),
⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))) |