Detailed syntax breakdown of Definition df-srg
Step | Hyp | Ref
| Expression |
1 | | csrg 19374 |
. 2
class
SRing |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑓 |
4 | | cmgp 19358 |
. . . . . 6
class
mulGrp |
5 | 3, 4 | cfv 6339 |
. . . . 5
class
(mulGrp‘𝑓) |
6 | | cmnd 18027 |
. . . . 5
class
Mnd |
7 | 5, 6 | wcel 2114 |
. . . 4
wff
(mulGrp‘𝑓)
∈ Mnd |
8 | | vx |
. . . . . . . . . . . . . . . 16
setvar 𝑥 |
9 | 8 | cv 1541 |
. . . . . . . . . . . . . . 15
class 𝑥 |
10 | | vy |
. . . . . . . . . . . . . . . . 17
setvar 𝑦 |
11 | 10 | cv 1541 |
. . . . . . . . . . . . . . . 16
class 𝑦 |
12 | | vz |
. . . . . . . . . . . . . . . . 17
setvar 𝑧 |
13 | 12 | cv 1541 |
. . . . . . . . . . . . . . . 16
class 𝑧 |
14 | | vp |
. . . . . . . . . . . . . . . . 17
setvar 𝑝 |
15 | 14 | cv 1541 |
. . . . . . . . . . . . . . . 16
class 𝑝 |
16 | 11, 13, 15 | co 7170 |
. . . . . . . . . . . . . . 15
class (𝑦𝑝𝑧) |
17 | | vt |
. . . . . . . . . . . . . . . 16
setvar 𝑡 |
18 | 17 | cv 1541 |
. . . . . . . . . . . . . . 15
class 𝑡 |
19 | 9, 16, 18 | co 7170 |
. . . . . . . . . . . . . 14
class (𝑥𝑡(𝑦𝑝𝑧)) |
20 | 9, 11, 18 | co 7170 |
. . . . . . . . . . . . . . 15
class (𝑥𝑡𝑦) |
21 | 9, 13, 18 | co 7170 |
. . . . . . . . . . . . . . 15
class (𝑥𝑡𝑧) |
22 | 20, 21, 15 | co 7170 |
. . . . . . . . . . . . . 14
class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) |
23 | 19, 22 | wceq 1542 |
. . . . . . . . . . . . 13
wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) |
24 | 9, 11, 15 | co 7170 |
. . . . . . . . . . . . . . 15
class (𝑥𝑝𝑦) |
25 | 24, 13, 18 | co 7170 |
. . . . . . . . . . . . . 14
class ((𝑥𝑝𝑦)𝑡𝑧) |
26 | 11, 13, 18 | co 7170 |
. . . . . . . . . . . . . . 15
class (𝑦𝑡𝑧) |
27 | 21, 26, 15 | co 7170 |
. . . . . . . . . . . . . 14
class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) |
28 | 25, 27 | wceq 1542 |
. . . . . . . . . . . . 13
wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) |
29 | 23, 28 | wa 399 |
. . . . . . . . . . . 12
wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) |
30 | | vr |
. . . . . . . . . . . . 13
setvar 𝑟 |
31 | 30 | cv 1541 |
. . . . . . . . . . . 12
class 𝑟 |
32 | 29, 12, 31 | wral 3053 |
. . . . . . . . . . 11
wff
∀𝑧 ∈
𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) |
33 | 32, 10, 31 | wral 3053 |
. . . . . . . . . 10
wff
∀𝑦 ∈
𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) |
34 | | vn |
. . . . . . . . . . . . . 14
setvar 𝑛 |
35 | 34 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑛 |
36 | 35, 9, 18 | co 7170 |
. . . . . . . . . . . 12
class (𝑛𝑡𝑥) |
37 | 36, 35 | wceq 1542 |
. . . . . . . . . . 11
wff (𝑛𝑡𝑥) = 𝑛 |
38 | 9, 35, 18 | co 7170 |
. . . . . . . . . . . 12
class (𝑥𝑡𝑛) |
39 | 38, 35 | wceq 1542 |
. . . . . . . . . . 11
wff (𝑥𝑡𝑛) = 𝑛 |
40 | 37, 39 | wa 399 |
. . . . . . . . . 10
wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛) |
41 | 33, 40 | wa 399 |
. . . . . . . . 9
wff
(∀𝑦 ∈
𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) |
42 | 41, 8, 31 | wral 3053 |
. . . . . . . 8
wff
∀𝑥 ∈
𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) |
43 | | c0g 16816 |
. . . . . . . . 9
class
0g |
44 | 3, 43 | cfv 6339 |
. . . . . . . 8
class
(0g‘𝑓) |
45 | 42, 34, 44 | wsbc 3680 |
. . . . . . 7
wff
[(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) |
46 | | cmulr 16669 |
. . . . . . . 8
class
.r |
47 | 3, 46 | cfv 6339 |
. . . . . . 7
class
(.r‘𝑓) |
48 | 45, 17, 47 | wsbc 3680 |
. . . . . 6
wff
[(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) |
49 | | cplusg 16668 |
. . . . . . 7
class
+g |
50 | 3, 49 | cfv 6339 |
. . . . . 6
class
(+g‘𝑓) |
51 | 48, 14, 50 | wsbc 3680 |
. . . . 5
wff
[(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) |
52 | | cbs 16586 |
. . . . . 6
class
Base |
53 | 3, 52 | cfv 6339 |
. . . . 5
class
(Base‘𝑓) |
54 | 51, 30, 53 | wsbc 3680 |
. . . 4
wff
[(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) |
55 | 7, 54 | wa 399 |
. . 3
wff
((mulGrp‘𝑓)
∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))) |
56 | | ccmn 19024 |
. . 3
class
CMnd |
57 | 55, 2, 56 | crab 3057 |
. 2
class {𝑓 ∈ CMnd ∣
((mulGrp‘𝑓) ∈
Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))} |
58 | 1, 57 | wceq 1542 |
1
wff SRing =
{𝑓 ∈ CMnd ∣
((mulGrp‘𝑓) ∈
Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))} |