Step | Hyp | Ref
| Expression |
1 | | xp1st 6144 |
. . . 4
⊢ (𝐴 ∈ (N ×
N) → (1st ‘𝐴) ∈ N) |
2 | | xp1st 6144 |
. . . 4
⊢ (𝐵 ∈ (N ×
N) → (1st ‘𝐵) ∈ N) |
3 | | mulclpi 7290 |
. . . 4
⊢
(((1st ‘𝐴) ∈ N ∧
(1st ‘𝐵)
∈ N) → ((1st ‘𝐴) ·N
(1st ‘𝐵))
∈ N) |
4 | 1, 2, 3 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → ((1st
‘𝐴)
·N (1st ‘𝐵)) ∈ N) |
5 | | xp2nd 6145 |
. . . 4
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) |
6 | | xp2nd 6145 |
. . . 4
⊢ (𝐵 ∈ (N ×
N) → (2nd ‘𝐵) ∈ N) |
7 | | mulclpi 7290 |
. . . 4
⊢
(((2nd ‘𝐴) ∈ N ∧
(2nd ‘𝐵)
∈ N) → ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) |
8 | 5, 6, 7 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → ((2nd
‘𝐴)
·N (2nd ‘𝐵)) ∈ N) |
9 | | opexg 4213 |
. . 3
⊢
((((1st ‘𝐴) ·N
(1st ‘𝐵))
∈ N ∧ ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) → 〈((1st ‘𝐴) ·N
(1st ‘𝐵)),
((2nd ‘𝐴)
·N (2nd ‘𝐵))〉 ∈ V) |
10 | 4, 8, 9 | syl2anc 409 |
. 2
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉 ∈ V) |
11 | | fveq2 5496 |
. . . . 5
⊢ (𝑥 = 𝐴 → (1st ‘𝑥) = (1st ‘𝐴)) |
12 | 11 | oveq1d 5868 |
. . . 4
⊢ (𝑥 = 𝐴 → ((1st ‘𝑥)
·N (1st ‘𝑦)) = ((1st ‘𝐴)
·N (1st ‘𝑦))) |
13 | | fveq2 5496 |
. . . . 5
⊢ (𝑥 = 𝐴 → (2nd ‘𝑥) = (2nd ‘𝐴)) |
14 | 13 | oveq1d 5868 |
. . . 4
⊢ (𝑥 = 𝐴 → ((2nd ‘𝑥)
·N (2nd ‘𝑦)) = ((2nd ‘𝐴)
·N (2nd ‘𝑦))) |
15 | 12, 14 | opeq12d 3773 |
. . 3
⊢ (𝑥 = 𝐴 → 〈((1st ‘𝑥)
·N (1st ‘𝑦)), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉 = 〈((1st
‘𝐴)
·N (1st ‘𝑦)), ((2nd ‘𝐴) ·N
(2nd ‘𝑦))〉) |
16 | | fveq2 5496 |
. . . . 5
⊢ (𝑦 = 𝐵 → (1st ‘𝑦) = (1st ‘𝐵)) |
17 | 16 | oveq2d 5869 |
. . . 4
⊢ (𝑦 = 𝐵 → ((1st ‘𝐴)
·N (1st ‘𝑦)) = ((1st ‘𝐴)
·N (1st ‘𝐵))) |
18 | | fveq2 5496 |
. . . . 5
⊢ (𝑦 = 𝐵 → (2nd ‘𝑦) = (2nd ‘𝐵)) |
19 | 18 | oveq2d 5869 |
. . . 4
⊢ (𝑦 = 𝐵 → ((2nd ‘𝐴)
·N (2nd ‘𝑦)) = ((2nd ‘𝐴)
·N (2nd ‘𝐵))) |
20 | 17, 19 | opeq12d 3773 |
. . 3
⊢ (𝑦 = 𝐵 → 〈((1st ‘𝐴)
·N (1st ‘𝑦)), ((2nd ‘𝐴) ·N
(2nd ‘𝑦))〉 = 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) |
21 | | df-mpq 7307 |
. . 3
⊢
·pQ = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ 〈((1st
‘𝑥)
·N (1st ‘𝑦)), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |
22 | 15, 20, 21 | ovmpog 5987 |
. 2
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N) ∧ 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉 ∈ V) → (𝐴 ·pQ 𝐵) = 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) |
23 | 10, 22 | mpd3an3 1333 |
1
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·pQ 𝐵) = 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) |