Step | Hyp | Ref
| Expression |
1 | | xp1st 6165 |
. . . 4
โข (๐ด โ (N ร
N) โ (1st โ๐ด) โ N) |
2 | | xp1st 6165 |
. . . 4
โข (๐ต โ (N ร
N) โ (1st โ๐ต) โ N) |
3 | | mulclpi 7326 |
. . . 4
โข
(((1st โ๐ด) โ N โง
(1st โ๐ต)
โ N) โ ((1st โ๐ด) ยทN
(1st โ๐ต))
โ N) |
4 | 1, 2, 3 | syl2an 289 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ((1st
โ๐ด)
ยทN (1st โ๐ต)) โ N) |
5 | | xp2nd 6166 |
. . . 4
โข (๐ด โ (N ร
N) โ (2nd โ๐ด) โ N) |
6 | | xp2nd 6166 |
. . . 4
โข (๐ต โ (N ร
N) โ (2nd โ๐ต) โ N) |
7 | | mulclpi 7326 |
. . . 4
โข
(((2nd โ๐ด) โ N โง
(2nd โ๐ต)
โ N) โ ((2nd โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
8 | 5, 6, 7 | syl2an 289 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ((2nd
โ๐ด)
ยทN (2nd โ๐ต)) โ N) |
9 | | opexg 4228 |
. . 3
โข
((((1st โ๐ด) ยทN
(1st โ๐ต))
โ N โง ((2nd โ๐ด) ยทN
(2nd โ๐ต))
โ N) โ โจ((1st โ๐ด) ยทN
(1st โ๐ต)),
((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ โ V) |
10 | 4, 8, 9 | syl2anc 411 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ โจ((1st
โ๐ด)
ยทN (1st โ๐ต)), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ โ V) |
11 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = ๐ด โ (1st โ๐ฅ) = (1st โ๐ด)) |
12 | 11 | oveq1d 5889 |
. . . 4
โข (๐ฅ = ๐ด โ ((1st โ๐ฅ)
ยทN (1st โ๐ฆ)) = ((1st โ๐ด)
ยทN (1st โ๐ฆ))) |
13 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = ๐ด โ (2nd โ๐ฅ) = (2nd โ๐ด)) |
14 | 13 | oveq1d 5889 |
. . . 4
โข (๐ฅ = ๐ด โ ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ)) = ((2nd โ๐ด)
ยทN (2nd โ๐ฆ))) |
15 | 12, 14 | opeq12d 3786 |
. . 3
โข (๐ฅ = ๐ด โ โจ((1st โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ = โจ((1st
โ๐ด)
ยทN (1st โ๐ฆ)), ((2nd โ๐ด) ยทN
(2nd โ๐ฆ))โฉ) |
16 | | fveq2 5515 |
. . . . 5
โข (๐ฆ = ๐ต โ (1st โ๐ฆ) = (1st โ๐ต)) |
17 | 16 | oveq2d 5890 |
. . . 4
โข (๐ฆ = ๐ต โ ((1st โ๐ด)
ยทN (1st โ๐ฆ)) = ((1st โ๐ด)
ยทN (1st โ๐ต))) |
18 | | fveq2 5515 |
. . . . 5
โข (๐ฆ = ๐ต โ (2nd โ๐ฆ) = (2nd โ๐ต)) |
19 | 18 | oveq2d 5890 |
. . . 4
โข (๐ฆ = ๐ต โ ((2nd โ๐ด)
ยทN (2nd โ๐ฆ)) = ((2nd โ๐ด)
ยทN (2nd โ๐ต))) |
20 | 17, 19 | opeq12d 3786 |
. . 3
โข (๐ฆ = ๐ต โ โจ((1st โ๐ด)
ยทN (1st โ๐ฆ)), ((2nd โ๐ด) ยทN
(2nd โ๐ฆ))โฉ = โจ((1st
โ๐ด)
ยทN (1st โ๐ต)), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |
21 | | df-mpq 7343 |
. . 3
โข
ยทpQ = (๐ฅ โ (N ร
N), ๐ฆ โ
(N ร N) โฆ โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) |
22 | 15, 20, 21 | ovmpog 6008 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง โจ((1st
โ๐ด)
ยทN (1st โ๐ต)), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ โ V) โ (๐ด ยทpQ ๐ต) = โจ((1st
โ๐ด)
ยทN (1st โ๐ต)), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |
23 | 10, 22 | mpd3an3 1338 |
1
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ยทpQ ๐ต) = โจ((1st
โ๐ด)
ยทN (1st โ๐ต)), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |