Step | Hyp | Ref
| Expression |
1 | | addpipqqslem 6353 |
. 2
⊢
(((A ∈ N ∧ B ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N)) → 〈((A
·N 𝐷) +N (B ·N 𝐶)), (B ·N 𝐷)〉 ∈ (N ×
N)) |
2 | | addpipqqslem 6353 |
. 2
⊢ (((𝑎 ∈ N ∧ 𝑏
∈ N) ∧ (g ∈ N ∧ ℎ
∈ N)) → 〈((𝑎 ·N
ℎ) +N
(𝑏
·N g)),
(𝑏
·N ℎ)〉 ∈
(N × N)) |
3 | | addpipqqslem 6353 |
. 2
⊢ (((𝑐 ∈ N ∧ 𝑑
∈ N) ∧ (𝑡 ∈
N ∧ 𝑠 ∈
N)) → 〈((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡)), (𝑑 ·N 𝑠)〉 ∈ (N ×
N)) |
4 | | enqex 6344 |
. 2
⊢
~Q ∈
V |
5 | | enqer 6342 |
. 2
⊢
~Q Er (N ×
N) |
6 | | df-enq 6331 |
. 2
⊢
~Q = {〈x,
y〉 ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
∃z∃w∃v∃u((x = 〈z,
w〉 ∧
y = 〈v, u〉)
∧ (z
·N u) =
(w ·N
v)))} |
7 | | oveq12 5464 |
. . . 4
⊢
((z = 𝑎 ∧ u = 𝑑) → (z ·N u) = (𝑎 ·N 𝑑)) |
8 | | oveq12 5464 |
. . . 4
⊢
((w = 𝑏 ∧ v = 𝑐) → (w ·N v) = (𝑏 ·N 𝑐)) |
9 | 7, 8 | eqeqan12d 2052 |
. . 3
⊢
(((z = 𝑎 ∧ u = 𝑑) ∧
(w = 𝑏 ∧ v = 𝑐)) → ((z ·N u) = (w
·N v)
↔ (𝑎
·N 𝑑) = (𝑏 ·N 𝑐))) |
10 | 9 | an42s 523 |
. 2
⊢
(((z = 𝑎 ∧ w = 𝑏) ∧
(v = 𝑐 ∧ u = 𝑑)) → ((z ·N u) = (w
·N v)
↔ (𝑎
·N 𝑑) = (𝑏 ·N 𝑐))) |
11 | | oveq12 5464 |
. . . 4
⊢
((z = g ∧ u = 𝑠) → (z ·N u) = (g
·N 𝑠)) |
12 | | oveq12 5464 |
. . . 4
⊢
((w = ℎ ∧ v = 𝑡) → (w ·N v) = (ℎ ·N 𝑡)) |
13 | 11, 12 | eqeqan12d 2052 |
. . 3
⊢
(((z = g ∧ u = 𝑠) ∧
(w = ℎ ∧ v = 𝑡)) → ((z ·N u) = (w
·N v)
↔ (g
·N 𝑠) = (ℎ ·N 𝑡))) |
14 | 13 | an42s 523 |
. 2
⊢
(((z = g ∧ w = ℎ) ∧ (v = 𝑡 ∧ u = 𝑠)) → ((z ·N u) = (w
·N v)
↔ (g
·N 𝑠) = (ℎ ·N 𝑡))) |
15 | | dfplpq2 6338 |
. 2
⊢
+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)〉))} |
16 | | oveq12 5464 |
. . . . 5
⊢
((w = 𝑎 ∧ f = ℎ) → (w ·N f) = (𝑎 ·N ℎ)) |
17 | | oveq12 5464 |
. . . . 5
⊢
((v = 𝑏 ∧ u = g) →
(v ·N
u) = (𝑏 ·N g)) |
18 | 16, 17 | oveqan12d 5474 |
. . . 4
⊢
(((w = 𝑎 ∧ f = ℎ) ∧ (v = 𝑏 ∧ u = g)) →
((w ·N
f) +N (v ·N u)) = ((𝑎 ·N ℎ) +N (𝑏 ·N
g))) |
19 | 18 | an42s 523 |
. . 3
⊢
(((w = 𝑎 ∧ v = 𝑏) ∧
(u = g
∧ f =
ℎ)) → ((w ·N f) +N (v ·N u)) = ((𝑎 ·N ℎ) +N (𝑏 ·N
g))) |
20 | | oveq12 5464 |
. . . 4
⊢
((v = 𝑏 ∧ f = ℎ) → (v ·N f) = (𝑏 ·N ℎ)) |
21 | 20 | ad2ant2l 477 |
. . 3
⊢
(((w = 𝑎 ∧ v = 𝑏) ∧
(u = g
∧ f =
ℎ)) → (v ·N f) = (𝑏 ·N ℎ)) |
22 | 19, 21 | opeq12d 3548 |
. 2
⊢
(((w = 𝑎 ∧ v = 𝑏) ∧
(u = g
∧ f =
ℎ)) → 〈((w ·N f) +N (v ·N u)), (v
·N f)〉
= 〈((𝑎
·N ℎ) +N (𝑏 ·N g)), (𝑏 ·N ℎ)〉) |
23 | | oveq12 5464 |
. . . . 5
⊢
((w = 𝑐 ∧ f = 𝑠) → (w ·N f) = (𝑐 ·N 𝑠)) |
24 | | oveq12 5464 |
. . . . 5
⊢
((v = 𝑑 ∧ u = 𝑡) → (v ·N u) = (𝑑 ·N 𝑡)) |
25 | 23, 24 | oveqan12d 5474 |
. . . 4
⊢
(((w = 𝑐 ∧ f = 𝑠) ∧
(v = 𝑑 ∧ u = 𝑡)) → ((w ·N f) +N (v ·N u)) = ((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡))) |
26 | 25 | an42s 523 |
. . 3
⊢
(((w = 𝑐 ∧ v = 𝑑) ∧
(u = 𝑡 ∧ f = 𝑠)) → ((w ·N f) +N (v ·N u)) = ((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡))) |
27 | | oveq12 5464 |
. . . 4
⊢
((v = 𝑑 ∧ f = 𝑠) → (v ·N f) = (𝑑 ·N 𝑠)) |
28 | 27 | ad2ant2l 477 |
. . 3
⊢
(((w = 𝑐 ∧ v = 𝑑) ∧
(u = 𝑡 ∧ f = 𝑠)) → (v ·N f) = (𝑑 ·N 𝑠)) |
29 | 26, 28 | opeq12d 3548 |
. 2
⊢
(((w = 𝑐 ∧ v = 𝑑) ∧
(u = 𝑡 ∧ f = 𝑠)) → 〈((w ·N f) +N (v ·N u)), (v
·N f)〉
= 〈((𝑐
·N 𝑠) +N (𝑑 ·N
𝑡)), (𝑑 ·N 𝑠)〉) |
30 | | oveq12 5464 |
. . . . 5
⊢
((w = A ∧ f = 𝐷) → (w ·N f) = (A
·N 𝐷)) |
31 | | oveq12 5464 |
. . . . 5
⊢
((v = B ∧ u = 𝐶) → (v ·N u) = (B
·N 𝐶)) |
32 | 30, 31 | oveqan12d 5474 |
. . . 4
⊢
(((w = A ∧ f = 𝐷) ∧
(v = B
∧ u =
𝐶)) → ((w ·N f) +N (v ·N u)) = ((A
·N 𝐷) +N (B ·N 𝐶))) |
33 | 32 | an42s 523 |
. . 3
⊢
(((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → ((w ·N f) +N (v ·N u)) = ((A
·N 𝐷) +N (B ·N 𝐶))) |
34 | | oveq12 5464 |
. . . 4
⊢
((v = B ∧ f = 𝐷) → (v ·N f) = (B
·N 𝐷)) |
35 | 34 | ad2ant2l 477 |
. . 3
⊢
(((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → (v ·N f) = (B
·N 𝐷)) |
36 | 33, 35 | opeq12d 3548 |
. 2
⊢
(((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → 〈((w ·N f) +N (v ·N u)), (v
·N f)〉
= 〈((A
·N 𝐷) +N (B ·N 𝐶)), (B ·N 𝐷)〉) |
37 | | df-plqqs 6333 |
. 2
⊢
+Q = {〈〈x, y〉,
z〉 ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((x = [〈𝑎, 𝑏〉] ~Q ∧ y =
[〈𝑐, 𝑑〉] ~Q ) ∧ z =
[(〈𝑎, 𝑏〉 +pQ
〈𝑐, 𝑑〉)] ~Q
))} |
38 | | df-nqqs 6332 |
. 2
⊢
Q = ((N × N) /
~Q ) |
39 | | addcmpblnq 6351 |
. 2
⊢ ((((𝑎 ∈ N ∧ 𝑏
∈ N) ∧ (𝑐 ∈
N ∧ 𝑑 ∈
N)) ∧ ((g ∈
N ∧ ℎ ∈
N) ∧ (𝑡 ∈
N ∧ 𝑠 ∈
N))) → (((𝑎
·N 𝑑) = (𝑏 ·N 𝑐) ∧ (g
·N 𝑠) = (ℎ ·N 𝑡)) → 〈((𝑎 ·N ℎ) +N (𝑏 ·N
g)), (𝑏 ·N ℎ)〉 ~Q
〈((𝑐
·N 𝑠) +N (𝑑 ·N
𝑡)), (𝑑 ·N 𝑠)〉)) |
40 | 1, 2, 3, 4, 5, 6, 10, 14, 15, 22, 29, 36, 37, 38, 39 | oviec 6148 |
1
⊢
(((A ∈ N ∧ B ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N)) → ([〈A,
B〉] ~Q
+Q [〈𝐶, 𝐷〉] ~Q ) =
[〈((A
·N 𝐷) +N (B ·N 𝐶)), (B ·N 𝐷)〉]
~Q ) |