Step | Hyp | Ref
| Expression |
1 | | 1nq 10871 |
. . 3
โข
1Q โ Q |
2 | | mulpqnq 10884 |
. . 3
โข ((๐ด โ Q โง
1Q โ Q) โ (๐ด ยทQ
1Q) = ([Q]โ(๐ด ยทpQ
1Q))) |
3 | 1, 2 | mpan2 690 |
. 2
โข (๐ด โ Q โ
(๐ด
ยทQ 1Q) =
([Q]โ(๐ด
ยทpQ
1Q))) |
4 | | relxp 5656 |
. . . . . . 7
โข Rel
(N ร N) |
5 | | elpqn 10868 |
. . . . . . 7
โข (๐ด โ Q โ
๐ด โ (N
ร N)) |
6 | | 1st2nd 7976 |
. . . . . . 7
โข ((Rel
(N ร N) โง ๐ด โ (N ร
N)) โ ๐ด
= โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . 6
โข (๐ด โ Q โ
๐ด = โจ(1st
โ๐ด), (2nd
โ๐ด)โฉ) |
8 | | df-1nq 10859 |
. . . . . . 7
โข
1Q = โจ1o,
1oโฉ |
9 | 8 | a1i 11 |
. . . . . 6
โข (๐ด โ Q โ
1Q = โจ1o,
1oโฉ) |
10 | 7, 9 | oveq12d 7380 |
. . . . 5
โข (๐ด โ Q โ
(๐ด
ยทpQ 1Q) =
(โจ(1st โ๐ด), (2nd โ๐ด)โฉ ยทpQ
โจ1o, 1oโฉ)) |
11 | | xp1st 7958 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ (1st โ๐ด) โ N) |
12 | 5, 11 | syl 17 |
. . . . . 6
โข (๐ด โ Q โ
(1st โ๐ด)
โ N) |
13 | | xp2nd 7959 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ (2nd โ๐ด) โ N) |
14 | 5, 13 | syl 17 |
. . . . . 6
โข (๐ด โ Q โ
(2nd โ๐ด)
โ N) |
15 | | 1pi 10826 |
. . . . . . 7
โข
1o โ N |
16 | 15 | a1i 11 |
. . . . . 6
โข (๐ด โ Q โ
1o โ N) |
17 | | mulpipq 10883 |
. . . . . 6
โข
((((1st โ๐ด) โ N โง
(2nd โ๐ด)
โ N) โง (1o โ N โง
1o โ N)) โ (โจ(1st
โ๐ด), (2nd
โ๐ด)โฉ
ยทpQ โจ1o, 1oโฉ) =
โจ((1st โ๐ด) ยทN
1o), ((2nd โ๐ด) ยทN
1o)โฉ) |
18 | 12, 14, 16, 16, 17 | syl22anc 838 |
. . . . 5
โข (๐ด โ Q โ
(โจ(1st โ๐ด), (2nd โ๐ด)โฉ ยทpQ
โจ1o, 1oโฉ) = โจ((1st โ๐ด)
ยทN 1o), ((2nd
โ๐ด)
ยทN 1o)โฉ) |
19 | | mulidpi 10829 |
. . . . . . . 8
โข
((1st โ๐ด) โ N โ
((1st โ๐ด)
ยทN 1o) = (1st
โ๐ด)) |
20 | 11, 19 | syl 17 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ ((1st โ๐ด) ยทN
1o) = (1st โ๐ด)) |
21 | | mulidpi 10829 |
. . . . . . . 8
โข
((2nd โ๐ด) โ N โ
((2nd โ๐ด)
ยทN 1o) = (2nd
โ๐ด)) |
22 | 13, 21 | syl 17 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ ((2nd โ๐ด) ยทN
1o) = (2nd โ๐ด)) |
23 | 20, 22 | opeq12d 4843 |
. . . . . 6
โข (๐ด โ (N ร
N) โ โจ((1st โ๐ด) ยทN
1o), ((2nd โ๐ด) ยทN
1o)โฉ = โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
24 | 5, 23 | syl 17 |
. . . . 5
โข (๐ด โ Q โ
โจ((1st โ๐ด) ยทN
1o), ((2nd โ๐ด) ยทN
1o)โฉ = โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
25 | 10, 18, 24 | 3eqtrd 2781 |
. . . 4
โข (๐ด โ Q โ
(๐ด
ยทpQ 1Q) =
โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
26 | 25, 7 | eqtr4d 2780 |
. . 3
โข (๐ด โ Q โ
(๐ด
ยทpQ 1Q) = ๐ด) |
27 | 26 | fveq2d 6851 |
. 2
โข (๐ด โ Q โ
([Q]โ(๐ด
ยทpQ 1Q)) =
([Q]โ๐ด)) |
28 | | nqerid 10876 |
. 2
โข (๐ด โ Q โ
([Q]โ๐ด)
= ๐ด) |
29 | 3, 27, 28 | 3eqtrd 2781 |
1
โข (๐ด โ Q โ
(๐ด
ยทQ 1Q) = ๐ด) |