Step | Hyp | Ref
| Expression |
1 | | issh 30456 |
. 2
โข (๐ป โ
Sโ โ ((๐ป โ โ โง 0โ
โ ๐ป) โง ((
+โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป))) |
2 | | ax-hfvadd 30248 |
. . . . . . 7
โข
+โ :( โ ร โ)โถ
โ |
3 | | ffun 6720 |
. . . . . . 7
โข (
+โ :( โ ร โ)โถ โ โ Fun
+โ ) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
โข Fun
+โ |
5 | | xpss12 5691 |
. . . . . . . 8
โข ((๐ป โ โ โง ๐ป โ โ) โ (๐ป ร ๐ป) โ ( โ ร
โ)) |
6 | 5 | anidms 567 |
. . . . . . 7
โข (๐ป โ โ โ (๐ป ร ๐ป) โ ( โ ร
โ)) |
7 | 2 | fdmi 6729 |
. . . . . . 7
โข dom
+โ = ( โ ร โ) |
8 | 6, 7 | sseqtrrdi 4033 |
. . . . . 6
โข (๐ป โ โ โ (๐ป ร ๐ป) โ dom +โ
) |
9 | | funimassov 7583 |
. . . . . 6
โข ((Fun
+โ โง (๐ป ร ๐ป) โ dom +โ ) โ
(( +โ โ (๐ป ร ๐ป)) โ ๐ป โ โ๐ฅ โ ๐ป โ๐ฆ โ ๐ป (๐ฅ +โ ๐ฆ) โ ๐ป)) |
10 | 4, 8, 9 | sylancr 587 |
. . . . 5
โข (๐ป โ โ โ ((
+โ โ (๐ป ร ๐ป)) โ ๐ป โ โ๐ฅ โ ๐ป โ๐ฆ โ ๐ป (๐ฅ +โ ๐ฆ) โ ๐ป)) |
11 | | ax-hfvmul 30253 |
. . . . . . 7
โข
ยทโ :(โ ร โ)โถ
โ |
12 | | ffun 6720 |
. . . . . . 7
โข (
ยทโ :(โ ร โ)โถ โ
โ Fun ยทโ ) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
โข Fun
ยทโ |
14 | | xpss2 5696 |
. . . . . . 7
โข (๐ป โ โ โ (โ
ร ๐ป) โ (โ
ร โ)) |
15 | 11 | fdmi 6729 |
. . . . . . 7
โข dom
ยทโ = (โ ร โ) |
16 | 14, 15 | sseqtrrdi 4033 |
. . . . . 6
โข (๐ป โ โ โ (โ
ร ๐ป) โ dom
ยทโ ) |
17 | | funimassov 7583 |
. . . . . 6
โข ((Fun
ยทโ โง (โ ร ๐ป) โ dom
ยทโ ) โ ((
ยทโ โ (โ ร ๐ป)) โ ๐ป โ โ๐ฅ โ โ โ๐ฆ โ ๐ป (๐ฅ ยทโ ๐ฆ) โ ๐ป)) |
18 | 13, 16, 17 | sylancr 587 |
. . . . 5
โข (๐ป โ โ โ ((
ยทโ โ (โ ร ๐ป)) โ ๐ป โ โ๐ฅ โ โ โ๐ฆ โ ๐ป (๐ฅ ยทโ ๐ฆ) โ ๐ป)) |
19 | 10, 18 | anbi12d 631 |
. . . 4
โข (๐ป โ โ โ (((
+โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป) โ (โ๐ฅ โ ๐ป โ๐ฆ โ ๐ป (๐ฅ +โ ๐ฆ) โ ๐ป โง โ๐ฅ โ โ โ๐ฆ โ ๐ป (๐ฅ ยทโ ๐ฆ) โ ๐ป))) |
20 | 19 | adantr 481 |
. . 3
โข ((๐ป โ โ โง
0โ โ ๐ป) โ ((( +โ โ
(๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป) โ (โ๐ฅ โ ๐ป โ๐ฆ โ ๐ป (๐ฅ +โ ๐ฆ) โ ๐ป โง โ๐ฅ โ โ โ๐ฆ โ ๐ป (๐ฅ ยทโ ๐ฆ) โ ๐ป))) |
21 | 20 | pm5.32i 575 |
. 2
โข (((๐ป โ โ โง
0โ โ ๐ป) โง (( +โ โ
(๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป)) โ ((๐ป โ โ โง 0โ
โ ๐ป) โง
(โ๐ฅ โ ๐ป โ๐ฆ โ ๐ป (๐ฅ +โ ๐ฆ) โ ๐ป โง โ๐ฅ โ โ โ๐ฆ โ ๐ป (๐ฅ ยทโ ๐ฆ) โ ๐ป))) |
22 | 1, 21 | bitri 274 |
1
โข (๐ป โ
Sโ โ ((๐ป โ โ โง 0โ
โ ๐ป) โง
(โ๐ฅ โ ๐ป โ๐ฆ โ ๐ป (๐ฅ +โ ๐ฆ) โ ๐ป โง โ๐ฅ โ โ โ๐ฆ โ ๐ป (๐ฅ ยทโ ๐ฆ) โ ๐ป))) |