Detailed syntax breakdown of Definition df-assa
Step | Hyp | Ref
| Expression |
1 | | casa 20668 |
. 2
class
AssAlg |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑓 |
4 | | ccrg 19419 |
. . . . . 6
class
CRing |
5 | 3, 4 | wcel 2114 |
. . . . 5
wff 𝑓 ∈ CRing |
6 | | vr |
. . . . . . . . . . . . . . 15
setvar 𝑟 |
7 | 6 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑟 |
8 | | vx |
. . . . . . . . . . . . . . 15
setvar 𝑥 |
9 | 8 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑥 |
10 | | vs |
. . . . . . . . . . . . . . 15
setvar 𝑠 |
11 | 10 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑠 |
12 | 7, 9, 11 | co 7172 |
. . . . . . . . . . . . 13
class (𝑟𝑠𝑥) |
13 | | vy |
. . . . . . . . . . . . . 14
setvar 𝑦 |
14 | 13 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑦 |
15 | | vt |
. . . . . . . . . . . . . 14
setvar 𝑡 |
16 | 15 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑡 |
17 | 12, 14, 16 | co 7172 |
. . . . . . . . . . . 12
class ((𝑟𝑠𝑥)𝑡𝑦) |
18 | 9, 14, 16 | co 7172 |
. . . . . . . . . . . . 13
class (𝑥𝑡𝑦) |
19 | 7, 18, 11 | co 7172 |
. . . . . . . . . . . 12
class (𝑟𝑠(𝑥𝑡𝑦)) |
20 | 17, 19 | wceq 1542 |
. . . . . . . . . . 11
wff ((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) |
21 | 7, 14, 11 | co 7172 |
. . . . . . . . . . . . 13
class (𝑟𝑠𝑦) |
22 | 9, 21, 16 | co 7172 |
. . . . . . . . . . . 12
class (𝑥𝑡(𝑟𝑠𝑦)) |
23 | 22, 19 | wceq 1542 |
. . . . . . . . . . 11
wff (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) |
24 | 20, 23 | wa 399 |
. . . . . . . . . 10
wff (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
25 | | vw |
. . . . . . . . . . . 12
setvar 𝑤 |
26 | 25 | cv 1541 |
. . . . . . . . . . 11
class 𝑤 |
27 | | cmulr 16671 |
. . . . . . . . . . 11
class
.r |
28 | 26, 27 | cfv 6339 |
. . . . . . . . . 10
class
(.r‘𝑤) |
29 | 24, 15, 28 | wsbc 3680 |
. . . . . . . . 9
wff
[(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
30 | | cvsca 16674 |
. . . . . . . . . 10
class
·𝑠 |
31 | 26, 30 | cfv 6339 |
. . . . . . . . 9
class (
·𝑠 ‘𝑤) |
32 | 29, 10, 31 | wsbc 3680 |
. . . . . . . 8
wff [(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
33 | | cbs 16588 |
. . . . . . . . 9
class
Base |
34 | 26, 33 | cfv 6339 |
. . . . . . . 8
class
(Base‘𝑤) |
35 | 32, 13, 34 | wral 3053 |
. . . . . . 7
wff
∀𝑦 ∈
(Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
36 | 35, 8, 34 | wral 3053 |
. . . . . 6
wff
∀𝑥 ∈
(Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
37 | 3, 33 | cfv 6339 |
. . . . . 6
class
(Base‘𝑓) |
38 | 36, 6, 37 | wral 3053 |
. . . . 5
wff
∀𝑟 ∈
(Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
39 | 5, 38 | wa 399 |
. . . 4
wff (𝑓 ∈ CRing ∧
∀𝑟 ∈
(Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) |
40 | | csca 16673 |
. . . . 5
class
Scalar |
41 | 26, 40 | cfv 6339 |
. . . 4
class
(Scalar‘𝑤) |
42 | 39, 2, 41 | wsbc 3680 |
. . 3
wff
[(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) |
43 | | clmod 19755 |
. . . 4
class
LMod |
44 | | crg 19418 |
. . . 4
class
Ring |
45 | 43, 44 | cin 3842 |
. . 3
class (LMod
∩ Ring) |
46 | 42, 25, 45 | crab 3057 |
. 2
class {𝑤 ∈ (LMod ∩ Ring)
∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))} |
47 | 1, 46 | wceq 1542 |
1
wff AssAlg =
{𝑤 ∈ (LMod ∩ Ring)
∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))} |