Step | Hyp | Ref
| Expression |
1 | | mhmrcl1 18610 |
. . . 4
β’ (πΉ β (π MndHom π) β π β Mnd) |
2 | 1 | adantl 483 |
. . 3
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β π β Mnd) |
3 | | resmhm2.u |
. . . . 5
β’ π = (π βΎs π) |
4 | 3 | submmnd 18629 |
. . . 4
β’ (π β (SubMndβπ) β π β Mnd) |
5 | 4 | ad2antrr 725 |
. . 3
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β π β Mnd) |
6 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
7 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
8 | 6, 7 | mhmf 18612 |
. . . . . . . 8
β’ (πΉ β (π MndHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
9 | 8 | adantl 483 |
. . . . . . 7
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
10 | 9 | ffnd 6670 |
. . . . . 6
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β πΉ Fn (Baseβπ)) |
11 | | simplr 768 |
. . . . . 6
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β ran πΉ β π) |
12 | | df-f 6501 |
. . . . . 6
β’ (πΉ:(Baseβπ)βΆπ β (πΉ Fn (Baseβπ) β§ ran πΉ β π)) |
13 | 10, 11, 12 | sylanbrc 584 |
. . . . 5
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β πΉ:(Baseβπ)βΆπ) |
14 | 3 | submbas 18630 |
. . . . . . 7
β’ (π β (SubMndβπ) β π = (Baseβπ)) |
15 | 14 | ad2antrr 725 |
. . . . . 6
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β π = (Baseβπ)) |
16 | 15 | feq3d 6656 |
. . . . 5
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β (πΉ:(Baseβπ)βΆπ β πΉ:(Baseβπ)βΆ(Baseβπ))) |
17 | 13, 16 | mpbid 231 |
. . . 4
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
18 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
19 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
20 | 6, 18, 19 | mhmlin 18614 |
. . . . . . . 8
β’ ((πΉ β (π MndHom π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
21 | 20 | 3expb 1121 |
. . . . . . 7
β’ ((πΉ β (π MndHom π) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
22 | 21 | adantll 713 |
. . . . . 6
β’ ((((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
23 | 3, 19 | ressplusg 17176 |
. . . . . . . 8
β’ (π β (SubMndβπ) β
(+gβπ) =
(+gβπ)) |
24 | 23 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (+gβπ) = (+gβπ)) |
25 | 24 | oveqd 7375 |
. . . . . 6
β’ ((((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((πΉβπ₯)(+gβπ)(πΉβπ¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
26 | 22, 25 | eqtrd 2773 |
. . . . 5
β’ ((((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
27 | 26 | ralrimivva 3194 |
. . . 4
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
28 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
29 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
30 | 28, 29 | mhm0 18615 |
. . . . . 6
β’ (πΉ β (π MndHom π) β (πΉβ(0gβπ)) = (0gβπ)) |
31 | 30 | adantl 483 |
. . . . 5
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β (πΉβ(0gβπ)) = (0gβπ)) |
32 | 3, 29 | subm0 18631 |
. . . . . 6
β’ (π β (SubMndβπ) β
(0gβπ) =
(0gβπ)) |
33 | 32 | ad2antrr 725 |
. . . . 5
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β (0gβπ) = (0gβπ)) |
34 | 31, 33 | eqtrd 2773 |
. . . 4
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β (πΉβ(0gβπ)) = (0gβπ)) |
35 | 17, 27, 34 | 3jca 1129 |
. . 3
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦)) β§ (πΉβ(0gβπ)) = (0gβπ))) |
36 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
37 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
38 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
39 | 6, 36, 18, 37, 28, 38 | ismhm 18608 |
. . 3
β’ (πΉ β (π MndHom π) β ((π β Mnd β§ π β Mnd) β§ (πΉ:(Baseβπ)βΆ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦)) β§ (πΉβ(0gβπ)) = (0gβπ)))) |
40 | 2, 5, 35, 39 | syl21anbrc 1345 |
. 2
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β πΉ β (π MndHom π)) |
41 | 3 | resmhm2 18637 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β πΉ β (π MndHom π)) |
42 | 41 | ancoms 460 |
. . 3
β’ ((π β (SubMndβπ) β§ πΉ β (π MndHom π)) β πΉ β (π MndHom π)) |
43 | 42 | adantlr 714 |
. 2
β’ (((π β (SubMndβπ) β§ ran πΉ β π) β§ πΉ β (π MndHom π)) β πΉ β (π MndHom π)) |
44 | 40, 43 | impbida 800 |
1
β’ ((π β (SubMndβπ) β§ ran πΉ β π) β (πΉ β (π MndHom π) β πΉ β (π MndHom π))) |