Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ๐
โ Mnd) |
2 | | simplr 768 |
. . . 4
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ๐ผ โ ๐) |
3 | | simpr3 1197 |
. . . 4
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ๐ด โ ๐ผ) |
4 | | pwsmulg.y |
. . . . 5
โข ๐ = (๐
โs ๐ผ) |
5 | | pwsmulg.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
6 | 4, 5 | pwspjmhm 18648 |
. . . 4
โข ((๐
โ Mnd โง ๐ผ โ ๐ โง ๐ด โ ๐ผ) โ (๐ฅ โ ๐ต โฆ (๐ฅโ๐ด)) โ (๐ MndHom ๐
)) |
7 | 1, 2, 3, 6 | syl3anc 1372 |
. . 3
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ (๐ฅ โ ๐ต โฆ (๐ฅโ๐ด)) โ (๐ MndHom ๐
)) |
8 | | simpr1 1195 |
. . 3
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ๐ โ
โ0) |
9 | | simpr2 1196 |
. . 3
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ๐ โ ๐ต) |
10 | | pwsmulg.s |
. . . 4
โข โ =
(.gโ๐) |
11 | | pwsmulg.t |
. . . 4
โข ยท =
(.gโ๐
) |
12 | 5, 10, 11 | mhmmulg 18925 |
. . 3
โข (((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด)) โ (๐ MndHom ๐
) โง ๐ โ โ0 โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ(๐ โ ๐)) = (๐ ยท ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ๐))) |
13 | 7, 8, 9, 12 | syl3anc 1372 |
. 2
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ(๐ โ ๐)) = (๐ ยท ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ๐))) |
14 | 4 | pwsmnd 18599 |
. . . . 5
โข ((๐
โ Mnd โง ๐ผ โ ๐) โ ๐ โ Mnd) |
15 | 14 | adantr 482 |
. . . 4
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ๐ โ Mnd) |
16 | 5, 10, 15, 8, 9 | mulgnn0cld 18905 |
. . 3
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ (๐ โ ๐) โ ๐ต) |
17 | | fveq1 6845 |
. . . 4
โข (๐ฅ = (๐ โ ๐) โ (๐ฅโ๐ด) = ((๐ โ ๐)โ๐ด)) |
18 | | eqid 2733 |
. . . 4
โข (๐ฅ โ ๐ต โฆ (๐ฅโ๐ด)) = (๐ฅ โ ๐ต โฆ (๐ฅโ๐ด)) |
19 | | fvex 6859 |
. . . 4
โข ((๐ โ ๐)โ๐ด) โ V |
20 | 17, 18, 19 | fvmpt 6952 |
. . 3
โข ((๐ โ ๐) โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ(๐ โ ๐)) = ((๐ โ ๐)โ๐ด)) |
21 | 16, 20 | syl 17 |
. 2
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ(๐ โ ๐)) = ((๐ โ ๐)โ๐ด)) |
22 | | fveq1 6845 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ฅโ๐ด) = (๐โ๐ด)) |
23 | | fvex 6859 |
. . . . 5
โข (๐โ๐ด) โ V |
24 | 22, 18, 23 | fvmpt 6952 |
. . . 4
โข (๐ โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ๐) = (๐โ๐ด)) |
25 | 9, 24 | syl 17 |
. . 3
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ๐) = (๐โ๐ด)) |
26 | 25 | oveq2d 7377 |
. 2
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ (๐ ยท ((๐ฅ โ ๐ต โฆ (๐ฅโ๐ด))โ๐)) = (๐ ยท (๐โ๐ด))) |
27 | 13, 21, 26 | 3eqtr3d 2781 |
1
โข (((๐
โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ((๐ โ ๐)โ๐ด) = (๐ ยท (๐โ๐ด))) |