Step | Hyp | Ref
| Expression |
1 | | fvco3 6941 |
. . . . . 6
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = ((๐ด ยทop ๐)โ(๐โ๐ฅ))) |
2 | 1 | 3ad2antl3 1188 |
. . . . 5
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = ((๐ด ยทop ๐)โ(๐โ๐ฅ))) |
3 | | fvco3 6941 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
4 | 3 | 3ad2antl3 1188 |
. . . . . . 7
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
5 | 4 | oveq2d 7374 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐ โ ๐)โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
6 | | ffvelcdm 7033 |
. . . . . . . . . 10
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
7 | | homval 30725 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐: โโถ โ โง
(๐โ๐ฅ) โ โ) โ ((๐ด ยทop ๐)โ(๐โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
8 | 6, 7 | syl3an3 1166 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐: โโถ โ โง
(๐: โโถ โ
โง ๐ฅ โ โ))
โ ((๐ด
ยทop ๐)โ(๐โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
9 | 8 | 3expa 1119 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐: โโถ โ) โง
(๐: โโถ โ
โง ๐ฅ โ โ))
โ ((๐ด
ยทop ๐)โ(๐โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
10 | 9 | exp43 438 |
. . . . . . 7
โข (๐ด โ โ โ (๐: โโถ โ โ
(๐: โโถ โ
โ (๐ฅ โ โ
โ ((๐ด
ยทop ๐)โ(๐โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ))))))) |
11 | 10 | 3imp1 1348 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop ๐)โ(๐โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
12 | 5, 11 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐ โ ๐)โ๐ฅ)) = ((๐ด ยทop ๐)โ(๐โ๐ฅ))) |
13 | 2, 12 | eqtr4d 2776 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ))) |
14 | | fco 6693 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (๐ โ ๐): โโถ
โ) |
15 | | homval 30725 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ โ ๐): โโถ โ โง ๐ฅ โ โ) โ ((๐ด ยทop
(๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ))) |
16 | 14, 15 | syl3an2 1165 |
. . . . . . 7
โข ((๐ด โ โ โง (๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop (๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ))) |
17 | 16 | 3expia 1122 |
. . . . . 6
โข ((๐ด โ โ โง (๐: โโถ โ โง
๐: โโถ
โ)) โ (๐ฅ โ
โ โ ((๐ด
ยทop (๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ)))) |
18 | 17 | 3impb 1116 |
. . . . 5
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (๐ฅ โ โ
โ ((๐ด
ยทop (๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ)))) |
19 | 18 | imp 408 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop (๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ))) |
20 | 13, 19 | eqtr4d 2776 |
. . 3
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ)) |
21 | 20 | ralrimiva 3140 |
. 2
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ โ๐ฅ โ
โ (((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ)) |
22 | | homulcl 30743 |
. . . 4
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
23 | | fco 6693 |
. . . 4
โข (((๐ด ยทop
๐): โโถ โ
โง ๐: โโถ
โ) โ ((๐ด
ยทop ๐) โ ๐): โโถ โ) |
24 | 22, 23 | stoic3 1779 |
. . 3
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ ((๐ด
ยทop ๐) โ ๐): โโถ โ) |
25 | | homulcl 30743 |
. . . . 5
โข ((๐ด โ โ โง (๐ โ ๐): โโถ โ) โ (๐ด ยทop
(๐ โ ๐)): โโถ
โ) |
26 | 14, 25 | sylan2 594 |
. . . 4
โข ((๐ด โ โ โง (๐: โโถ โ โง
๐: โโถ
โ)) โ (๐ด
ยทop (๐ โ ๐)): โโถ
โ) |
27 | 26 | 3impb 1116 |
. . 3
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (๐ด
ยทop (๐ โ ๐)): โโถ
โ) |
28 | | hoeq 30744 |
. . 3
โข ((((๐ด ยทop
๐) โ ๐): โโถ โ โง
(๐ด
ยทop (๐ โ ๐)): โโถ โ) โ
(โ๐ฅ โ โ
(((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ) โ ((๐ด ยทop ๐) โ ๐) = (๐ด ยทop (๐ โ ๐)))) |
29 | 24, 27, 28 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (โ๐ฅ โ
โ (((๐ด
ยทop ๐) โ ๐)โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ) โ ((๐ด ยทop ๐) โ ๐) = (๐ด ยทop (๐ โ ๐)))) |
30 | 21, 29 | mpbid 231 |
1
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ ((๐ด
ยทop ๐) โ ๐) = (๐ด ยทop (๐ โ ๐))) |