Step | Hyp | Ref
| Expression |
1 | | df-mq 10858 |
. . . . 5
โข
ยทQ = (([Q] โ
ยทpQ ) โพ (Q ร
Q)) |
2 | 1 | fveq1i 6848 |
. . . 4
โข (
ยทQ โโจ๐ด, ๐ตโฉ) = ((([Q] โ
ยทpQ ) โพ (Q ร
Q))โโจ๐ด, ๐ตโฉ) |
3 | 2 | a1i 11 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ ( ยทQ โโจ๐ด, ๐ตโฉ) = ((([Q] โ
ยทpQ ) โพ (Q ร
Q))โโจ๐ด, ๐ตโฉ)) |
4 | | opelxpi 5675 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ โจ๐ด, ๐ตโฉ โ (Q
ร Q)) |
5 | 4 | fvresd 6867 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((([Q] โ ยทpQ )
โพ (Q ร Q))โโจ๐ด, ๐ตโฉ) = (([Q] โ
ยทpQ )โโจ๐ด, ๐ตโฉ)) |
6 | | df-mpq 10852 |
. . . . 5
โข
ยทpQ = (๐ฅ โ (N ร
N), ๐ฆ โ
(N ร N) โฆ โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) |
7 | | opex 5426 |
. . . . 5
โข
โจ((1st โ๐ฅ) ยทN
(1st โ๐ฆ)),
((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ โ V |
8 | 6, 7 | fnmpoi 8007 |
. . . 4
โข
ยทpQ Fn ((N ร
N) ร (N ร
N)) |
9 | | elpqn 10868 |
. . . . 5
โข (๐ด โ Q โ
๐ด โ (N
ร N)) |
10 | | elpqn 10868 |
. . . . 5
โข (๐ต โ Q โ
๐ต โ (N
ร N)) |
11 | | opelxpi 5675 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ โจ๐ด, ๐ตโฉ โ ((N ร
N) ร (N ร
N))) |
12 | 9, 10, 11 | syl2an 597 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ โจ๐ด, ๐ตโฉ โ ((N
ร N) ร (N ร
N))) |
13 | | fvco2 6943 |
. . . 4
โข ((
ยทpQ Fn ((N ร
N) ร (N ร N)) โง
โจ๐ด, ๐ตโฉ โ ((N ร
N) ร (N ร N))) โ
(([Q] โ ยทpQ
)โโจ๐ด, ๐ตโฉ) =
([Q]โ( ยทpQ
โโจ๐ด, ๐ตโฉ))) |
14 | 8, 12, 13 | sylancr 588 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (([Q] โ ยทpQ
)โโจ๐ด, ๐ตโฉ) =
([Q]โ( ยทpQ
โโจ๐ด, ๐ตโฉ))) |
15 | 3, 5, 14 | 3eqtrd 2781 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ ( ยทQ โโจ๐ด, ๐ตโฉ) = ([Q]โ(
ยทpQ โโจ๐ด, ๐ตโฉ))) |
16 | | df-ov 7365 |
. 2
โข (๐ด
ยทQ ๐ต) = ( ยทQ
โโจ๐ด, ๐ตโฉ) |
17 | | df-ov 7365 |
. . 3
โข (๐ด
ยทpQ ๐ต) = ( ยทpQ
โโจ๐ด, ๐ตโฉ) |
18 | 17 | fveq2i 6850 |
. 2
โข
([Q]โ(๐ด ยทpQ ๐ต)) = ([Q]โ(
ยทpQ โโจ๐ด, ๐ตโฉ)) |
19 | 15, 16, 18 | 3eqtr4g 2802 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
ยทQ ๐ต) = ([Q]โ(๐ด
ยทpQ ๐ต))) |