Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . 5
โข (๐ฅ = ๐ด โ (1st โ๐ฅ) = (1st โ๐ด)) |
2 | 1 | oveq1d 7377 |
. . . 4
โข (๐ฅ = ๐ด โ ((1st โ๐ฅ)
ยทN (2nd โ๐ฆ)) = ((1st โ๐ด)
ยทN (2nd โ๐ฆ))) |
3 | | fveq2 6847 |
. . . . 5
โข (๐ฅ = ๐ด โ (2nd โ๐ฅ) = (2nd โ๐ด)) |
4 | 3 | oveq2d 7378 |
. . . 4
โข (๐ฅ = ๐ด โ ((1st โ๐ฆ)
ยทN (2nd โ๐ฅ)) = ((1st โ๐ฆ)
ยทN (2nd โ๐ด))) |
5 | 2, 4 | oveq12d 7380 |
. . 3
โข (๐ฅ = ๐ด โ (((1st โ๐ฅ)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))) = (((1st โ๐ด)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ด)))) |
6 | 3 | oveq1d 7377 |
. . 3
โข (๐ฅ = ๐ด โ ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ)) = ((2nd โ๐ด)
ยทN (2nd โ๐ฆ))) |
7 | 5, 6 | opeq12d 4843 |
. 2
โข (๐ฅ = ๐ด โ โจ(((1st โ๐ฅ)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ = โจ(((1st
โ๐ด)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ฆ))โฉ) |
8 | | fveq2 6847 |
. . . . 5
โข (๐ฆ = ๐ต โ (2nd โ๐ฆ) = (2nd โ๐ต)) |
9 | 8 | oveq2d 7378 |
. . . 4
โข (๐ฆ = ๐ต โ ((1st โ๐ด)
ยทN (2nd โ๐ฆ)) = ((1st โ๐ด)
ยทN (2nd โ๐ต))) |
10 | | fveq2 6847 |
. . . . 5
โข (๐ฆ = ๐ต โ (1st โ๐ฆ) = (1st โ๐ต)) |
11 | 10 | oveq1d 7377 |
. . . 4
โข (๐ฆ = ๐ต โ ((1st โ๐ฆ)
ยทN (2nd โ๐ด)) = ((1st โ๐ต)
ยทN (2nd โ๐ด))) |
12 | 9, 11 | oveq12d 7380 |
. . 3
โข (๐ฆ = ๐ต โ (((1st โ๐ด)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ด))) = (((1st โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
13 | 8 | oveq2d 7378 |
. . 3
โข (๐ฆ = ๐ต โ ((2nd โ๐ด)
ยทN (2nd โ๐ฆ)) = ((2nd โ๐ด)
ยทN (2nd โ๐ต))) |
14 | 12, 13 | opeq12d 4843 |
. 2
โข (๐ฆ = ๐ต โ โจ(((1st โ๐ด)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ฆ))โฉ = โจ(((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |
15 | | df-plpq 10851 |
. 2
โข
+pQ = (๐ฅ โ (N ร
N), ๐ฆ โ
(N ร N) โฆ โจ(((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) |
16 | | opex 5426 |
. 2
โข
โจ(((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ โ V |
17 | 7, 14, 15, 16 | ovmpo 7520 |
1
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด +pQ ๐ต) = โจ(((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |