Step | Hyp | Ref
| Expression |
1 | | imassrn 6025 |
. . 3
β’ (πΉ β π) β ran πΉ |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
4 | 2, 3 | mhmf 18612 |
. . . . 5
β’ (πΉ β (π MndHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
5 | 4 | adantr 482 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
6 | 5 | frnd 6677 |
. . 3
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β ran πΉ β (Baseβπ)) |
7 | 1, 6 | sstrid 3956 |
. 2
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (πΉ β π) β (Baseβπ)) |
8 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
9 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
10 | 8, 9 | mhm0 18615 |
. . . 4
β’ (πΉ β (π MndHom π) β (πΉβ(0gβπ)) = (0gβπ)) |
11 | 10 | adantr 482 |
. . 3
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (πΉβ(0gβπ)) = (0gβπ)) |
12 | 5 | ffnd 6670 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β πΉ Fn (Baseβπ)) |
13 | 2 | submss 18625 |
. . . . 5
β’ (π β (SubMndβπ) β π β (Baseβπ)) |
14 | 13 | adantl 483 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β π β (Baseβπ)) |
15 | 8 | subm0cl 18627 |
. . . . 5
β’ (π β (SubMndβπ) β
(0gβπ)
β π) |
16 | 15 | adantl 483 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (0gβπ) β π) |
17 | | fnfvima 7184 |
. . . 4
β’ ((πΉ Fn (Baseβπ) β§ π β (Baseβπ) β§ (0gβπ) β π) β (πΉβ(0gβπ)) β (πΉ β π)) |
18 | 12, 14, 16, 17 | syl3anc 1372 |
. . 3
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (πΉβ(0gβπ)) β (πΉ β π)) |
19 | 11, 18 | eqeltrrd 2835 |
. 2
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (0gβπ) β (πΉ β π)) |
20 | | simpll 766 |
. . . . . . . . 9
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β πΉ β (π MndHom π)) |
21 | 14 | adantr 482 |
. . . . . . . . . 10
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β π β (Baseβπ)) |
22 | | simprl 770 |
. . . . . . . . . 10
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β π§ β π) |
23 | 21, 22 | sseldd 3946 |
. . . . . . . . 9
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β π§ β (Baseβπ)) |
24 | | simprr 772 |
. . . . . . . . . 10
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β π₯ β π) |
25 | 21, 24 | sseldd 3946 |
. . . . . . . . 9
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β π₯ β (Baseβπ)) |
26 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
27 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
28 | 2, 26, 27 | mhmlin 18614 |
. . . . . . . . 9
β’ ((πΉ β (π MndHom π) β§ π§ β (Baseβπ) β§ π₯ β (Baseβπ)) β (πΉβ(π§(+gβπ)π₯)) = ((πΉβπ§)(+gβπ)(πΉβπ₯))) |
29 | 20, 23, 25, 28 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β (πΉβ(π§(+gβπ)π₯)) = ((πΉβπ§)(+gβπ)(πΉβπ₯))) |
30 | 12 | adantr 482 |
. . . . . . . . 9
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β πΉ Fn (Baseβπ)) |
31 | 26 | submcl 18628 |
. . . . . . . . . . 11
β’ ((π β (SubMndβπ) β§ π§ β π β§ π₯ β π) β (π§(+gβπ)π₯) β π) |
32 | 31 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π β (SubMndβπ) β§ (π§ β π β§ π₯ β π)) β (π§(+gβπ)π₯) β π) |
33 | 32 | adantll 713 |
. . . . . . . . 9
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β (π§(+gβπ)π₯) β π) |
34 | | fnfvima 7184 |
. . . . . . . . 9
β’ ((πΉ Fn (Baseβπ) β§ π β (Baseβπ) β§ (π§(+gβπ)π₯) β π) β (πΉβ(π§(+gβπ)π₯)) β (πΉ β π)) |
35 | 30, 21, 33, 34 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β (πΉβ(π§(+gβπ)π₯)) β (πΉ β π)) |
36 | 29, 35 | eqeltrrd 2835 |
. . . . . . 7
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ (π§ β π β§ π₯ β π)) β ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π)) |
37 | 36 | anassrs 469 |
. . . . . 6
β’ ((((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ π§ β π) β§ π₯ β π) β ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π)) |
38 | 37 | ralrimiva 3140 |
. . . . 5
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ π§ β π) β βπ₯ β π ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π)) |
39 | | oveq2 7366 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ₯) β ((πΉβπ§)(+gβπ)π¦) = ((πΉβπ§)(+gβπ)(πΉβπ₯))) |
40 | 39 | eleq1d 2819 |
. . . . . . . 8
β’ (π¦ = (πΉβπ₯) β (((πΉβπ§)(+gβπ)π¦) β (πΉ β π) β ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π))) |
41 | 40 | ralima 7189 |
. . . . . . 7
β’ ((πΉ Fn (Baseβπ) β§ π β (Baseβπ)) β (βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π) β βπ₯ β π ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π))) |
42 | 12, 14, 41 | syl2anc 585 |
. . . . . 6
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π) β βπ₯ β π ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π))) |
43 | 42 | adantr 482 |
. . . . 5
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ π§ β π) β (βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π) β βπ₯ β π ((πΉβπ§)(+gβπ)(πΉβπ₯)) β (πΉ β π))) |
44 | 38, 43 | mpbird 257 |
. . . 4
β’ (((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β§ π§ β π) β βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π)) |
45 | 44 | ralrimiva 3140 |
. . 3
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β βπ§ β π βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π)) |
46 | | oveq1 7365 |
. . . . . . 7
β’ (π₯ = (πΉβπ§) β (π₯(+gβπ)π¦) = ((πΉβπ§)(+gβπ)π¦)) |
47 | 46 | eleq1d 2819 |
. . . . . 6
β’ (π₯ = (πΉβπ§) β ((π₯(+gβπ)π¦) β (πΉ β π) β ((πΉβπ§)(+gβπ)π¦) β (πΉ β π))) |
48 | 47 | ralbidv 3171 |
. . . . 5
β’ (π₯ = (πΉβπ§) β (βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π) β βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π))) |
49 | 48 | ralima 7189 |
. . . 4
β’ ((πΉ Fn (Baseβπ) β§ π β (Baseβπ)) β (βπ₯ β (πΉ β π)βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π) β βπ§ β π βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π))) |
50 | 12, 14, 49 | syl2anc 585 |
. . 3
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (βπ₯ β (πΉ β π)βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π) β βπ§ β π βπ¦ β (πΉ β π)((πΉβπ§)(+gβπ)π¦) β (πΉ β π))) |
51 | 45, 50 | mpbird 257 |
. 2
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β βπ₯ β (πΉ β π)βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π)) |
52 | | mhmrcl2 18611 |
. . . 4
β’ (πΉ β (π MndHom π) β π β Mnd) |
53 | 52 | adantr 482 |
. . 3
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β π β Mnd) |
54 | 3, 9, 27 | issubm 18619 |
. . 3
β’ (π β Mnd β ((πΉ β π) β (SubMndβπ) β ((πΉ β π) β (Baseβπ) β§ (0gβπ) β (πΉ β π) β§ βπ₯ β (πΉ β π)βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π)))) |
55 | 53, 54 | syl 17 |
. 2
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β ((πΉ β π) β (SubMndβπ) β ((πΉ β π) β (Baseβπ) β§ (0gβπ) β (πΉ β π) β§ βπ₯ β (πΉ β π)βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π)))) |
56 | 7, 19, 51, 55 | mpbir3and 1343 |
1
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (πΉ β π) β (SubMndβπ)) |