Detailed syntax breakdown of Definition df-plq0
Step | Hyp | Ref
| Expression |
1 | | cplq0 6273 |
. 2
class
+Q0 |
2 | | vx |
. . . . . . 7
setvar x |
3 | 2 | cv 1241 |
. . . . . 6
class x |
4 | | cnq0 6271 |
. . . . . 6
class
Q0 |
5 | 3, 4 | wcel 1390 |
. . . . 5
wff x ∈
Q0 |
6 | | vy |
. . . . . . 7
setvar y |
7 | 6 | cv 1241 |
. . . . . 6
class y |
8 | 7, 4 | wcel 1390 |
. . . . 5
wff y ∈
Q0 |
9 | 5, 8 | wa 97 |
. . . 4
wff (x ∈
Q0 ∧ y ∈
Q0) |
10 | | vw |
. . . . . . . . . . . . . 14
setvar w |
11 | 10 | cv 1241 |
. . . . . . . . . . . . 13
class w |
12 | | vv |
. . . . . . . . . . . . . 14
setvar v |
13 | 12 | cv 1241 |
. . . . . . . . . . . . 13
class v |
14 | 11, 13 | cop 3370 |
. . . . . . . . . . . 12
class 〈w, v〉 |
15 | | ceq0 6270 |
. . . . . . . . . . . 12
class
~Q0 |
16 | 14, 15 | cec 6040 |
. . . . . . . . . . 11
class [〈w, v〉]
~Q0 |
17 | 3, 16 | wceq 1242 |
. . . . . . . . . 10
wff x = [〈w,
v〉]
~Q0 |
18 | | vu |
. . . . . . . . . . . . . 14
setvar u |
19 | 18 | cv 1241 |
. . . . . . . . . . . . 13
class u |
20 | | vf |
. . . . . . . . . . . . . 14
setvar f |
21 | 20 | cv 1241 |
. . . . . . . . . . . . 13
class f |
22 | 19, 21 | cop 3370 |
. . . . . . . . . . . 12
class 〈u, f〉 |
23 | 22, 15 | cec 6040 |
. . . . . . . . . . 11
class [〈u, f〉]
~Q0 |
24 | 7, 23 | wceq 1242 |
. . . . . . . . . 10
wff y = [〈u,
f〉]
~Q0 |
25 | 17, 24 | wa 97 |
. . . . . . . . 9
wff (x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0
) |
26 | | vz |
. . . . . . . . . . 11
setvar z |
27 | 26 | cv 1241 |
. . . . . . . . . 10
class z |
28 | | comu 5938 |
. . . . . . . . . . . . . 14
class
·𝑜 |
29 | 11, 21, 28 | co 5455 |
. . . . . . . . . . . . 13
class (w ·𝑜 f) |
30 | 13, 19, 28 | co 5455 |
. . . . . . . . . . . . 13
class (v ·𝑜 u) |
31 | | coa 5937 |
. . . . . . . . . . . . 13
class
+𝑜 |
32 | 29, 30, 31 | co 5455 |
. . . . . . . . . . . 12
class ((w ·𝑜 f) +𝑜 (v ·𝑜 u)) |
33 | 13, 21, 28 | co 5455 |
. . . . . . . . . . . 12
class (v ·𝑜 f) |
34 | 32, 33 | cop 3370 |
. . . . . . . . . . 11
class 〈((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉 |
35 | 34, 15 | cec 6040 |
. . . . . . . . . 10
class [〈((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 |
36 | 27, 35 | wceq 1242 |
. . . . . . . . 9
wff z = [〈((w
·𝑜 f)
+𝑜 (v
·𝑜 u)), (v ·𝑜 f)〉]
~Q0 |
37 | 25, 36 | wa 97 |
. . . . . . . 8
wff ((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ) |
38 | 37, 20 | wex 1378 |
. . . . . . 7
wff ∃f((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ) |
39 | 38, 18 | wex 1378 |
. . . . . 6
wff ∃u∃f((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ) |
40 | 39, 12 | wex 1378 |
. . . . 5
wff ∃v∃u∃f((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ) |
41 | 40, 10 | wex 1378 |
. . . 4
wff ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ) |
42 | 9, 41 | wa 97 |
. . 3
wff ((x ∈
Q0 ∧ y ∈
Q0) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 )) |
43 | 42, 2, 6, 26 | coprab 5456 |
. 2
class {〈〈x, y〉,
z〉 ∣ ((x ∈
Q0 ∧ y ∈
Q0) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ))} |
44 | 1, 43 | wceq 1242 |
1
wff +Q0
= {〈〈x, y〉, z〉
∣ ((x ∈ Q0 ∧ y ∈ Q0) ∧ ∃w∃v∃u∃f((x =
[〈w, v〉] ~Q0 ∧ y =
[〈u, f〉] ~Q0 ) ∧ z =
[〈((w ·𝑜
f) +𝑜 (v ·𝑜 u)), (v
·𝑜 f)〉]
~Q0 ))} |