Detailed syntax breakdown of Definition df-assa
Step | Hyp | Ref
| Expression |
1 | | casa 21338 |
. 2
class
AssAlg |
2 | | vr |
. . . . . . . . . . . . . 14
setvar 𝑟 |
3 | 2 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑟 |
4 | | vx |
. . . . . . . . . . . . . 14
setvar 𝑥 |
5 | 4 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑥 |
6 | | vs |
. . . . . . . . . . . . . 14
setvar 𝑠 |
7 | 6 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑠 |
8 | 3, 5, 7 | co 7393 |
. . . . . . . . . . . 12
class (𝑟𝑠𝑥) |
9 | | vy |
. . . . . . . . . . . . 13
setvar 𝑦 |
10 | 9 | cv 1540 |
. . . . . . . . . . . 12
class 𝑦 |
11 | | vt |
. . . . . . . . . . . . 13
setvar 𝑡 |
12 | 11 | cv 1540 |
. . . . . . . . . . . 12
class 𝑡 |
13 | 8, 10, 12 | co 7393 |
. . . . . . . . . . 11
class ((𝑟𝑠𝑥)𝑡𝑦) |
14 | 5, 10, 12 | co 7393 |
. . . . . . . . . . . 12
class (𝑥𝑡𝑦) |
15 | 3, 14, 7 | co 7393 |
. . . . . . . . . . 11
class (𝑟𝑠(𝑥𝑡𝑦)) |
16 | 13, 15 | wceq 1541 |
. . . . . . . . . 10
wff ((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) |
17 | 3, 10, 7 | co 7393 |
. . . . . . . . . . . 12
class (𝑟𝑠𝑦) |
18 | 5, 17, 12 | co 7393 |
. . . . . . . . . . 11
class (𝑥𝑡(𝑟𝑠𝑦)) |
19 | 18, 15 | wceq 1541 |
. . . . . . . . . 10
wff (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) |
20 | 16, 19 | wa 396 |
. . . . . . . . 9
wff (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
21 | | vw |
. . . . . . . . . . 11
setvar 𝑤 |
22 | 21 | cv 1540 |
. . . . . . . . . 10
class 𝑤 |
23 | | cmulr 17180 |
. . . . . . . . . 10
class
.r |
24 | 22, 23 | cfv 6532 |
. . . . . . . . 9
class
(.r‘𝑤) |
25 | 20, 11, 24 | wsbc 3773 |
. . . . . . . 8
wff
[(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
26 | | cvsca 17183 |
. . . . . . . . 9
class
·𝑠 |
27 | 22, 26 | cfv 6532 |
. . . . . . . 8
class (
·𝑠 ‘𝑤) |
28 | 25, 6, 27 | wsbc 3773 |
. . . . . . 7
wff [(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
29 | | cbs 17126 |
. . . . . . . 8
class
Base |
30 | 22, 29 | cfv 6532 |
. . . . . . 7
class
(Base‘𝑤) |
31 | 28, 9, 30 | wral 3060 |
. . . . . 6
wff
∀𝑦 ∈
(Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
32 | 31, 4, 30 | wral 3060 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
33 | | vf |
. . . . . . 7
setvar 𝑓 |
34 | 33 | cv 1540 |
. . . . . 6
class 𝑓 |
35 | 34, 29 | cfv 6532 |
. . . . 5
class
(Base‘𝑓) |
36 | 32, 2, 35 | wral 3060 |
. . . 4
wff
∀𝑟 ∈
(Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
37 | | csca 17182 |
. . . . 5
class
Scalar |
38 | 22, 37 | cfv 6532 |
. . . 4
class
(Scalar‘𝑤) |
39 | 36, 33, 38 | wsbc 3773 |
. . 3
wff
[(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) |
40 | | clmod 20420 |
. . . 4
class
LMod |
41 | | crg 20014 |
. . . 4
class
Ring |
42 | 40, 41 | cin 3943 |
. . 3
class (LMod
∩ Ring) |
43 | 39, 21, 42 | crab 3431 |
. 2
class {𝑤 ∈ (LMod ∩ Ring)
∣ [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))} |
44 | 1, 43 | wceq 1541 |
1
wff AssAlg =
{𝑤 ∈ (LMod ∩ Ring)
∣ [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))} |