Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
๐ด โ
โ) |
2 | | simpl3 1193 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
๐: โโถ
โ) |
3 | | simpr 485 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
๐ฅ โ
โ) |
4 | | homval 30989 |
. . . . . 6
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
5 | 1, 2, 3, 4 | syl3anc 1371 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
6 | 5 | fveq2d 6895 |
. . . 4
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐โ((๐ด ยทop
๐)โ๐ฅ)) = (๐โ(๐ด ยทโ (๐โ๐ฅ)))) |
7 | | homulcl 31007 |
. . . . . 6
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
8 | 7 | 3adant2 1131 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
9 | | fvco3 6990 |
. . . . 5
โข (((๐ด ยทop
๐): โโถ โ
โง ๐ฅ โ โ)
โ ((๐ โ (๐ด ยทop
๐))โ๐ฅ) = (๐โ((๐ด ยทop ๐)โ๐ฅ))) |
10 | 8, 9 | sylan 580 |
. . . 4
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ โ (๐ด ยทop
๐))โ๐ฅ) = (๐โ((๐ด ยทop ๐)โ๐ฅ))) |
11 | | fvco3 6990 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
12 | 2, 3, 11 | syl2anc 584 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
13 | 12 | oveq2d 7424 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐ด
ยทโ ((๐ โ ๐)โ๐ฅ)) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
14 | | lnopf 31107 |
. . . . . . . . 9
โข (๐ โ LinOp โ ๐: โโถ
โ) |
15 | 14 | 3ad2ant2 1134 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ ๐: โโถ
โ) |
16 | | simp3 1138 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ ๐: โโถ
โ) |
17 | | fco 6741 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (๐ โ ๐): โโถ
โ) |
18 | 15, 16, 17 | syl2anc 584 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ (๐ โ ๐): โโถ
โ) |
19 | 18 | adantr 481 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐ โ ๐): โโถ
โ) |
20 | | homval 30989 |
. . . . . 6
โข ((๐ด โ โ โง (๐ โ ๐): โโถ โ โง ๐ฅ โ โ) โ ((๐ด ยทop
(๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ))) |
21 | 1, 19, 3, 20 | syl3anc 1371 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop (๐ โ ๐))โ๐ฅ) = (๐ด ยทโ ((๐ โ ๐)โ๐ฅ))) |
22 | | simpl2 1192 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
๐ โ
LinOp) |
23 | 16 | ffvelcdmda 7086 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
24 | | lnopmul 31215 |
. . . . . 6
โข ((๐ โ LinOp โง ๐ด โ โ โง (๐โ๐ฅ) โ โ) โ (๐โ(๐ด ยทโ (๐โ๐ฅ))) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
25 | 22, 1, 23, 24 | syl3anc 1371 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐โ(๐ด ยทโ (๐โ๐ฅ))) = (๐ด ยทโ (๐โ(๐โ๐ฅ)))) |
26 | 13, 21, 25 | 3eqtr4d 2782 |
. . . 4
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop (๐ โ ๐))โ๐ฅ) = (๐โ(๐ด ยทโ (๐โ๐ฅ)))) |
27 | 6, 10, 26 | 3eqtr4d 2782 |
. . 3
โข (((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ โ (๐ด ยทop
๐))โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ)) |
28 | 27 | ralrimiva 3146 |
. 2
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ โ๐ฅ โ
โ ((๐ โ (๐ด ยทop
๐))โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ)) |
29 | | fco 6741 |
. . . 4
โข ((๐: โโถ โ โง
(๐ด
ยทop ๐): โโถ โ) โ (๐ โ (๐ด ยทop ๐)): โโถ
โ) |
30 | 15, 8, 29 | syl2anc 584 |
. . 3
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ (๐ โ (๐ด ยทop
๐)): โโถ
โ) |
31 | | simp1 1136 |
. . . 4
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ ๐ด โ
โ) |
32 | | homulcl 31007 |
. . . 4
โข ((๐ด โ โ โง (๐ โ ๐): โโถ โ) โ (๐ด ยทop
(๐ โ ๐)): โโถ
โ) |
33 | 31, 18, 32 | syl2anc 584 |
. . 3
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ (๐ด
ยทop (๐ โ ๐)): โโถ
โ) |
34 | | hoeq 31008 |
. . 3
โข (((๐ โ (๐ด ยทop ๐)): โโถ โ
โง (๐ด
ยทop (๐ โ ๐)): โโถ โ) โ
(โ๐ฅ โ โ
((๐ โ (๐ด ยทop
๐))โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ) โ (๐ โ (๐ด ยทop ๐)) = (๐ด ยทop (๐ โ ๐)))) |
35 | 30, 33, 34 | syl2anc 584 |
. 2
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ (โ๐ฅ โ
โ ((๐ โ (๐ด ยทop
๐))โ๐ฅ) = ((๐ด ยทop (๐ โ ๐))โ๐ฅ) โ (๐ โ (๐ด ยทop ๐)) = (๐ด ยทop (๐ โ ๐)))) |
36 | 28, 35 | mpbid 231 |
1
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ)
โ (๐ โ (๐ด ยทop
๐)) = (๐ด ยทop (๐ โ ๐))) |