Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . 4
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
2 | | eqid 2732 |
. . . 4
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
3 | 1, 2 | mhmf 18676 |
. . 3
โข (๐น โ (๐บ MndHom ๐ป) โ ๐น:(Baseโ๐บ)โถ(Baseโ๐ป)) |
4 | | cntzmhm.z |
. . . . 5
โข ๐ = (Cntzโ๐บ) |
5 | 1, 4 | cntzssv 19191 |
. . . 4
โข (๐โ๐) โ (Baseโ๐บ) |
6 | 5 | sseli 3978 |
. . 3
โข (๐ด โ (๐โ๐) โ ๐ด โ (Baseโ๐บ)) |
7 | | ffvelcdm 7083 |
. . 3
โข ((๐น:(Baseโ๐บ)โถ(Baseโ๐ป) โง ๐ด โ (Baseโ๐บ)) โ (๐นโ๐ด) โ (Baseโ๐ป)) |
8 | 3, 6, 7 | syl2an 596 |
. 2
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ (๐นโ๐ด) โ (Baseโ๐ป)) |
9 | | eqid 2732 |
. . . . . . . 8
โข
(+gโ๐บ) = (+gโ๐บ) |
10 | 9, 4 | cntzi 19192 |
. . . . . . 7
โข ((๐ด โ (๐โ๐) โง ๐ฅ โ ๐) โ (๐ด(+gโ๐บ)๐ฅ) = (๐ฅ(+gโ๐บ)๐ด)) |
11 | 10 | adantll 712 |
. . . . . 6
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ (๐ด(+gโ๐บ)๐ฅ) = (๐ฅ(+gโ๐บ)๐ด)) |
12 | 11 | fveq2d 6895 |
. . . . 5
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ (๐นโ(๐ด(+gโ๐บ)๐ฅ)) = (๐นโ(๐ฅ(+gโ๐บ)๐ด))) |
13 | | simpll 765 |
. . . . . 6
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ ๐น โ (๐บ MndHom ๐ป)) |
14 | 6 | ad2antlr 725 |
. . . . . 6
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ ๐ด โ (Baseโ๐บ)) |
15 | 1, 4 | cntzrcl 19190 |
. . . . . . . . 9
โข (๐ด โ (๐โ๐) โ (๐บ โ V โง ๐ โ (Baseโ๐บ))) |
16 | 15 | adantl 482 |
. . . . . . . 8
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ (๐บ โ V โง ๐ โ (Baseโ๐บ))) |
17 | 16 | simprd 496 |
. . . . . . 7
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ ๐ โ (Baseโ๐บ)) |
18 | 17 | sselda 3982 |
. . . . . 6
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ ๐ฅ โ (Baseโ๐บ)) |
19 | | eqid 2732 |
. . . . . . 7
โข
(+gโ๐ป) = (+gโ๐ป) |
20 | 1, 9, 19 | mhmlin 18678 |
. . . . . 6
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (Baseโ๐บ) โง ๐ฅ โ (Baseโ๐บ)) โ (๐นโ(๐ด(+gโ๐บ)๐ฅ)) = ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ))) |
21 | 13, 14, 18, 20 | syl3anc 1371 |
. . . . 5
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ (๐นโ(๐ด(+gโ๐บ)๐ฅ)) = ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ))) |
22 | 1, 9, 19 | mhmlin 18678 |
. . . . . 6
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ฅ โ (Baseโ๐บ) โง ๐ด โ (Baseโ๐บ)) โ (๐นโ(๐ฅ(+gโ๐บ)๐ด)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด))) |
23 | 13, 18, 14, 22 | syl3anc 1371 |
. . . . 5
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ (๐นโ(๐ฅ(+gโ๐บ)๐ด)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด))) |
24 | 12, 21, 23 | 3eqtr3d 2780 |
. . . 4
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โง ๐ฅ โ ๐) โ ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด))) |
25 | 24 | ralrimiva 3146 |
. . 3
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ โ๐ฅ โ ๐ ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด))) |
26 | 3 | adantr 481 |
. . . . 5
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ ๐น:(Baseโ๐บ)โถ(Baseโ๐ป)) |
27 | 26 | ffnd 6718 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ ๐น Fn (Baseโ๐บ)) |
28 | | oveq2 7416 |
. . . . . 6
โข (๐ฆ = (๐นโ๐ฅ) โ ((๐นโ๐ด)(+gโ๐ป)๐ฆ) = ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ))) |
29 | | oveq1 7415 |
. . . . . 6
โข (๐ฆ = (๐นโ๐ฅ) โ (๐ฆ(+gโ๐ป)(๐นโ๐ด)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด))) |
30 | 28, 29 | eqeq12d 2748 |
. . . . 5
โข (๐ฆ = (๐นโ๐ฅ) โ (((๐นโ๐ด)(+gโ๐ป)๐ฆ) = (๐ฆ(+gโ๐ป)(๐นโ๐ด)) โ ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด)))) |
31 | 30 | ralima 7239 |
. . . 4
โข ((๐น Fn (Baseโ๐บ) โง ๐ โ (Baseโ๐บ)) โ (โ๐ฆ โ (๐น โ ๐)((๐นโ๐ด)(+gโ๐ป)๐ฆ) = (๐ฆ(+gโ๐ป)(๐นโ๐ด)) โ โ๐ฅ โ ๐ ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด)))) |
32 | 27, 17, 31 | syl2anc 584 |
. . 3
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ (โ๐ฆ โ (๐น โ ๐)((๐นโ๐ด)(+gโ๐ป)๐ฆ) = (๐ฆ(+gโ๐ป)(๐นโ๐ด)) โ โ๐ฅ โ ๐ ((๐นโ๐ด)(+gโ๐ป)(๐นโ๐ฅ)) = ((๐นโ๐ฅ)(+gโ๐ป)(๐นโ๐ด)))) |
33 | 25, 32 | mpbird 256 |
. 2
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ โ๐ฆ โ (๐น โ ๐)((๐นโ๐ด)(+gโ๐ป)๐ฆ) = (๐ฆ(+gโ๐ป)(๐นโ๐ด))) |
34 | | imassrn 6070 |
. . . 4
โข (๐น โ ๐) โ ran ๐น |
35 | 26 | frnd 6725 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ ran ๐น โ (Baseโ๐ป)) |
36 | 34, 35 | sstrid 3993 |
. . 3
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ (๐น โ ๐) โ (Baseโ๐ป)) |
37 | | cntzmhm.y |
. . . 4
โข ๐ = (Cntzโ๐ป) |
38 | 2, 19, 37 | elcntz 19185 |
. . 3
โข ((๐น โ ๐) โ (Baseโ๐ป) โ ((๐นโ๐ด) โ (๐โ(๐น โ ๐)) โ ((๐นโ๐ด) โ (Baseโ๐ป) โง โ๐ฆ โ (๐น โ ๐)((๐นโ๐ด)(+gโ๐ป)๐ฆ) = (๐ฆ(+gโ๐ป)(๐นโ๐ด))))) |
39 | 36, 38 | syl 17 |
. 2
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ ((๐นโ๐ด) โ (๐โ(๐น โ ๐)) โ ((๐นโ๐ด) โ (Baseโ๐ป) โง โ๐ฆ โ (๐น โ ๐)((๐นโ๐ด)(+gโ๐ป)๐ฆ) = (๐ฆ(+gโ๐ป)(๐นโ๐ด))))) |
40 | 8, 33, 39 | mpbir2and 711 |
1
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ด โ (๐โ๐)) โ (๐นโ๐ด) โ (๐โ(๐น โ ๐))) |