Step | Hyp | Ref
| Expression |
1 | | cntzmhm.z |
. . . . 5
โข ๐ = (Cntzโ๐บ) |
2 | | cntzmhm.y |
. . . . 5
โข ๐ = (Cntzโ๐ป) |
3 | 1, 2 | cntzmhm 19246 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ฅ โ (๐โ๐)) โ (๐นโ๐ฅ) โ (๐โ(๐น โ ๐))) |
4 | 3 | ralrimiva 3146 |
. . 3
โข (๐น โ (๐บ MndHom ๐ป) โ โ๐ฅ โ (๐โ๐)(๐นโ๐ฅ) โ (๐โ(๐น โ ๐))) |
5 | | ssralv 4050 |
. . 3
โข (๐ โ (๐โ๐) โ (โ๐ฅ โ (๐โ๐)(๐นโ๐ฅ) โ (๐โ(๐น โ ๐)) โ โ๐ฅ โ ๐ (๐นโ๐ฅ) โ (๐โ(๐น โ ๐)))) |
6 | 4, 5 | mpan9 507 |
. 2
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ โ๐ฅ โ ๐ (๐นโ๐ฅ) โ (๐โ(๐น โ ๐))) |
7 | | eqid 2732 |
. . . . . 6
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
8 | | eqid 2732 |
. . . . . 6
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
9 | 7, 8 | mhmf 18711 |
. . . . 5
โข (๐น โ (๐บ MndHom ๐ป) โ ๐น:(Baseโ๐บ)โถ(Baseโ๐ป)) |
10 | 9 | adantr 481 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ ๐น:(Baseโ๐บ)โถ(Baseโ๐ป)) |
11 | 10 | ffund 6721 |
. . 3
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ Fun ๐น) |
12 | | simpr 485 |
. . . . 5
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ ๐ โ (๐โ๐)) |
13 | 7, 1 | cntzssv 19233 |
. . . . 5
โข (๐โ๐) โ (Baseโ๐บ) |
14 | 12, 13 | sstrdi 3994 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ ๐ โ (Baseโ๐บ)) |
15 | 10 | fdmd 6728 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ dom ๐น = (Baseโ๐บ)) |
16 | 14, 15 | sseqtrrd 4023 |
. . 3
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ ๐ โ dom ๐น) |
17 | | funimass4 6956 |
. . 3
โข ((Fun
๐น โง ๐ โ dom ๐น) โ ((๐น โ ๐) โ (๐โ(๐น โ ๐)) โ โ๐ฅ โ ๐ (๐นโ๐ฅ) โ (๐โ(๐น โ ๐)))) |
18 | 11, 16, 17 | syl2anc 584 |
. 2
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ ((๐น โ ๐) โ (๐โ(๐น โ ๐)) โ โ๐ฅ โ ๐ (๐นโ๐ฅ) โ (๐โ(๐น โ ๐)))) |
19 | 6, 18 | mpbird 256 |
1
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ (๐โ๐)) โ (๐น โ ๐) โ (๐โ(๐น โ ๐))) |