Step | Hyp | Ref
| Expression |
1 | | df-plq 10857 |
. . . . 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-plpq 10851 |
. . . . 5
โข
+pQ = (๐ฅ โ (N ร
N), ๐ฆ โ
(N ร N) โฆ โจ(((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) +N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) |
7 | | opex 5426 |
. . . . 5
โข
โจ(((1st โ๐ฅ) ยทN
(2nd โ๐ฆ))
+N ((1st โ๐ฆ) ยทN
(2nd โ๐ฅ))), ((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
๐ต))) |