Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | 1, 2 | mhmf 18612 |
. . . . 5
β’ (πΉ β (π MndHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
4 | 3 | adantr 482 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
5 | 4 | ffnd 6670 |
. . 3
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β πΉ Fn (Baseβπ)) |
6 | 1, 2 | mhmf 18612 |
. . . . 5
β’ (πΊ β (π MndHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
7 | 6 | adantl 483 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
8 | 7 | ffnd 6670 |
. . 3
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β πΊ Fn (Baseβπ)) |
9 | | fndmin 6996 |
. . 3
β’ ((πΉ Fn (Baseβπ) β§ πΊ Fn (Baseβπ)) β dom (πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
10 | 5, 8, 9 | syl2anc 585 |
. 2
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β dom (πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
11 | | ssrab2 4038 |
. . . 4
β’ {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (Baseβπ) |
12 | 11 | a1i 11 |
. . 3
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (Baseβπ)) |
13 | | fveq2 6843 |
. . . . 5
β’ (π§ = (0gβπ) β (πΉβπ§) = (πΉβ(0gβπ))) |
14 | | fveq2 6843 |
. . . . 5
β’ (π§ = (0gβπ) β (πΊβπ§) = (πΊβ(0gβπ))) |
15 | 13, 14 | eqeq12d 2749 |
. . . 4
β’ (π§ = (0gβπ) β ((πΉβπ§) = (πΊβπ§) β (πΉβ(0gβπ)) = (πΊβ(0gβπ)))) |
16 | | mhmrcl1 18610 |
. . . . . 6
β’ (πΉ β (π MndHom π) β π β Mnd) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β π β Mnd) |
18 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
19 | 1, 18 | mndidcl 18576 |
. . . . 5
β’ (π β Mnd β
(0gβπ)
β (Baseβπ)) |
20 | 17, 19 | syl 17 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β (0gβπ) β (Baseβπ)) |
21 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
22 | 18, 21 | mhm0 18615 |
. . . . . 6
β’ (πΉ β (π MndHom π) β (πΉβ(0gβπ)) = (0gβπ)) |
23 | 22 | adantr 482 |
. . . . 5
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β (πΉβ(0gβπ)) = (0gβπ)) |
24 | 18, 21 | mhm0 18615 |
. . . . . 6
β’ (πΊ β (π MndHom π) β (πΊβ(0gβπ)) = (0gβπ)) |
25 | 24 | adantl 483 |
. . . . 5
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β (πΊβ(0gβπ)) = (0gβπ)) |
26 | 23, 25 | eqtr4d 2776 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β (πΉβ(0gβπ)) = (πΊβ(0gβπ))) |
27 | 15, 20, 26 | elrabd 3648 |
. . 3
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β (0gβπ) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
28 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π§ = (π₯(+gβπ)π¦) β (πΉβπ§) = (πΉβ(π₯(+gβπ)π¦))) |
29 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π§ = (π₯(+gβπ)π¦) β (πΊβπ§) = (πΊβ(π₯(+gβπ)π¦))) |
30 | 28, 29 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π§ = (π₯(+gβπ)π¦) β ((πΉβπ§) = (πΊβπ§) β (πΉβ(π₯(+gβπ)π¦)) = (πΊβ(π₯(+gβπ)π¦)))) |
31 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β π β Mnd) |
32 | | simplrl 776 |
. . . . . . . . . . 11
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β π₯ β (Baseβπ)) |
33 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β π¦ β (Baseβπ)) |
34 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
35 | 1, 34 | mndcl 18569 |
. . . . . . . . . . 11
β’ ((π β Mnd β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) β (Baseβπ)) |
36 | 31, 32, 33, 35 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (π₯(+gβπ)π¦) β (Baseβπ)) |
37 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β πΉ β (π MndHom π)) |
38 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(+gβπ) = (+gβπ) |
39 | 1, 34, 38 | mhmlin 18614 |
. . . . . . . . . . . 12
β’ ((πΉ β (π MndHom π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
40 | 37, 32, 33, 39 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
41 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β πΊ β (π MndHom π)) |
42 | 1, 34, 38 | mhmlin 18614 |
. . . . . . . . . . . . 13
β’ ((πΊ β (π MndHom π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΊβ(π₯(+gβπ)π¦)) = ((πΊβπ₯)(+gβπ)(πΊβπ¦))) |
43 | 41, 32, 33, 42 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΊβ(π₯(+gβπ)π¦)) = ((πΊβπ₯)(+gβπ)(πΊβπ¦))) |
44 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΉβπ₯) = (πΊβπ₯)) |
45 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΉβπ¦) = (πΊβπ¦)) |
46 | 44, 45 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β ((πΉβπ₯)(+gβπ)(πΉβπ¦)) = ((πΊβπ₯)(+gβπ)(πΊβπ¦))) |
47 | 43, 46 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΊβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
48 | 40, 47 | eqtr4d 2776 |
. . . . . . . . . 10
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΉβ(π₯(+gβπ)π¦)) = (πΊβ(π₯(+gβπ)π¦))) |
49 | 30, 36, 48 | elrabd 3648 |
. . . . . . . . 9
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
50 | 49 | expr 458 |
. . . . . . . 8
β’ ((((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β§ π¦ β (Baseβπ)) β ((πΉβπ¦) = (πΊβπ¦) β (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
51 | 50 | ralrimiva 3140 |
. . . . . . 7
β’ (((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β βπ¦ β (Baseβπ)((πΉβπ¦) = (πΊβπ¦) β (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
52 | | fveq2 6843 |
. . . . . . . . 9
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
53 | | fveq2 6843 |
. . . . . . . . 9
β’ (π§ = π¦ β (πΊβπ§) = (πΊβπ¦)) |
54 | 52, 53 | eqeq12d 2749 |
. . . . . . . 8
β’ (π§ = π¦ β ((πΉβπ§) = (πΊβπ§) β (πΉβπ¦) = (πΊβπ¦))) |
55 | 54 | ralrab 3652 |
. . . . . . 7
β’
(βπ¦ β
{π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β βπ¦ β (Baseβπ)((πΉβπ¦) = (πΊβπ¦) β (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
56 | 51, 55 | sylibr 233 |
. . . . . 6
β’ (((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ (π₯ β (Baseβπ) β§ (πΉβπ₯) = (πΊβπ₯))) β βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
57 | 56 | expr 458 |
. . . . 5
β’ (((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β§ π₯ β (Baseβπ)) β ((πΉβπ₯) = (πΊβπ₯) β βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
58 | 57 | ralrimiva 3140 |
. . . 4
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β βπ₯ β (Baseβπ)((πΉβπ₯) = (πΊβπ₯) β βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
59 | | fveq2 6843 |
. . . . . 6
β’ (π§ = π₯ β (πΉβπ§) = (πΉβπ₯)) |
60 | | fveq2 6843 |
. . . . . 6
β’ (π§ = π₯ β (πΊβπ§) = (πΊβπ₯)) |
61 | 59, 60 | eqeq12d 2749 |
. . . . 5
β’ (π§ = π₯ β ((πΉβπ§) = (πΊβπ§) β (πΉβπ₯) = (πΊβπ₯))) |
62 | 61 | ralrab 3652 |
. . . 4
β’
(βπ₯ β
{π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β βπ₯ β (Baseβπ)((πΉβπ₯) = (πΊβπ₯) β βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
63 | 58, 62 | sylibr 233 |
. . 3
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β βπ₯ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
64 | 1, 18, 34 | issubm 18619 |
. . . 4
β’ (π β Mnd β ({π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (SubMndβπ) β ({π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (Baseβπ) β§ (0gβπ) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β§ βπ₯ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}))) |
65 | 17, 64 | syl 17 |
. . 3
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β ({π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (SubMndβπ) β ({π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (Baseβπ) β§ (0gβπ) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β§ βπ₯ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯(+gβπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}))) |
66 | 12, 27, 63, 65 | mpbir3and 1343 |
. 2
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (SubMndβπ)) |
67 | 10, 66 | eqeltrd 2834 |
1
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β dom (πΉ β© πΊ) β (SubMndβπ)) |