Proof of Theorem dfplpq2
Step | Hyp | Ref
| Expression |
1 | | df-mpt2 5460 |
. 2
⊢ (x ∈
(N × N), y ∈
(N × N) ↦ 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉) =
{〈〈x, y〉, z〉
∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ z =
〈(((1st ‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉)} |
2 | | df-plpq 6328 |
. 2
⊢
+pQ = (x ∈ (N × N),
y ∈
(N × N) ↦ 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉) |
3 | | 1st2nd2 5743 |
. . . . . . . . . 10
⊢ (x ∈
(N × N) → x = 〈(1st ‘x), (2nd ‘x)〉) |
4 | 3 | eqeq1d 2045 |
. . . . . . . . 9
⊢ (x ∈
(N × N) → (x = 〈w,
v〉 ↔ 〈(1st
‘x), (2nd ‘x)〉 = 〈w, v〉)) |
5 | | 1st2nd2 5743 |
. . . . . . . . . 10
⊢ (y ∈
(N × N) → y = 〈(1st ‘y), (2nd ‘y)〉) |
6 | 5 | eqeq1d 2045 |
. . . . . . . . 9
⊢ (y ∈
(N × N) → (y = 〈u,
f〉 ↔ 〈(1st
‘y), (2nd ‘y)〉 = 〈u, f〉)) |
7 | 4, 6 | bi2anan9 538 |
. . . . . . . 8
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
((x = 〈w, v〉 ∧ y =
〈u, f〉) ↔ (〈(1st
‘x), (2nd ‘x)〉 = 〈w, v〉 ∧ 〈(1st ‘y), (2nd ‘y)〉 = 〈u, f〉))) |
8 | 7 | anbi1d 438 |
. . . . . . 7
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(((x = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉) ↔ ((〈(1st
‘x), (2nd ‘x)〉 = 〈w, v〉 ∧ 〈(1st ‘y), (2nd ‘y)〉 = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉))) |
9 | | xp1st 5734 |
. . . . . . . . . . . . . 14
⊢ (y ∈
(N × N) → (1st
‘y) ∈ N) |
10 | 9 | ad2antlr 458 |
. . . . . . . . . . . . 13
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → (1st
‘y) ∈ N) |
11 | 7 | biimpa 280 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → (〈(1st
‘x), (2nd ‘x)〉 = 〈w, v〉 ∧ 〈(1st ‘y), (2nd ‘y)〉 = 〈u, f〉)) |
12 | 11 | simprd 107 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → 〈(1st
‘y), (2nd ‘y)〉 = 〈u, f〉) |
13 | | vex 2554 |
. . . . . . . . . . . . . . . . 17
⊢ u ∈
V |
14 | | vex 2554 |
. . . . . . . . . . . . . . . . 17
⊢ f ∈
V |
15 | 13, 14 | opth2 3968 |
. . . . . . . . . . . . . . . 16
⊢
(〈(1st ‘y),
(2nd ‘y)〉 =
〈u, f〉 ↔ ((1st ‘y) = u ∧ (2nd ‘y) = f)) |
16 | 15 | simplbi 259 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘y),
(2nd ‘y)〉 =
〈u, f〉 → (1st ‘y) = u) |
17 | 16 | eleq1d 2103 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘y),
(2nd ‘y)〉 =
〈u, f〉 → ((1st ‘y) ∈
N ↔ u ∈ N)) |
18 | 12, 17 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → ((1st
‘y) ∈ N ↔ u ∈
N)) |
19 | 10, 18 | mpbid 135 |
. . . . . . . . . . . 12
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → u ∈
N) |
20 | | xp2nd 5735 |
. . . . . . . . . . . . . 14
⊢ (x ∈
(N × N) → (2nd
‘x) ∈ N) |
21 | 20 | ad2antrr 457 |
. . . . . . . . . . . . 13
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → (2nd
‘x) ∈ N) |
22 | 11 | simpld 105 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → 〈(1st
‘x), (2nd ‘x)〉 = 〈w, v〉) |
23 | | vex 2554 |
. . . . . . . . . . . . . . . . 17
⊢ w ∈
V |
24 | | vex 2554 |
. . . . . . . . . . . . . . . . 17
⊢ v ∈
V |
25 | 23, 24 | opth2 3968 |
. . . . . . . . . . . . . . . 16
⊢
(〈(1st ‘x),
(2nd ‘x)〉 =
〈w, v〉 ↔ ((1st ‘x) = w ∧ (2nd ‘x) = v)) |
26 | 25 | simprbi 260 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘x),
(2nd ‘x)〉 =
〈w, v〉 → (2nd ‘x) = v) |
27 | 26 | eleq1d 2103 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘x),
(2nd ‘x)〉 =
〈w, v〉 → ((2nd ‘x) ∈
N ↔ v ∈ N)) |
28 | 22, 27 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → ((2nd
‘x) ∈ N ↔ v ∈
N)) |
29 | 21, 28 | mpbid 135 |
. . . . . . . . . . . 12
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → v ∈
N) |
30 | | mulcompig 6315 |
. . . . . . . . . . . 12
⊢
((u ∈ N ∧ v ∈ N) → (u ·N v) = (v
·N u)) |
31 | 19, 29, 30 | syl2anc 391 |
. . . . . . . . . . 11
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → (u ·N v) = (v
·N u)) |
32 | 31 | oveq2d 5471 |
. . . . . . . . . 10
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → ((w ·N f) +N (u ·N v)) = ((w
·N f)
+N (v
·N u))) |
33 | 32 | opeq1d 3546 |
. . . . . . . . 9
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → 〈((w ·N f) +N (u ·N v)), (v
·N f)〉
= 〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉) |
34 | 33 | eqeq2d 2048 |
. . . . . . . 8
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ (x =
〈w, v〉 ∧ y = 〈u,
f〉)) → (z = 〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉 ↔ z = 〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉)) |
35 | 34 | pm5.32da 425 |
. . . . . . 7
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(((x = 〈w, v〉 ∧ y =
〈u, f〉) ∧ z = 〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉) ↔ ((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉))) |
36 | 8, 35 | bitr3d 179 |
. . . . . 6
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(((〈(1st ‘x),
(2nd ‘x)〉 =
〈w, v〉 ∧
〈(1st ‘y),
(2nd ‘y)〉 =
〈u, f〉) ∧ z = 〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉) ↔ ((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉))) |
37 | 36 | 4exbidv 1747 |
. . . . 5
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(∃w∃v∃u∃f((〈(1st ‘x), (2nd ‘x)〉 = 〈w, v〉 ∧ 〈(1st ‘y), (2nd ‘y)〉 = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉) ↔ ∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉))) |
38 | | xp1st 5734 |
. . . . . . 7
⊢ (x ∈
(N × N) → (1st
‘x) ∈ N) |
39 | 38, 20 | jca 290 |
. . . . . 6
⊢ (x ∈
(N × N) → ((1st
‘x) ∈ N ∧ (2nd ‘x) ∈
N)) |
40 | | xp2nd 5735 |
. . . . . . 7
⊢ (y ∈
(N × N) → (2nd
‘y) ∈ N) |
41 | 9, 40 | jca 290 |
. . . . . 6
⊢ (y ∈
(N × N) → ((1st
‘y) ∈ N ∧ (2nd ‘y) ∈
N)) |
42 | | simpll 481 |
. . . . . . . . . . 11
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) → w = (1st ‘x)) |
43 | | simprr 484 |
. . . . . . . . . . 11
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) → f = (2nd ‘y)) |
44 | 42, 43 | oveq12d 5473 |
. . . . . . . . . 10
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) →
(w ·N
f) = ((1st ‘x) ·N
(2nd ‘y))) |
45 | | simprl 483 |
. . . . . . . . . . 11
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) → u = (1st ‘y)) |
46 | | simplr 482 |
. . . . . . . . . . 11
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) → v = (2nd ‘x)) |
47 | 45, 46 | oveq12d 5473 |
. . . . . . . . . 10
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) →
(u ·N
v) = ((1st ‘y) ·N
(2nd ‘x))) |
48 | 44, 47 | oveq12d 5473 |
. . . . . . . . 9
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) →
((w ·N
f) +N (u ·N v)) = (((1st ‘x) ·N
(2nd ‘y))
+N ((1st ‘y) ·N
(2nd ‘x)))) |
49 | 46, 43 | oveq12d 5473 |
. . . . . . . . 9
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) →
(v ·N
f) = ((2nd ‘x) ·N
(2nd ‘y))) |
50 | 48, 49 | opeq12d 3548 |
. . . . . . . 8
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) →
〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉 = 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉) |
51 | 50 | eqeq2d 2048 |
. . . . . . 7
⊢
(((w = (1st
‘x) ∧ v =
(2nd ‘x)) ∧ (u =
(1st ‘y) ∧ f =
(2nd ‘y))) →
(z = 〈((w ·N f) +N (u ·N v)), (v
·N f)〉
↔ z = 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉)) |
52 | 51 | copsex4g 3975 |
. . . . . 6
⊢
((((1st ‘x) ∈ N ∧ (2nd ‘x) ∈
N) ∧ ((1st
‘y) ∈ N ∧ (2nd ‘y) ∈
N)) → (∃w∃v∃u∃f((〈(1st ‘x), (2nd ‘x)〉 = 〈w, v〉 ∧ 〈(1st ‘y), (2nd ‘y)〉 = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉) ↔ z = 〈(((1st ‘x) ·N
(2nd ‘y))
+N ((1st ‘y) ·N
(2nd ‘x))),
((2nd ‘x)
·N (2nd ‘y))〉)) |
53 | 39, 41, 52 | syl2an 273 |
. . . . 5
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(∃w∃v∃u∃f((〈(1st ‘x), (2nd ‘x)〉 = 〈w, v〉 ∧ 〈(1st ‘y), (2nd ‘y)〉 = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (u
·N v)),
(v ·N
f)〉) ↔ z = 〈(((1st ‘x) ·N
(2nd ‘y))
+N ((1st ‘y) ·N
(2nd ‘x))),
((2nd ‘x)
·N (2nd ‘y))〉)) |
54 | 37, 53 | bitr3d 179 |
. . . 4
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉) ↔ z = 〈(((1st ‘x) ·N
(2nd ‘y))
+N ((1st ‘y) ·N
(2nd ‘x))),
((2nd ‘x)
·N (2nd ‘y))〉)) |
55 | 54 | pm5.32i 427 |
. . 3
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 〈((w ·N f) +N (v ·N u)), (v
·N f)〉)) ↔ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
z = 〈(((1st ‘x) ·N
(2nd ‘y))
+N ((1st ‘y) ·N
(2nd ‘x))),
((2nd ‘x)
·N (2nd ‘y))〉)) |
56 | 55 | oprabbii 5502 |
. 2
⊢
{〈〈x, y〉, z〉
∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧
z = 〈((w ·N f) +N (v ·N u)), (v
·N f)〉))} = {〈〈x, y〉,
z〉 ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
z = 〈(((1st ‘x) ·N
(2nd ‘y))
+N ((1st ‘y) ·N
(2nd ‘x))),
((2nd ‘x)
·N (2nd ‘y))〉)} |
57 | 1, 2, 56 | 3eqtr4i 2067 |
1
⊢
+pQ = {〈〈x, y〉,
z〉 ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
∃w∃v∃u∃f((x = 〈w,
v〉 ∧
y = 〈u, f〉)
∧ z =
〈((w
·N f)
+N (v
·N u)),
(v ·N
f)〉))} |