Detailed syntax breakdown of Definition df-vc
Step | Hyp | Ref
| Expression |
1 | | cvc 28899 |
. 2
class
CVecOLD |
2 | | vg |
. . . . . 6
setvar 𝑔 |
3 | 2 | cv 1540 |
. . . . 5
class 𝑔 |
4 | | cablo 28885 |
. . . . 5
class
AbelOp |
5 | 3, 4 | wcel 2109 |
. . . 4
wff 𝑔 ∈ AbelOp |
6 | | cc 10853 |
. . . . . 6
class
ℂ |
7 | 3 | crn 5589 |
. . . . . 6
class ran 𝑔 |
8 | 6, 7 | cxp 5586 |
. . . . 5
class (ℂ
× ran 𝑔) |
9 | | vs |
. . . . . 6
setvar 𝑠 |
10 | 9 | cv 1540 |
. . . . 5
class 𝑠 |
11 | 8, 7, 10 | wf 6426 |
. . . 4
wff 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 |
12 | | c1 10856 |
. . . . . . . 8
class
1 |
13 | | vx |
. . . . . . . . 9
setvar 𝑥 |
14 | 13 | cv 1540 |
. . . . . . . 8
class 𝑥 |
15 | 12, 14, 10 | co 7268 |
. . . . . . 7
class (1𝑠𝑥) |
16 | 15, 14 | wceq 1541 |
. . . . . 6
wff (1𝑠𝑥) = 𝑥 |
17 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
18 | 17 | cv 1540 |
. . . . . . . . . . 11
class 𝑦 |
19 | | vz |
. . . . . . . . . . . . 13
setvar 𝑧 |
20 | 19 | cv 1540 |
. . . . . . . . . . . 12
class 𝑧 |
21 | 14, 20, 3 | co 7268 |
. . . . . . . . . . 11
class (𝑥𝑔𝑧) |
22 | 18, 21, 10 | co 7268 |
. . . . . . . . . 10
class (𝑦𝑠(𝑥𝑔𝑧)) |
23 | 18, 14, 10 | co 7268 |
. . . . . . . . . . 11
class (𝑦𝑠𝑥) |
24 | 18, 20, 10 | co 7268 |
. . . . . . . . . . 11
class (𝑦𝑠𝑧) |
25 | 23, 24, 3 | co 7268 |
. . . . . . . . . 10
class ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) |
26 | 22, 25 | wceq 1541 |
. . . . . . . . 9
wff (𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) |
27 | 26, 19, 7 | wral 3065 |
. . . . . . . 8
wff
∀𝑧 ∈ ran
𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) |
28 | | caddc 10858 |
. . . . . . . . . . . . 13
class
+ |
29 | 18, 20, 28 | co 7268 |
. . . . . . . . . . . 12
class (𝑦 + 𝑧) |
30 | 29, 14, 10 | co 7268 |
. . . . . . . . . . 11
class ((𝑦 + 𝑧)𝑠𝑥) |
31 | 20, 14, 10 | co 7268 |
. . . . . . . . . . . 12
class (𝑧𝑠𝑥) |
32 | 23, 31, 3 | co 7268 |
. . . . . . . . . . 11
class ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) |
33 | 30, 32 | wceq 1541 |
. . . . . . . . . 10
wff ((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) |
34 | | cmul 10860 |
. . . . . . . . . . . . 13
class
· |
35 | 18, 20, 34 | co 7268 |
. . . . . . . . . . . 12
class (𝑦 · 𝑧) |
36 | 35, 14, 10 | co 7268 |
. . . . . . . . . . 11
class ((𝑦 · 𝑧)𝑠𝑥) |
37 | 18, 31, 10 | co 7268 |
. . . . . . . . . . 11
class (𝑦𝑠(𝑧𝑠𝑥)) |
38 | 36, 37 | wceq 1541 |
. . . . . . . . . 10
wff ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)) |
39 | 33, 38 | wa 395 |
. . . . . . . . 9
wff (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))) |
40 | 39, 19, 6 | wral 3065 |
. . . . . . . 8
wff
∀𝑧 ∈
ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))) |
41 | 27, 40 | wa 395 |
. . . . . . 7
wff
(∀𝑧 ∈
ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))) |
42 | 41, 17, 6 | wral 3065 |
. . . . . 6
wff
∀𝑦 ∈
ℂ (∀𝑧 ∈
ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))) |
43 | 16, 42 | wa 395 |
. . . . 5
wff ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))) |
44 | 43, 13, 7 | wral 3065 |
. . . 4
wff
∀𝑥 ∈ ran
𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))) |
45 | 5, 11, 44 | w3a 1085 |
. . 3
wff (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))) |
46 | 45, 2, 9 | copab 5140 |
. 2
class
{〈𝑔, 𝑠〉 ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))} |
47 | 1, 46 | wceq 1541 |
1
wff
CVecOLD = {〈𝑔, 𝑠〉 ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))} |