Proof of Theorem dfplq0qs
Step | Hyp | Ref
| Expression |
1 | | df-plq0 6617 |
. 2
⊢
+Q0 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·𝑜
𝑓) +𝑜
(𝑣
·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)〉]
~Q0 ))} |
2 | | df-nq0 6615 |
. . . . . 6
⊢
Q0 = ((ω × N)
/ ~Q0 ) |
3 | 2 | eleq2i 2145 |
. . . . 5
⊢ (𝑥 ∈
Q0 ↔ 𝑥 ∈ ((ω × N)
/ ~Q0 )) |
4 | 2 | eleq2i 2145 |
. . . . 5
⊢ (𝑦 ∈
Q0 ↔ 𝑦 ∈ ((ω × N)
/ ~Q0 )) |
5 | 3, 4 | anbi12i 447 |
. . . 4
⊢ ((𝑥 ∈
Q0 ∧ 𝑦 ∈ Q0) ↔
(𝑥 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝑦 ∈ ((ω ×
N) / ~Q0 ))) |
6 | 5 | anbi1i 445 |
. . 3
⊢ (((𝑥 ∈
Q0 ∧ 𝑦 ∈ Q0) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·𝑜
𝑓) +𝑜
(𝑣
·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)〉]
~Q0 )) ↔ ((𝑥 ∈ ((ω × N)
/ ~Q0 ) ∧ 𝑦 ∈ ((ω × N)
/ ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·𝑜
𝑓) +𝑜
(𝑣
·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)〉]
~Q0 ))) |
7 | 6 | oprabbii 5580 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·𝑜
𝑓) +𝑜
(𝑣
·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)〉]
~Q0 ))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((ω × N)
/ ~Q0 ) ∧ 𝑦 ∈ ((ω × N)
/ ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·𝑜
𝑓) +𝑜
(𝑣
·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)〉]
~Q0 ))} |
8 | 1, 7 | eqtri 2101 |
1
⊢
+Q0 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((ω × N)
/ ~Q0 ) ∧ 𝑦 ∈ ((ω × N)
/ ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·𝑜
𝑓) +𝑜
(𝑣
·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)〉]
~Q0 ))} |