Step | Hyp | Ref
| Expression |
1 | | addpipqqslem 7289 |
. 2
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) → 〈((𝐴 ·N 𝐷) +N
(𝐵
·N 𝐶)), (𝐵 ·N 𝐷)〉 ∈ (N
× N)) |
2 | | addpipqqslem 7289 |
. 2
⊢ (((𝑎 ∈ N ∧
𝑏 ∈ N)
∧ (𝑔 ∈
N ∧ ℎ
∈ N)) → 〈((𝑎 ·N ℎ) +N
(𝑏
·N 𝑔)), (𝑏 ·N ℎ)〉 ∈ (N
× N)) |
3 | | addpipqqslem 7289 |
. 2
⊢ (((𝑐 ∈ N ∧
𝑑 ∈ N)
∧ (𝑡 ∈
N ∧ 𝑠
∈ N)) → 〈((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡)), (𝑑 ·N 𝑠)〉 ∈ (N
× N)) |
4 | | enqex 7280 |
. 2
⊢
~Q ∈ V |
5 | | enqer 7278 |
. 2
⊢
~Q Er (N ×
N) |
6 | | df-enq 7267 |
. 2
⊢
~Q = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |
7 | | oveq12 5833 |
. . . 4
⊢ ((𝑧 = 𝑎 ∧ 𝑢 = 𝑑) → (𝑧 ·N 𝑢) = (𝑎 ·N 𝑑)) |
8 | | oveq12 5833 |
. . . 4
⊢ ((𝑤 = 𝑏 ∧ 𝑣 = 𝑐) → (𝑤 ·N 𝑣) = (𝑏 ·N 𝑐)) |
9 | 7, 8 | eqeqan12d 2173 |
. . 3
⊢ (((𝑧 = 𝑎 ∧ 𝑢 = 𝑑) ∧ (𝑤 = 𝑏 ∧ 𝑣 = 𝑐)) → ((𝑧 ·N 𝑢) = (𝑤 ·N 𝑣) ↔ (𝑎 ·N 𝑑) = (𝑏 ·N 𝑐))) |
10 | 9 | an42s 579 |
. 2
⊢ (((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) ∧ (𝑣 = 𝑐 ∧ 𝑢 = 𝑑)) → ((𝑧 ·N 𝑢) = (𝑤 ·N 𝑣) ↔ (𝑎 ·N 𝑑) = (𝑏 ·N 𝑐))) |
11 | | oveq12 5833 |
. . . 4
⊢ ((𝑧 = 𝑔 ∧ 𝑢 = 𝑠) → (𝑧 ·N 𝑢) = (𝑔 ·N 𝑠)) |
12 | | oveq12 5833 |
. . . 4
⊢ ((𝑤 = ℎ ∧ 𝑣 = 𝑡) → (𝑤 ·N 𝑣) = (ℎ ·N 𝑡)) |
13 | 11, 12 | eqeqan12d 2173 |
. . 3
⊢ (((𝑧 = 𝑔 ∧ 𝑢 = 𝑠) ∧ (𝑤 = ℎ ∧ 𝑣 = 𝑡)) → ((𝑧 ·N 𝑢) = (𝑤 ·N 𝑣) ↔ (𝑔 ·N 𝑠) = (ℎ ·N 𝑡))) |
14 | 13 | an42s 579 |
. 2
⊢ (((𝑧 = 𝑔 ∧ 𝑤 = ℎ) ∧ (𝑣 = 𝑡 ∧ 𝑢 = 𝑠)) → ((𝑧 ·N 𝑢) = (𝑤 ·N 𝑣) ↔ (𝑔 ·N 𝑠) = (ℎ ·N 𝑡))) |
15 | | dfplpq2 7274 |
. 2
⊢
+pQ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))} |
16 | | oveq12 5833 |
. . . . 5
⊢ ((𝑤 = 𝑎 ∧ 𝑓 = ℎ) → (𝑤 ·N 𝑓) = (𝑎 ·N ℎ)) |
17 | | oveq12 5833 |
. . . . 5
⊢ ((𝑣 = 𝑏 ∧ 𝑢 = 𝑔) → (𝑣 ·N 𝑢) = (𝑏 ·N 𝑔)) |
18 | 16, 17 | oveqan12d 5843 |
. . . 4
⊢ (((𝑤 = 𝑎 ∧ 𝑓 = ℎ) ∧ (𝑣 = 𝑏 ∧ 𝑢 = 𝑔)) → ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)) = ((𝑎 ·N ℎ) +N
(𝑏
·N 𝑔))) |
19 | 18 | an42s 579 |
. . 3
⊢ (((𝑤 = 𝑎 ∧ 𝑣 = 𝑏) ∧ (𝑢 = 𝑔 ∧ 𝑓 = ℎ)) → ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)) = ((𝑎 ·N ℎ) +N
(𝑏
·N 𝑔))) |
20 | | oveq12 5833 |
. . . 4
⊢ ((𝑣 = 𝑏 ∧ 𝑓 = ℎ) → (𝑣 ·N 𝑓) = (𝑏 ·N ℎ)) |
21 | 20 | ad2ant2l 500 |
. . 3
⊢ (((𝑤 = 𝑎 ∧ 𝑣 = 𝑏) ∧ (𝑢 = 𝑔 ∧ 𝑓 = ℎ)) → (𝑣 ·N 𝑓) = (𝑏 ·N ℎ)) |
22 | 19, 21 | opeq12d 3749 |
. 2
⊢ (((𝑤 = 𝑎 ∧ 𝑣 = 𝑏) ∧ (𝑢 = 𝑔 ∧ 𝑓 = ℎ)) → 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉 = 〈((𝑎
·N ℎ) +N (𝑏
·N 𝑔)), (𝑏 ·N ℎ)〉) |
23 | | oveq12 5833 |
. . . . 5
⊢ ((𝑤 = 𝑐 ∧ 𝑓 = 𝑠) → (𝑤 ·N 𝑓) = (𝑐 ·N 𝑠)) |
24 | | oveq12 5833 |
. . . . 5
⊢ ((𝑣 = 𝑑 ∧ 𝑢 = 𝑡) → (𝑣 ·N 𝑢) = (𝑑 ·N 𝑡)) |
25 | 23, 24 | oveqan12d 5843 |
. . . 4
⊢ (((𝑤 = 𝑐 ∧ 𝑓 = 𝑠) ∧ (𝑣 = 𝑑 ∧ 𝑢 = 𝑡)) → ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)) = ((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡))) |
26 | 25 | an42s 579 |
. . 3
⊢ (((𝑤 = 𝑐 ∧ 𝑣 = 𝑑) ∧ (𝑢 = 𝑡 ∧ 𝑓 = 𝑠)) → ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)) = ((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡))) |
27 | | oveq12 5833 |
. . . 4
⊢ ((𝑣 = 𝑑 ∧ 𝑓 = 𝑠) → (𝑣 ·N 𝑓) = (𝑑 ·N 𝑠)) |
28 | 27 | ad2ant2l 500 |
. . 3
⊢ (((𝑤 = 𝑐 ∧ 𝑣 = 𝑑) ∧ (𝑢 = 𝑡 ∧ 𝑓 = 𝑠)) → (𝑣 ·N 𝑓) = (𝑑 ·N 𝑠)) |
29 | 26, 28 | opeq12d 3749 |
. 2
⊢ (((𝑤 = 𝑐 ∧ 𝑣 = 𝑑) ∧ (𝑢 = 𝑡 ∧ 𝑓 = 𝑠)) → 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉 = 〈((𝑐
·N 𝑠) +N (𝑑
·N 𝑡)), (𝑑 ·N 𝑠)〉) |
30 | | oveq12 5833 |
. . . . 5
⊢ ((𝑤 = 𝐴 ∧ 𝑓 = 𝐷) → (𝑤 ·N 𝑓) = (𝐴 ·N 𝐷)) |
31 | | oveq12 5833 |
. . . . 5
⊢ ((𝑣 = 𝐵 ∧ 𝑢 = 𝐶) → (𝑣 ·N 𝑢) = (𝐵 ·N 𝐶)) |
32 | 30, 31 | oveqan12d 5843 |
. . . 4
⊢ (((𝑤 = 𝐴 ∧ 𝑓 = 𝐷) ∧ (𝑣 = 𝐵 ∧ 𝑢 = 𝐶)) → ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)) = ((𝐴 ·N 𝐷) +N
(𝐵
·N 𝐶))) |
33 | 32 | an42s 579 |
. . 3
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → ((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)) = ((𝐴 ·N 𝐷) +N
(𝐵
·N 𝐶))) |
34 | | oveq12 5833 |
. . . 4
⊢ ((𝑣 = 𝐵 ∧ 𝑓 = 𝐷) → (𝑣 ·N 𝑓) = (𝐵 ·N 𝐷)) |
35 | 34 | ad2ant2l 500 |
. . 3
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (𝑣 ·N 𝑓) = (𝐵 ·N 𝐷)) |
36 | 33, 35 | opeq12d 3749 |
. 2
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉 = 〈((𝐴
·N 𝐷) +N (𝐵
·N 𝐶)), (𝐵 ·N 𝐷)〉) |
37 | | df-plqqs 7269 |
. 2
⊢
+Q = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ~Q ∧
𝑦 = [〈𝑐, 𝑑〉] ~Q ) ∧
𝑧 = [(〈𝑎, 𝑏〉 +pQ
〈𝑐, 𝑑〉)] ~Q
))} |
38 | | df-nqqs 7268 |
. 2
⊢
Q = ((N × N) /
~Q ) |
39 | | addcmpblnq 7287 |
. 2
⊢ ((((𝑎 ∈ N ∧
𝑏 ∈ N)
∧ (𝑐 ∈
N ∧ 𝑑
∈ N)) ∧ ((𝑔 ∈ N ∧ ℎ ∈ N) ∧
(𝑡 ∈ N
∧ 𝑠 ∈
N))) → (((𝑎 ·N 𝑑) = (𝑏 ·N 𝑐) ∧ (𝑔 ·N 𝑠) = (ℎ ·N 𝑡)) → 〈((𝑎
·N ℎ) +N (𝑏
·N 𝑔)), (𝑏 ·N ℎ)〉
~Q 〈((𝑐 ·N 𝑠) +N
(𝑑
·N 𝑡)), (𝑑 ·N 𝑠)〉)) |
40 | 1, 2, 3, 4, 5, 6, 10, 14, 15, 22, 29, 36, 37, 38, 39 | oviec 6586 |
1
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) → ([〈𝐴, 𝐵〉] ~Q
+Q [〈𝐶, 𝐷〉] ~Q ) =
[〈((𝐴
·N 𝐷) +N (𝐵
·N 𝐶)), (𝐵 ·N 𝐷)〉]
~Q ) |