Proof of Theorem dfplpq2
Step | Hyp | Ref
| Expression |
1 | | df-mpo 5855 |
. 2
⊢ (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ 𝑧 = 〈(((1st ‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)} |
2 | | df-plpq 7293 |
. 2
⊢
+pQ = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |
3 | | 1st2nd2 6151 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (N ×
N) → 𝑥 =
〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
4 | 3 | eqeq1d 2179 |
. . . . . . . . 9
⊢ (𝑥 ∈ (N ×
N) → (𝑥
= 〈𝑤, 𝑣〉 ↔
〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉)) |
5 | | 1st2nd2 6151 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (N ×
N) → 𝑦 =
〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
6 | 5 | eqeq1d 2179 |
. . . . . . . . 9
⊢ (𝑦 ∈ (N ×
N) → (𝑦
= 〈𝑢, 𝑓〉 ↔
〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈𝑢, 𝑓〉)) |
7 | 4, 6 | bi2anan9 601 |
. . . . . . . 8
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → ((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ↔ (〈(1st
‘𝑥), (2nd
‘𝑥)〉 =
〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉))) |
8 | 7 | anbi1d 462 |
. . . . . . 7
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉) ↔
((〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉))) |
9 | | xp1st 6141 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (N ×
N) → (1st ‘𝑦) ∈ N) |
10 | 9 | ad2antlr 486 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → (1st ‘𝑦) ∈
N) |
11 | 7 | biimpa 294 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → (〈(1st
‘𝑥), (2nd
‘𝑥)〉 =
〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉)) |
12 | 11 | simprd 113 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉) |
13 | | vex 2733 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
14 | | vex 2733 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
15 | 13, 14 | opth2 4223 |
. . . . . . . . . . . . . . . 16
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈𝑢, 𝑓〉 ↔ ((1st ‘𝑦) = 𝑢 ∧ (2nd ‘𝑦) = 𝑓)) |
16 | 15 | simplbi 272 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈𝑢, 𝑓〉 → (1st ‘𝑦) = 𝑢) |
17 | 16 | eleq1d 2239 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈𝑢, 𝑓〉 → ((1st ‘𝑦) ∈ N ↔
𝑢 ∈
N)) |
18 | 12, 17 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → ((1st ‘𝑦) ∈ N ↔
𝑢 ∈
N)) |
19 | 10, 18 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → 𝑢 ∈ N) |
20 | | xp2nd 6142 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (N ×
N) → (2nd ‘𝑥) ∈ N) |
21 | 20 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → (2nd ‘𝑥) ∈
N) |
22 | 11 | simpld 111 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → 〈(1st
‘𝑥), (2nd
‘𝑥)〉 =
〈𝑤, 𝑣〉) |
23 | | vex 2733 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
24 | | vex 2733 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
25 | 23, 24 | opth2 4223 |
. . . . . . . . . . . . . . . 16
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 ↔ ((1st ‘𝑥) = 𝑤 ∧ (2nd ‘𝑥) = 𝑣)) |
26 | 25 | simprbi 273 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 → (2nd ‘𝑥) = 𝑣) |
27 | 26 | eleq1d 2239 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 → ((2nd ‘𝑥) ∈ N ↔
𝑣 ∈
N)) |
28 | 22, 27 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → ((2nd ‘𝑥) ∈ N ↔
𝑣 ∈
N)) |
29 | 21, 28 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → 𝑣 ∈ N) |
30 | | mulcompig 7280 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ N ∧
𝑣 ∈ N)
→ (𝑢
·N 𝑣) = (𝑣 ·N 𝑢)) |
31 | 19, 29, 30 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → (𝑢 ·N 𝑣) = (𝑣 ·N 𝑢)) |
32 | 31 | oveq2d 5866 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → ((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)) = ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢))) |
33 | 32 | opeq1d 3769 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉 = 〈((𝑤
·N 𝑓) +N (𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉) |
34 | 33 | eqeq2d 2182 |
. . . . . . . 8
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉)) → (𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉 ↔ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉)) |
35 | 34 | pm5.32da 449 |
. . . . . . 7
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉) ↔ ((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))) |
36 | 8, 35 | bitr3d 189 |
. . . . . 6
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) →
(((〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉) ↔ ((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))) |
37 | 36 | 4exbidv 1863 |
. . . . 5
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉) ↔ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))) |
38 | | xp1st 6141 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → (1st ‘𝑥) ∈ N) |
39 | 38, 20 | jca 304 |
. . . . . 6
⊢ (𝑥 ∈ (N ×
N) → ((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑥)
∈ N)) |
40 | | xp2nd 6142 |
. . . . . . 7
⊢ (𝑦 ∈ (N ×
N) → (2nd ‘𝑦) ∈ N) |
41 | 9, 40 | jca 304 |
. . . . . 6
⊢ (𝑦 ∈ (N ×
N) → ((1st ‘𝑦) ∈ N ∧
(2nd ‘𝑦)
∈ N)) |
42 | | simpll 524 |
. . . . . . . . . . 11
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → 𝑤 = (1st ‘𝑥)) |
43 | | simprr 527 |
. . . . . . . . . . 11
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → 𝑓 = (2nd ‘𝑦)) |
44 | 42, 43 | oveq12d 5868 |
. . . . . . . . . 10
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → (𝑤 ·N 𝑓) = ((1st
‘𝑥)
·N (2nd ‘𝑦))) |
45 | | simprl 526 |
. . . . . . . . . . 11
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → 𝑢 = (1st ‘𝑦)) |
46 | | simplr 525 |
. . . . . . . . . . 11
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → 𝑣 = (2nd ‘𝑥)) |
47 | 45, 46 | oveq12d 5868 |
. . . . . . . . . 10
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → (𝑢 ·N 𝑣) = ((1st
‘𝑦)
·N (2nd ‘𝑥))) |
48 | 44, 47 | oveq12d 5868 |
. . . . . . . . 9
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → ((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)) = (((1st ‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥)))) |
49 | 46, 43 | oveq12d 5868 |
. . . . . . . . 9
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → (𝑣 ·N 𝑓) = ((2nd
‘𝑥)
·N (2nd ‘𝑦))) |
50 | 48, 49 | opeq12d 3771 |
. . . . . . . 8
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉 =
〈(((1st ‘𝑥) ·N
(2nd ‘𝑦))
+N ((1st ‘𝑦) ·N
(2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |
51 | 50 | eqeq2d 2182 |
. . . . . . 7
⊢ (((𝑤 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) ∧ (𝑢 = (1st ‘𝑦) ∧ 𝑓 = (2nd ‘𝑦))) → (𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉 ↔ 𝑧 = 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)) |
52 | 51 | copsex4g 4230 |
. . . . . 6
⊢
((((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑥)
∈ N) ∧ ((1st ‘𝑦) ∈ N ∧
(2nd ‘𝑦)
∈ N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉) ↔ 𝑧 = 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)) |
53 | 39, 41, 52 | syl2an 287 |
. . . . 5
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑤, 𝑣〉 ∧ 〈(1st
‘𝑦), (2nd
‘𝑦)〉 =
〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑢
·N 𝑣)), (𝑣 ·N 𝑓)〉) ↔ 𝑧 = 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)) |
54 | 37, 53 | bitr3d 189 |
. . . 4
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉) ↔ 𝑧 = 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)) |
55 | 54 | pm5.32i 451 |
. . 3
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉)) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ 𝑧 = 〈(((1st ‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)) |
56 | 55 | oprabbii 5905 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ 𝑧 = 〈(((1st ‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉)} |
57 | 1, 2, 56 | 3eqtr4i 2201 |
1
⊢
+pQ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))} |