Step | Hyp | Ref
| Expression |
1 | | 2on 8430 |
. . . 4
β’
2o β On |
2 | | xpexg 7688 |
. . . 4
β’ ((πΌ β π β§ 2o β On) β
(πΌ Γ 2o)
β V) |
3 | 1, 2 | mpan2 690 |
. . 3
β’ (πΌ β π β (πΌ Γ 2o) β
V) |
4 | | frgpmhm.m |
. . . 4
β’ π = (freeMndβ(πΌ Γ
2o)) |
5 | 4 | frmdmnd 18677 |
. . 3
β’ ((πΌ Γ 2o) β V
β π β
Mnd) |
6 | 3, 5 | syl 17 |
. 2
β’ (πΌ β π β π β Mnd) |
7 | | frgpmhm.g |
. . . 4
β’ πΊ = (freeGrpβπΌ) |
8 | 7 | frgpgrp 19552 |
. . 3
β’ (πΌ β π β πΊ β Grp) |
9 | 8 | grpmndd 18768 |
. 2
β’ (πΌ β π β πΊ β Mnd) |
10 | | frgpmhm.w |
. . . . . . . . . 10
β’ π = (Baseβπ) |
11 | 4, 10 | frmdbas 18670 |
. . . . . . . . 9
β’ ((πΌ Γ 2o) β V
β π = Word (πΌ Γ
2o)) |
12 | | wrdexg 14421 |
. . . . . . . . . 10
β’ ((πΌ Γ 2o) β V
β Word (πΌ Γ
2o) β V) |
13 | | fvi 6921 |
. . . . . . . . . 10
β’ (Word
(πΌ Γ 2o)
β V β ( I βWord (πΌ Γ 2o)) = Word (πΌ Γ
2o)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
β’ ((πΌ Γ 2o) β V
β ( I βWord (πΌ
Γ 2o)) = Word (πΌ Γ 2o)) |
15 | 11, 14 | eqtr4d 2776 |
. . . . . . . 8
β’ ((πΌ Γ 2o) β V
β π = ( I βWord
(πΌ Γ
2o))) |
16 | 3, 15 | syl 17 |
. . . . . . 7
β’ (πΌ β π β π = ( I βWord (πΌ Γ 2o))) |
17 | 16 | eleq2d 2820 |
. . . . . 6
β’ (πΌ β π β (π₯ β π β π₯ β ( I βWord (πΌ Γ 2o)))) |
18 | 17 | biimpa 478 |
. . . . 5
β’ ((πΌ β π β§ π₯ β π) β π₯ β ( I βWord (πΌ Γ 2o))) |
19 | | frgpmhm.r |
. . . . . 6
β’ βΌ = (
~FG βπΌ) |
20 | | eqid 2733 |
. . . . . 6
β’ ( I
βWord (πΌ Γ
2o)) = ( I βWord (πΌ Γ 2o)) |
21 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
22 | 7, 19, 20, 21 | frgpeccl 19551 |
. . . . 5
β’ (π₯ β ( I βWord (πΌ Γ 2o)) β
[π₯] βΌ β
(BaseβπΊ)) |
23 | 18, 22 | syl 17 |
. . . 4
β’ ((πΌ β π β§ π₯ β π) β [π₯] βΌ β
(BaseβπΊ)) |
24 | | frgpmhm.f |
. . . 4
β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) |
25 | 23, 24 | fmptd 7066 |
. . 3
β’ (πΌ β π β πΉ:πβΆ(BaseβπΊ)) |
26 | 20, 19 | efger 19508 |
. . . . . . . 8
β’ βΌ Er ( I
βWord (πΌ Γ
2o)) |
27 | | ereq2 8662 |
. . . . . . . . 9
β’ (π = ( I βWord (πΌ Γ 2o)) β
( βΌ Er π β βΌ Er ( I βWord
(πΌ Γ
2o)))) |
28 | 16, 27 | syl 17 |
. . . . . . . 8
β’ (πΌ β π β ( βΌ Er π β βΌ Er ( I βWord
(πΌ Γ
2o)))) |
29 | 26, 28 | mpbiri 258 |
. . . . . . 7
β’ (πΌ β π β βΌ Er π) |
30 | 29 | adantr 482 |
. . . . . 6
β’ ((πΌ β π β§ (π β π β§ π β π)) β βΌ Er π) |
31 | 10 | fvexi 6860 |
. . . . . . 7
β’ π β V |
32 | 31 | a1i 11 |
. . . . . 6
β’ ((πΌ β π β§ (π β π β§ π β π)) β π β V) |
33 | 30, 32, 24 | divsfval 17437 |
. . . . 5
β’ ((πΌ β π β§ (π β π β§ π β π)) β (πΉβ(π ++ π)) = [(π ++ π)] βΌ ) |
34 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
35 | 4, 10, 34 | frmdadd 18673 |
. . . . . . 7
β’ ((π β π β§ π β π) β (π(+gβπ)π) = (π ++ π)) |
36 | 35 | adantl 483 |
. . . . . 6
β’ ((πΌ β π β§ (π β π β§ π β π)) β (π(+gβπ)π) = (π ++ π)) |
37 | 36 | fveq2d 6850 |
. . . . 5
β’ ((πΌ β π β§ (π β π β§ π β π)) β (πΉβ(π(+gβπ)π)) = (πΉβ(π ++ π))) |
38 | 30, 32, 24 | divsfval 17437 |
. . . . . . 7
β’ ((πΌ β π β§ (π β π β§ π β π)) β (πΉβπ) = [π] βΌ ) |
39 | 30, 32, 24 | divsfval 17437 |
. . . . . . 7
β’ ((πΌ β π β§ (π β π β§ π β π)) β (πΉβπ) = [π] βΌ ) |
40 | 38, 39 | oveq12d 7379 |
. . . . . 6
β’ ((πΌ β π β§ (π β π β§ π β π)) β ((πΉβπ)(+gβπΊ)(πΉβπ)) = ([π] βΌ
(+gβπΊ)[π] βΌ )) |
41 | 16 | eleq2d 2820 |
. . . . . . . . 9
β’ (πΌ β π β (π β π β π β ( I βWord (πΌ Γ 2o)))) |
42 | 16 | eleq2d 2820 |
. . . . . . . . 9
β’ (πΌ β π β (π β π β π β ( I βWord (πΌ Γ 2o)))) |
43 | 41, 42 | anbi12d 632 |
. . . . . . . 8
β’ (πΌ β π β ((π β π β§ π β π) β (π β ( I βWord (πΌ Γ 2o)) β§ π β ( I βWord (πΌ Γ
2o))))) |
44 | 43 | biimpa 478 |
. . . . . . 7
β’ ((πΌ β π β§ (π β π β§ π β π)) β (π β ( I βWord (πΌ Γ 2o)) β§ π β ( I βWord (πΌ Γ
2o)))) |
45 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
46 | 20, 7, 19, 45 | frgpadd 19553 |
. . . . . . 7
β’ ((π β ( I βWord (πΌ Γ 2o)) β§
π β ( I βWord
(πΌ Γ 2o)))
β ([π] βΌ
(+gβπΊ)[π] βΌ ) = [(π ++ π)] βΌ ) |
47 | 44, 46 | syl 17 |
. . . . . 6
β’ ((πΌ β π β§ (π β π β§ π β π)) β ([π] βΌ
(+gβπΊ)[π] βΌ ) = [(π ++ π)] βΌ ) |
48 | 40, 47 | eqtrd 2773 |
. . . . 5
β’ ((πΌ β π β§ (π β π β§ π β π)) β ((πΉβπ)(+gβπΊ)(πΉβπ)) = [(π ++ π)] βΌ ) |
49 | 33, 37, 48 | 3eqtr4d 2783 |
. . . 4
β’ ((πΌ β π β§ (π β π β§ π β π)) β (πΉβ(π(+gβπ)π)) = ((πΉβπ)(+gβπΊ)(πΉβπ))) |
50 | 49 | ralrimivva 3194 |
. . 3
β’ (πΌ β π β βπ β π βπ β π (πΉβ(π(+gβπ)π)) = ((πΉβπ)(+gβπΊ)(πΉβπ))) |
51 | 31 | a1i 11 |
. . . . 5
β’ (πΌ β π β π β V) |
52 | 29, 51, 24 | divsfval 17437 |
. . . 4
β’ (πΌ β π β (πΉββ
) = [β
] βΌ
) |
53 | 7, 19 | frgp0 19550 |
. . . . 5
β’ (πΌ β π β (πΊ β Grp β§ [β
] βΌ =
(0gβπΊ))) |
54 | 53 | simprd 497 |
. . . 4
β’ (πΌ β π β [β
] βΌ =
(0gβπΊ)) |
55 | 52, 54 | eqtrd 2773 |
. . 3
β’ (πΌ β π β (πΉββ
) = (0gβπΊ)) |
56 | 25, 50, 55 | 3jca 1129 |
. 2
β’ (πΌ β π β (πΉ:πβΆ(BaseβπΊ) β§ βπ β π βπ β π (πΉβ(π(+gβπ)π)) = ((πΉβπ)(+gβπΊ)(πΉβπ)) β§ (πΉββ
) = (0gβπΊ))) |
57 | 4 | frmd0 18678 |
. . 3
β’ β
=
(0gβπ) |
58 | | eqid 2733 |
. . 3
β’
(0gβπΊ) = (0gβπΊ) |
59 | 10, 21, 34, 45, 57, 58 | ismhm 18611 |
. 2
β’ (πΉ β (π MndHom πΊ) β ((π β Mnd β§ πΊ β Mnd) β§ (πΉ:πβΆ(BaseβπΊ) β§ βπ β π βπ β π (πΉβ(π(+gβπ)π)) = ((πΉβπ)(+gβπΊ)(πΉβπ)) β§ (πΉββ
) = (0gβπΊ)))) |
60 | 6, 9, 56, 59 | syl21anbrc 1345 |
1
β’ (πΌ β π β πΉ β (π MndHom πΊ)) |