Step | Hyp | Ref
| Expression |
1 | | df-mpt2 5517 |
. 2
⊢ (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ 𝑧 = ⟨((1^{st} ‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)} |
2 | | df-mpq 6443 |
. 2
⊢
·_{pQ} = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |
3 | | 1st2nd2 5801 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (N ×
N) → 𝑥 =
⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
4 | 3 | eqeq1d 2048 |
. . . . . . . . 9
⊢ (𝑥 ∈ (N ×
N) → (𝑥
= ⟨𝑤, 𝑣⟩ ↔
⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ = ⟨𝑤, 𝑣⟩)) |
5 | | 1st2nd2 5801 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (N ×
N) → 𝑦 =
⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
6 | 5 | eqeq1d 2048 |
. . . . . . . . 9
⊢ (𝑦 ∈ (N ×
N) → (𝑦
= ⟨𝑢, 𝑓⟩ ↔
⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩ = ⟨𝑢, 𝑓⟩)) |
7 | 4, 6 | bi2anan9 538 |
. . . . . . . 8
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → ((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ↔ (⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩ =
⟨𝑤, 𝑣⟩ ∧ ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩ =
⟨𝑢, 𝑓⟩))) |
8 | 7 | anbi1d 438 |
. . . . . . 7
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩) ↔
((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩ =
⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩))) |
9 | 8 | bicomd 129 |
. . . . . 6
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) →
(((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩ =
⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩) ↔ ((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩))) |
10 | 9 | 4exbidv 1750 |
. . . . 5
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩ =
⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩) ↔ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩))) |
11 | | xp1st 5792 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → (1^{st} ‘𝑥) ∈ N) |
12 | | xp2nd 5793 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → (2^{nd} ‘𝑥) ∈ N) |
13 | 11, 12 | jca 290 |
. . . . . 6
⊢ (𝑥 ∈ (N ×
N) → ((1^{st} ‘𝑥) ∈ N ∧
(2^{nd} ‘𝑥)
∈ N)) |
14 | | xp1st 5792 |
. . . . . . 7
⊢ (𝑦 ∈ (N ×
N) → (1^{st} ‘𝑦) ∈ N) |
15 | | xp2nd 5793 |
. . . . . . 7
⊢ (𝑦 ∈ (N ×
N) → (2^{nd} ‘𝑦) ∈ N) |
16 | 14, 15 | jca 290 |
. . . . . 6
⊢ (𝑦 ∈ (N ×
N) → ((1^{st} ‘𝑦) ∈ N ∧
(2^{nd} ‘𝑦)
∈ N)) |
17 | | simpll 481 |
. . . . . . . . . 10
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → 𝑤 = (1^{st} ‘𝑥)) |
18 | | simprl 483 |
. . . . . . . . . 10
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → 𝑢 = (1^{st} ‘𝑦)) |
19 | 17, 18 | oveq12d 5530 |
. . . . . . . . 9
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → (𝑤 ·_{N} 𝑢) = ((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦))) |
20 | | simplr 482 |
. . . . . . . . . 10
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → 𝑣 = (2^{nd} ‘𝑥)) |
21 | | simprr 484 |
. . . . . . . . . 10
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → 𝑓 = (2^{nd} ‘𝑦)) |
22 | 20, 21 | oveq12d 5530 |
. . . . . . . . 9
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → (𝑣 ·_{N} 𝑓) = ((2^{nd}
‘𝑥)
·_{N} (2^{nd} ‘𝑦))) |
23 | 19, 22 | opeq12d 3557 |
. . . . . . . 8
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩ = ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |
24 | 23 | eqeq2d 2051 |
. . . . . . 7
⊢ (((𝑤 = (1^{st} ‘𝑥) ∧ 𝑣 = (2^{nd} ‘𝑥)) ∧ (𝑢 = (1^{st} ‘𝑦) ∧ 𝑓 = (2^{nd} ‘𝑦))) → (𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩ ↔ 𝑧 = ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)) |
25 | 24 | copsex4g 3984 |
. . . . . 6
⊢
((((1^{st} ‘𝑥) ∈ N ∧
(2^{nd} ‘𝑥)
∈ N) ∧ ((1^{st} ‘𝑦) ∈ N ∧
(2^{nd} ‘𝑦)
∈ N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩ =
⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩) ↔ 𝑧 = ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)) |
26 | 13, 16, 25 | syl2an 273 |
. . . . 5
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ = ⟨𝑤, 𝑣⟩ ∧ ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩ =
⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩) ↔ 𝑧 = ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)) |
27 | 10, 26 | bitr3d 179 |
. . . 4
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩) ↔ 𝑧 = ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)) |
28 | 27 | pm5.32i 427 |
. . 3
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩)) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ 𝑧 = ⟨((1^{st} ‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)) |
29 | 28 | oprabbii 5560 |
. 2
⊢
{⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ 𝑧 = ⟨((1^{st} ‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩)} |
30 | 1, 2, 29 | 3eqtr4i 2070 |
1
⊢
·_{pQ} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩))} |