Step | Hyp | Ref
| Expression |
1 | | mulcl 11140 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
2 | | homval 30725 |
. . . . . . . . 9
โข (((๐ด ยท ๐ต) โ โ โง ๐: โโถ โ โง ๐ฅ โ โ) โ (((๐ด ยท ๐ต) ยทop ๐)โ๐ฅ) = ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ))) |
3 | 1, 2 | syl3an1 1164 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐: โโถ โ โง
๐ฅ โ โ) โ
(((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ))) |
4 | 3 | 3expia 1122 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐: โโถ โ)
โ (๐ฅ โ โ
โ (((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ)))) |
5 | 4 | 3impa 1111 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ (๐ฅ โ โ
โ (((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ)))) |
6 | 5 | imp 408 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ))) |
7 | | homval 30725 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ต
ยทop ๐)โ๐ฅ) = (๐ต ยทโ (๐โ๐ฅ))) |
8 | 7 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
(๐ด
ยทโ ((๐ต ยทop ๐)โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
9 | 8 | 3expa 1119 |
. . . . . . 7
โข (((๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐ด
ยทโ ((๐ต ยทop ๐)โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
10 | 9 | 3adantl1 1167 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐ด
ยทโ ((๐ต ยทop ๐)โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
11 | | ffvelcdm 7033 |
. . . . . . . . . 10
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
12 | | ax-hvmulass 29991 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐โ๐ฅ) โ โ) โ ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
13 | 11, 12 | syl3an3 1166 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐: โโถ โ โง
๐ฅ โ โ)) โ
((๐ด ยท ๐ต)
ยทโ (๐โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
14 | 13 | 3expa 1119 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐: โโถ โ โง
๐ฅ โ โ)) โ
((๐ด ยท ๐ต)
ยทโ (๐โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
15 | 14 | exp43 438 |
. . . . . . 7
โข (๐ด โ โ โ (๐ต โ โ โ (๐: โโถ โ โ
(๐ฅ โ โ โ
((๐ด ยท ๐ต)
ยทโ (๐โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ))))))) |
16 | 15 | 3imp1 1348 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด ยท ๐ต)
ยทโ (๐โ๐ฅ)) = (๐ด ยทโ (๐ต
ยทโ (๐โ๐ฅ)))) |
17 | 10, 16 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(๐ด
ยทโ ((๐ต ยทop ๐)โ๐ฅ)) = ((๐ด ยท ๐ต) ยทโ (๐โ๐ฅ))) |
18 | 6, 17 | eqtr4d 2776 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = (๐ด ยทโ ((๐ต ยทop
๐)โ๐ฅ))) |
19 | | homulcl 30743 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐: โโถ โ)
โ (๐ต
ยทop ๐): โโถ โ) |
20 | | homval 30725 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ต ยทop
๐): โโถ โ
โง ๐ฅ โ โ)
โ ((๐ด
ยทop (๐ต ยทop ๐))โ๐ฅ) = (๐ด ยทโ ((๐ต ยทop
๐)โ๐ฅ))) |
21 | 19, 20 | syl3an2 1165 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop (๐ต ยทop ๐))โ๐ฅ) = (๐ด ยทโ ((๐ต ยทop
๐)โ๐ฅ))) |
22 | 21 | 3expia 1122 |
. . . . . 6
โข ((๐ด โ โ โง (๐ต โ โ โง ๐: โโถ โ))
โ (๐ฅ โ โ
โ ((๐ด
ยทop (๐ต ยทop ๐))โ๐ฅ) = (๐ด ยทโ ((๐ต ยทop
๐)โ๐ฅ)))) |
23 | 22 | 3impb 1116 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ (๐ฅ โ โ
โ ((๐ด
ยทop (๐ต ยทop ๐))โ๐ฅ) = (๐ด ยทโ ((๐ต ยทop
๐)โ๐ฅ)))) |
24 | 23 | imp 408 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop (๐ต ยทop ๐))โ๐ฅ) = (๐ด ยทโ ((๐ต ยทop
๐)โ๐ฅ))) |
25 | 18, 24 | eqtr4d 2776 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยทop (๐ต ยทop
๐))โ๐ฅ)) |
26 | 25 | ralrimiva 3140 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ โ๐ฅ โ
โ (((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยทop (๐ต ยทop
๐))โ๐ฅ)) |
27 | | homulcl 30743 |
. . . 4
โข (((๐ด ยท ๐ต) โ โ โง ๐: โโถ โ) โ ((๐ด ยท ๐ต) ยทop ๐): โโถ
โ) |
28 | 1, 27 | stoic3 1779 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด ยท ๐ต) ยทop
๐): โโถ
โ) |
29 | | homulcl 30743 |
. . . . 5
โข ((๐ด โ โ โง (๐ต ยทop
๐): โโถ
โ) โ (๐ด
ยทop (๐ต ยทop ๐)): โโถ
โ) |
30 | 19, 29 | sylan2 594 |
. . . 4
โข ((๐ด โ โ โง (๐ต โ โ โง ๐: โโถ โ))
โ (๐ด
ยทop (๐ต ยทop ๐)): โโถ
โ) |
31 | 30 | 3impb 1116 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop (๐ต ยทop ๐)): โโถ
โ) |
32 | | hoeq 30744 |
. . 3
โข ((((๐ด ยท ๐ต) ยทop ๐): โโถ โ โง
(๐ด
ยทop (๐ต ยทop ๐)): โโถ โ)
โ (โ๐ฅ โ
โ (((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยทop (๐ต ยทop
๐))โ๐ฅ) โ ((๐ด ยท ๐ต) ยทop ๐) = (๐ด ยทop (๐ต ยทop
๐)))) |
33 | 28, 31, 32 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ (โ๐ฅ โ
โ (((๐ด ยท ๐ต) ยทop
๐)โ๐ฅ) = ((๐ด ยทop (๐ต ยทop
๐))โ๐ฅ) โ ((๐ด ยท ๐ต) ยทop ๐) = (๐ด ยทop (๐ต ยทop
๐)))) |
34 | 26, 33 | mpbid 231 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด ยท ๐ต) ยทop
๐) = (๐ด ยทop (๐ต ยทop
๐))) |