Step | Hyp | Ref
| Expression |
1 | | czlm 21049 |
. 2
class
ℤMod |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3474 |
. . 3
class
V |
4 | 2 | cv 1540 |
. . . . 5
class 𝑔 |
5 | | cnx 17125 |
. . . . . . 7
class
ndx |
6 | | csca 17199 |
. . . . . . 7
class
Scalar |
7 | 5, 6 | cfv 6543 |
. . . . . 6
class
(Scalar‘ndx) |
8 | | czring 21016 |
. . . . . 6
class
ℤring |
9 | 7, 8 | cop 4634 |
. . . . 5
class
⟨(Scalar‘ndx), ℤring⟩ |
10 | | csts 17095 |
. . . . 5
class
sSet |
11 | 4, 9, 10 | co 7408 |
. . . 4
class (𝑔 sSet ⟨(Scalar‘ndx),
ℤring⟩) |
12 | | cvsca 17200 |
. . . . . 6
class
·𝑠 |
13 | 5, 12 | cfv 6543 |
. . . . 5
class (
·𝑠 ‘ndx) |
14 | | cmg 18949 |
. . . . . 6
class
.g |
15 | 4, 14 | cfv 6543 |
. . . . 5
class
(.g‘𝑔) |
16 | 13, 15 | cop 4634 |
. . . 4
class ⟨(
·𝑠 ‘ndx), (.g‘𝑔)⟩ |
17 | 11, 16, 10 | co 7408 |
. . 3
class ((𝑔 sSet ⟨(Scalar‘ndx),
ℤring⟩) sSet ⟨( ·𝑠
‘ndx), (.g‘𝑔)⟩) |
18 | 2, 3, 17 | cmpt 5231 |
. 2
class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx),
ℤring⟩) sSet ⟨( ·𝑠
‘ndx), (.g‘𝑔)⟩)) |
19 | 1, 18 | wceq 1541 |
1
wff ℤMod
= (𝑔 ∈ V ↦
((𝑔 sSet
⟨(Scalar‘ndx), ℤring⟩) sSet ⟨(
·𝑠 ‘ndx), (.g‘𝑔)⟩)) |