Step | Hyp | Ref
| Expression |
1 | | opelxpi 5675 |
. . 3
โข ((๐ด โ N โง
๐ต โ N)
โ โจ๐ด, ๐ตโฉ โ (N
ร N)) |
2 | | opelxpi 5675 |
. . 3
โข ((๐ถ โ N โง
๐ท โ N)
โ โจ๐ถ, ๐ทโฉ โ (N
ร N)) |
3 | | mulpipq2 10882 |
. . 3
โข
((โจ๐ด, ๐ตโฉ โ (N
ร N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โ (โจ๐ด, ๐ตโฉ ยทpQ
โจ๐ถ, ๐ทโฉ) = โจ((1st
โโจ๐ด, ๐ตโฉ)
ยทN (1st โโจ๐ถ, ๐ทโฉ)), ((2nd
โโจ๐ด, ๐ตโฉ)
ยทN (2nd โโจ๐ถ, ๐ทโฉ))โฉ) |
4 | 1, 2, 3 | syl2an 597 |
. 2
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ (โจ๐ด, ๐ตโฉ ยทpQ
โจ๐ถ, ๐ทโฉ) = โจ((1st
โโจ๐ด, ๐ตโฉ)
ยทN (1st โโจ๐ถ, ๐ทโฉ)), ((2nd
โโจ๐ด, ๐ตโฉ)
ยทN (2nd โโจ๐ถ, ๐ทโฉ))โฉ) |
5 | | op1stg 7938 |
. . . 4
โข ((๐ด โ N โง
๐ต โ N)
โ (1st โโจ๐ด, ๐ตโฉ) = ๐ด) |
6 | | op1stg 7938 |
. . . 4
โข ((๐ถ โ N โง
๐ท โ N)
โ (1st โโจ๐ถ, ๐ทโฉ) = ๐ถ) |
7 | 5, 6 | oveqan12d 7381 |
. . 3
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ((1st โโจ๐ด, ๐ตโฉ) ยทN
(1st โโจ๐ถ, ๐ทโฉ)) = (๐ด ยทN ๐ถ)) |
8 | | op2ndg 7939 |
. . . 4
โข ((๐ด โ N โง
๐ต โ N)
โ (2nd โโจ๐ด, ๐ตโฉ) = ๐ต) |
9 | | op2ndg 7939 |
. . . 4
โข ((๐ถ โ N โง
๐ท โ N)
โ (2nd โโจ๐ถ, ๐ทโฉ) = ๐ท) |
10 | 8, 9 | oveqan12d 7381 |
. . 3
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ((2nd โโจ๐ด, ๐ตโฉ) ยทN
(2nd โโจ๐ถ, ๐ทโฉ)) = (๐ต ยทN ๐ท)) |
11 | 7, 10 | opeq12d 4843 |
. 2
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ โจ((1st โโจ๐ด, ๐ตโฉ) ยทN
(1st โโจ๐ถ, ๐ทโฉ)), ((2nd
โโจ๐ด, ๐ตโฉ)
ยทN (2nd โโจ๐ถ, ๐ทโฉ))โฉ = โจ(๐ด ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ) |
12 | 4, 11 | eqtrd 2777 |
1
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ (โจ๐ด, ๐ตโฉ ยทpQ
โจ๐ถ, ๐ทโฉ) = โจ(๐ด ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ) |