Detailed syntax breakdown of Definition df-zlm
Step | Hyp | Ref
| Expression |
1 | | czlm 20700 |
. 2
class
ℤMod |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3431 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . . 5
class 𝑔 |
5 | | cnx 16892 |
. . . . . . 7
class
ndx |
6 | | csca 16963 |
. . . . . . 7
class
Scalar |
7 | 5, 6 | cfv 6432 |
. . . . . 6
class
(Scalar‘ndx) |
8 | | czring 20668 |
. . . . . 6
class
ℤring |
9 | 7, 8 | cop 4573 |
. . . . 5
class
〈(Scalar‘ndx), ℤring〉 |
10 | | csts 16862 |
. . . . 5
class
sSet |
11 | 4, 9, 10 | co 7271 |
. . . 4
class (𝑔 sSet 〈(Scalar‘ndx),
ℤring〉) |
12 | | cvsca 16964 |
. . . . . 6
class
·𝑠 |
13 | 5, 12 | cfv 6432 |
. . . . 5
class (
·𝑠 ‘ndx) |
14 | | cmg 18698 |
. . . . . 6
class
.g |
15 | 4, 14 | cfv 6432 |
. . . . 5
class
(.g‘𝑔) |
16 | 13, 15 | cop 4573 |
. . . 4
class 〈(
·𝑠 ‘ndx), (.g‘𝑔)〉 |
17 | 11, 16, 10 | co 7271 |
. . 3
class ((𝑔 sSet 〈(Scalar‘ndx),
ℤring〉) sSet 〈( ·𝑠
‘ndx), (.g‘𝑔)〉) |
18 | 2, 3, 17 | cmpt 5162 |
. 2
class (𝑔 ∈ V ↦ ((𝑔 sSet 〈(Scalar‘ndx),
ℤring〉) sSet 〈( ·𝑠
‘ndx), (.g‘𝑔)〉)) |
19 | 1, 18 | wceq 1542 |
1
wff ℤMod
= (𝑔 ∈ V ↦
((𝑔 sSet
〈(Scalar‘ndx), ℤring〉) sSet 〈(
·𝑠 ‘ndx), (.g‘𝑔)〉)) |