Step | Hyp | Ref
| Expression |
1 | | frgpup3.k |
. . 3
β’ (π β πΎ β (πΊ GrpHom π»)) |
2 | | frgpup.x |
. . . 4
β’ π = (BaseβπΊ) |
3 | | frgpup.b |
. . . 4
β’ π΅ = (Baseβπ») |
4 | 2, 3 | ghmf 19145 |
. . 3
β’ (πΎ β (πΊ GrpHom π») β πΎ:πβΆπ΅) |
5 | | ffn 6711 |
. . 3
β’ (πΎ:πβΆπ΅ β πΎ Fn π) |
6 | 1, 4, 5 | 3syl 18 |
. 2
β’ (π β πΎ Fn π) |
7 | | frgpup.n |
. . . 4
β’ π = (invgβπ») |
8 | | frgpup.t |
. . . 4
β’ π = (π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), (πβ(πΉβπ¦)))) |
9 | | frgpup.h |
. . . 4
β’ (π β π» β Grp) |
10 | | frgpup.i |
. . . 4
β’ (π β πΌ β π) |
11 | | frgpup.a |
. . . 4
β’ (π β πΉ:πΌβΆπ΅) |
12 | | frgpup.w |
. . . 4
β’ π = ( I βWord (πΌ Γ
2o)) |
13 | | frgpup.r |
. . . 4
β’ βΌ = (
~FG βπΌ) |
14 | | frgpup.g |
. . . 4
β’ πΊ = (freeGrpβπΌ) |
15 | | frgpup.e |
. . . 4
β’ πΈ = ran (π β π β¦ β¨[π] βΌ , (π» Ξ£g
(π β π))β©) |
16 | 3, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15 | frgpup1 19695 |
. . 3
β’ (π β πΈ β (πΊ GrpHom π»)) |
17 | 2, 3 | ghmf 19145 |
. . 3
β’ (πΈ β (πΊ GrpHom π») β πΈ:πβΆπ΅) |
18 | | ffn 6711 |
. . 3
β’ (πΈ:πβΆπ΅ β πΈ Fn π) |
19 | 16, 17, 18 | 3syl 18 |
. 2
β’ (π β πΈ Fn π) |
20 | | eqid 2726 |
. . . . . . . . 9
β’
(freeMndβ(πΌ
Γ 2o)) = (freeMndβ(πΌ Γ 2o)) |
21 | 14, 20, 13 | frgpval 19678 |
. . . . . . . 8
β’ (πΌ β π β πΊ = ((freeMndβ(πΌ Γ 2o))
/s βΌ )) |
22 | 10, 21 | syl 17 |
. . . . . . 7
β’ (π β πΊ = ((freeMndβ(πΌ Γ 2o))
/s βΌ )) |
23 | | 2on 8481 |
. . . . . . . . . . 11
β’
2o β On |
24 | | xpexg 7734 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ 2o β On) β
(πΌ Γ 2o)
β V) |
25 | 10, 23, 24 | sylancl 585 |
. . . . . . . . . 10
β’ (π β (πΌ Γ 2o) β
V) |
26 | | wrdexg 14480 |
. . . . . . . . . 10
β’ ((πΌ Γ 2o) β V
β Word (πΌ Γ
2o) β V) |
27 | | fvi 6961 |
. . . . . . . . . 10
β’ (Word
(πΌ Γ 2o)
β V β ( I βWord (πΌ Γ 2o)) = Word (πΌ Γ
2o)) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . 9
β’ (π β ( I βWord (πΌ Γ 2o)) = Word
(πΌ Γ
2o)) |
29 | 12, 28 | eqtrid 2778 |
. . . . . . . 8
β’ (π β π = Word (πΌ Γ 2o)) |
30 | | eqid 2726 |
. . . . . . . . . 10
β’
(Baseβ(freeMndβ(πΌ Γ 2o))) =
(Baseβ(freeMndβ(πΌ Γ 2o))) |
31 | 20, 30 | frmdbas 18777 |
. . . . . . . . 9
β’ ((πΌ Γ 2o) β V
β (Baseβ(freeMndβ(πΌ Γ 2o))) = Word (πΌ Γ
2o)) |
32 | 25, 31 | syl 17 |
. . . . . . . 8
β’ (π β
(Baseβ(freeMndβ(πΌ Γ 2o))) = Word (πΌ Γ
2o)) |
33 | 29, 32 | eqtr4d 2769 |
. . . . . . 7
β’ (π β π = (Baseβ(freeMndβ(πΌ Γ
2o)))) |
34 | 13 | fvexi 6899 |
. . . . . . . 8
β’ βΌ β
V |
35 | 34 | a1i 11 |
. . . . . . 7
β’ (π β βΌ β
V) |
36 | | fvexd 6900 |
. . . . . . 7
β’ (π β (freeMndβ(πΌ Γ 2o)) β
V) |
37 | 22, 33, 35, 36 | qusbas 17500 |
. . . . . 6
β’ (π β (π / βΌ ) =
(BaseβπΊ)) |
38 | 2, 37 | eqtr4id 2785 |
. . . . 5
β’ (π β π = (π / βΌ )) |
39 | | eqimss 4035 |
. . . . 5
β’ (π = (π / βΌ ) β π β (π / βΌ )) |
40 | 38, 39 | syl 17 |
. . . 4
β’ (π β π β (π / βΌ )) |
41 | 40 | sselda 3977 |
. . 3
β’ ((π β§ π β π) β π β (π / βΌ )) |
42 | | eqid 2726 |
. . . 4
β’ (π / βΌ ) = (π / βΌ ) |
43 | | fveq2 6885 |
. . . . 5
β’ ([π‘] βΌ = π β (πΎβ[π‘] βΌ ) = (πΎβπ)) |
44 | | fveq2 6885 |
. . . . 5
β’ ([π‘] βΌ = π β (πΈβ[π‘] βΌ ) = (πΈβπ)) |
45 | 43, 44 | eqeq12d 2742 |
. . . 4
β’ ([π‘] βΌ = π β ((πΎβ[π‘] βΌ ) = (πΈβ[π‘] βΌ ) β (πΎβπ) = (πΈβπ))) |
46 | | simpr 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π) β π‘ β π) |
47 | 29 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π) β π = Word (πΌ Γ 2o)) |
48 | 46, 47 | eleqtrd 2829 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β π‘ β Word (πΌ Γ 2o)) |
49 | | wrdf 14475 |
. . . . . . . . . . . . 13
β’ (π‘ β Word (πΌ Γ 2o) β π‘:(0..^(β―βπ‘))βΆ(πΌ Γ 2o)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β π‘:(0..^(β―βπ‘))βΆ(πΌ Γ 2o)) |
51 | 50 | ffvelcdmda 7080 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β (π‘βπ) β (πΌ Γ 2o)) |
52 | | elxp2 5693 |
. . . . . . . . . . 11
β’ ((π‘βπ) β (πΌ Γ 2o) β βπ β πΌ βπ β 2o (π‘βπ) = β¨π, πβ©) |
53 | 51, 52 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β βπ β πΌ βπ β 2o (π‘βπ) = β¨π, πβ©) |
54 | | fveq2 6885 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
55 | 54 | fveq2d 6889 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π β (πβ(πΉβπ¦)) = (πβ(πΉβπ))) |
56 | 54, 55 | ifeq12d 4544 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β if(π§ = β
, (πΉβπ¦), (πβ(πΉβπ¦))) = if(π§ = β
, (πΉβπ), (πβ(πΉβπ)))) |
57 | | eqeq1 2730 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π§ = β
β π = β
)) |
58 | 57 | ifbid 4546 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β if(π§ = β
, (πΉβπ), (πβ(πΉβπ))) = if(π = β
, (πΉβπ), (πβ(πΉβπ)))) |
59 | | fvex 6898 |
. . . . . . . . . . . . . . . . 17
β’ (πΉβπ) β V |
60 | | fvex 6898 |
. . . . . . . . . . . . . . . . 17
β’ (πβ(πΉβπ)) β V |
61 | 59, 60 | ifex 4573 |
. . . . . . . . . . . . . . . 16
β’ if(π = β
, (πΉβπ), (πβ(πΉβπ))) β V |
62 | 56, 58, 8, 61 | ovmpo 7564 |
. . . . . . . . . . . . . . 15
β’ ((π β πΌ β§ π β 2o) β (πππ) = if(π = β
, (πΉβπ), (πβ(πΉβπ)))) |
63 | 62 | adantl 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β πΌ β§ π β 2o)) β (πππ) = if(π = β
, (πΉβπ), (πβ(πΉβπ)))) |
64 | | elpri 4645 |
. . . . . . . . . . . . . . . . 17
β’ (π β {β
, 1o}
β (π = β
β¨
π =
1o)) |
65 | | df2o3 8475 |
. . . . . . . . . . . . . . . . 17
β’
2o = {β
, 1o} |
66 | 64, 65 | eleq2s 2845 |
. . . . . . . . . . . . . . . 16
β’ (π β 2o β
(π = β
β¨ π =
1o)) |
67 | | frgpup3.e |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πΎ β π) = πΉ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β (πΎ β π) = πΉ) |
69 | 68 | fveq1d 6887 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β ((πΎ β π)βπ) = (πΉβπ)) |
70 | | frgpup.u |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π =
(varFGrpβπΌ) |
71 | 13, 70, 14, 2 | vrgpf 19688 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΌ β π β π:πΌβΆπ) |
72 | 10, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π:πΌβΆπ) |
73 | | fvco3 6984 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π:πΌβΆπ β§ π β πΌ) β ((πΎ β π)βπ) = (πΎβ(πβπ))) |
74 | 72, 73 | sylan 579 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β ((πΎ β π)βπ) = (πΎβ(πβπ))) |
75 | 69, 74 | eqtr3d 2768 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΌ) β (πΉβπ) = (πΎβ(πβπ))) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π = β
) β (πΉβπ) = (πΎβ(πβπ))) |
77 | | iftrue 4529 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β
β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΉβπ)) |
78 | 77 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π = β
) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΉβπ)) |
79 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β πΌ) β§ π = β
) β π = β
) |
80 | 79 | opeq2d 4875 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β πΌ) β§ π = β
) β β¨π, πβ© = β¨π, β
β©) |
81 | 80 | s1eqd 14557 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ π = β
) β β¨ββ¨π, πβ©ββ© =
β¨ββ¨π,
β
β©ββ©) |
82 | 81 | eceq1d 8744 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΌ) β§ π = β
) β [β¨ββ¨π, πβ©ββ©] βΌ =
[β¨ββ¨π,
β
β©ββ©] βΌ ) |
83 | 13, 70 | vrgpval 19687 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ β π β§ π β πΌ) β (πβπ) = [β¨ββ¨π, β
β©ββ©] βΌ
) |
84 | 10, 83 | sylan 579 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β (πβπ) = [β¨ββ¨π, β
β©ββ©] βΌ
) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΌ) β§ π = β
) β (πβπ) = [β¨ββ¨π, β
β©ββ©] βΌ
) |
86 | 82, 85 | eqtr4d 2769 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β πΌ) β§ π = β
) β [β¨ββ¨π, πβ©ββ©] βΌ = (πβπ)) |
87 | 86 | fveq2d 6889 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π = β
) β (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ ) = (πΎβ(πβπ))) |
88 | 76, 78, 87 | 3eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π = β
) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
89 | 75 | fveq2d 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β (πβ(πΉβπ)) = (πβ(πΎβ(πβπ)))) |
90 | 72 | ffvelcdmda 7080 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β (πβπ) β π) |
91 | | eqid 2726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(invgβπΊ) = (invgβπΊ) |
92 | 2, 91, 7 | ghminv 19148 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΎ β (πΊ GrpHom π») β§ (πβπ) β π) β (πΎβ((invgβπΊ)β(πβπ))) = (πβ(πΎβ(πβπ)))) |
93 | 1, 90, 92 | syl2an2r 682 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β (πΎβ((invgβπΊ)β(πβπ))) = (πβ(πΎβ(πβπ)))) |
94 | 89, 93 | eqtr4d 2769 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΌ) β (πβ(πΉβπ)) = (πΎβ((invgβπΊ)β(πβπ)))) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π = 1o) β (πβ(πΉβπ)) = (πΎβ((invgβπΊ)β(πβπ)))) |
96 | | 1n0 8489 |
. . . . . . . . . . . . . . . . . . . 20
β’
1o β β
|
97 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ π = 1o) β π = 1o) |
98 | 97 | neeq1d 2994 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΌ) β§ π = 1o) β (π β β
β 1o β
β
)) |
99 | 96, 98 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β πΌ) β§ π = 1o) β π β β
) |
100 | | ifnefalse 4535 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β
β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πβ(πΉβπ))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π = 1o) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πβ(πΉβπ))) |
102 | 97 | opeq2d 4875 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β πΌ) β§ π = 1o) β β¨π, πβ© = β¨π, 1oβ©) |
103 | 102 | s1eqd 14557 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ π = 1o) β
β¨ββ¨π, πβ©ββ© =
β¨ββ¨π,
1oβ©ββ©) |
104 | 103 | eceq1d 8744 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΌ) β§ π = 1o) β
[β¨ββ¨π,
πβ©ββ©] βΌ =
[β¨ββ¨π,
1oβ©ββ©] βΌ ) |
105 | 13, 70, 14, 91 | vrgpinv 19689 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ β π β§ π β πΌ) β ((invgβπΊ)β(πβπ)) = [β¨ββ¨π, 1oβ©ββ©] βΌ
) |
106 | 10, 105 | sylan 579 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β ((invgβπΊ)β(πβπ)) = [β¨ββ¨π, 1oβ©ββ©] βΌ
) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΌ) β§ π = 1o) β
((invgβπΊ)β(πβπ)) = [β¨ββ¨π, 1oβ©ββ©] βΌ
) |
108 | 104, 107 | eqtr4d 2769 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β πΌ) β§ π = 1o) β
[β¨ββ¨π,
πβ©ββ©] βΌ =
((invgβπΊ)β(πβπ))) |
109 | 108 | fveq2d 6889 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π = 1o) β (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ ) = (πΎβ((invgβπΊ)β(πβπ)))) |
110 | 95, 101, 109 | 3eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π = 1o) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
111 | 88, 110 | jaodan 954 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΌ) β§ (π = β
β¨ π = 1o)) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
112 | 66, 111 | sylan2 592 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΌ) β§ π β 2o) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
113 | 112 | anasss 466 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β πΌ β§ π β 2o)) β if(π = β
, (πΉβπ), (πβ(πΉβπ))) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
114 | 63, 113 | eqtrd 2766 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΌ β§ π β 2o)) β (πππ) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
115 | | fveq2 6885 |
. . . . . . . . . . . . . . 15
β’ ((π‘βπ) = β¨π, πβ© β (πβ(π‘βπ)) = (πββ¨π, πβ©)) |
116 | | df-ov 7408 |
. . . . . . . . . . . . . . 15
β’ (πππ) = (πββ¨π, πβ©) |
117 | 115, 116 | eqtr4di 2784 |
. . . . . . . . . . . . . 14
β’ ((π‘βπ) = β¨π, πβ© β (πβ(π‘βπ)) = (πππ)) |
118 | | s1eq 14556 |
. . . . . . . . . . . . . . . 16
β’ ((π‘βπ) = β¨π, πβ© β β¨β(π‘βπ)ββ© = β¨ββ¨π, πβ©ββ©) |
119 | 118 | eceq1d 8744 |
. . . . . . . . . . . . . . 15
β’ ((π‘βπ) = β¨π, πβ© β [β¨β(π‘βπ)ββ©] βΌ =
[β¨ββ¨π,
πβ©ββ©] βΌ
) |
120 | 119 | fveq2d 6889 |
. . . . . . . . . . . . . 14
β’ ((π‘βπ) = β¨π, πβ© β (πΎβ[β¨β(π‘βπ)ββ©] βΌ ) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ )) |
121 | 117, 120 | eqeq12d 2742 |
. . . . . . . . . . . . 13
β’ ((π‘βπ) = β¨π, πβ© β ((πβ(π‘βπ)) = (πΎβ[β¨β(π‘βπ)ββ©] βΌ ) β (πππ) = (πΎβ[β¨ββ¨π, πβ©ββ©] βΌ
))) |
122 | 114, 121 | syl5ibrcom 246 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΌ β§ π β 2o)) β ((π‘βπ) = β¨π, πβ© β (πβ(π‘βπ)) = (πΎβ[β¨β(π‘βπ)ββ©] βΌ
))) |
123 | 122 | rexlimdvva 3205 |
. . . . . . . . . . 11
β’ (π β (βπ β πΌ βπ β 2o (π‘βπ) = β¨π, πβ© β (πβ(π‘βπ)) = (πΎβ[β¨β(π‘βπ)ββ©] βΌ
))) |
124 | 123 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β (βπ β πΌ βπ β 2o (π‘βπ) = β¨π, πβ© β (πβ(π‘βπ)) = (πΎβ[β¨β(π‘βπ)ββ©] βΌ
))) |
125 | 53, 124 | mpd 15 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β (πβ(π‘βπ)) = (πΎβ[β¨β(π‘βπ)ββ©] βΌ )) |
126 | 125 | mpteq2dva 5241 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π β (0..^(β―βπ‘)) β¦ (πβ(π‘βπ))) = (π β (0..^(β―βπ‘)) β¦ (πΎβ[β¨β(π‘βπ)ββ©] βΌ
))) |
127 | 3, 7, 8, 9, 10, 11 | frgpuptf 19690 |
. . . . . . . . 9
β’ (π β π:(πΌ Γ 2o)βΆπ΅) |
128 | | fcompt 7127 |
. . . . . . . . 9
β’ ((π:(πΌ Γ 2o)βΆπ΅ β§ π‘:(0..^(β―βπ‘))βΆ(πΌ Γ 2o)) β (π β π‘) = (π β (0..^(β―βπ‘)) β¦ (πβ(π‘βπ)))) |
129 | 127, 50, 128 | syl2an2r 682 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π β π‘) = (π β (0..^(β―βπ‘)) β¦ (πβ(π‘βπ)))) |
130 | 51 | s1cld 14559 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β β¨β(π‘βπ)ββ© β Word (πΌ Γ 2o)) |
131 | 29 | ad2antrr 723 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β π = Word (πΌ Γ 2o)) |
132 | 130, 131 | eleqtrrd 2830 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β β¨β(π‘βπ)ββ© β π) |
133 | 14, 13, 12, 2 | frgpeccl 19681 |
. . . . . . . . . 10
β’
(β¨β(π‘βπ)ββ© β π β [β¨β(π‘βπ)ββ©] βΌ β π) |
134 | 132, 133 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ π β (0..^(β―βπ‘))) β [β¨β(π‘βπ)ββ©] βΌ β π) |
135 | 50 | feqmptd 6954 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β π‘ = (π β (0..^(β―βπ‘)) β¦ (π‘βπ))) |
136 | 10 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β πΌ β π) |
137 | 136, 23, 24 | sylancl 585 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β (πΌ Γ 2o) β
V) |
138 | | eqid 2726 |
. . . . . . . . . . . . 13
β’
(varFMndβ(πΌ Γ 2o)) =
(varFMndβ(πΌ Γ 2o)) |
139 | 138 | vrmdfval 18781 |
. . . . . . . . . . . 12
β’ ((πΌ Γ 2o) β V
β (varFMndβ(πΌ Γ 2o)) = (π€ β (πΌ Γ 2o) β¦
β¨βπ€ββ©)) |
140 | 137, 139 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β
(varFMndβ(πΌ Γ 2o)) = (π€ β (πΌ Γ 2o) β¦
β¨βπ€ββ©)) |
141 | | s1eq 14556 |
. . . . . . . . . . 11
β’ (π€ = (π‘βπ) β β¨βπ€ββ© = β¨β(π‘βπ)ββ©) |
142 | 51, 135, 140, 141 | fmptco 7123 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β
((varFMndβ(πΌ Γ 2o)) β π‘) = (π β (0..^(β―βπ‘)) β¦ β¨β(π‘βπ)ββ©)) |
143 | | eqidd 2727 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (π€ β π β¦ [π€] βΌ ) = (π€ β π β¦ [π€] βΌ )) |
144 | | eceq1 8743 |
. . . . . . . . . 10
β’ (π€ = β¨β(π‘βπ)ββ© β [π€] βΌ =
[β¨β(π‘βπ)ββ©] βΌ ) |
145 | 132, 142,
143, 144 | fmptco 7123 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)) = (π β (0..^(β―βπ‘)) β¦ [β¨β(π‘βπ)ββ©] βΌ )) |
146 | 1 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β πΎ β (πΊ GrpHom π»)) |
147 | 146, 4 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β πΎ:πβΆπ΅) |
148 | 147 | feqmptd 6954 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β πΎ = (π€ β π β¦ (πΎβπ€))) |
149 | | fveq2 6885 |
. . . . . . . . 9
β’ (π€ = [β¨β(π‘βπ)ββ©] βΌ β (πΎβπ€) = (πΎβ[β¨β(π‘βπ)ββ©] βΌ )) |
150 | 134, 145,
148, 149 | fmptco 7123 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πΎ β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘))) = (π β (0..^(β―βπ‘)) β¦ (πΎβ[β¨β(π‘βπ)ββ©] βΌ
))) |
151 | 126, 129,
150 | 3eqtr4d 2776 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (π β π‘) = (πΎ β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)))) |
152 | 151 | oveq2d 7421 |
. . . . . 6
β’ ((π β§ π‘ β π) β (π» Ξ£g (π β π‘)) = (π» Ξ£g (πΎ β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘))))) |
153 | 3, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15 | frgpupval 19694 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΈβ[π‘] βΌ ) = (π» Ξ£g
(π β π‘))) |
154 | | ghmmhm 19151 |
. . . . . . . 8
β’ (πΎ β (πΊ GrpHom π») β πΎ β (πΊ MndHom π»)) |
155 | 146, 154 | syl 17 |
. . . . . . 7
β’ ((π β§ π‘ β π) β πΎ β (πΊ MndHom π»)) |
156 | 138 | vrmdf 18783 |
. . . . . . . . . . 11
β’ ((πΌ Γ 2o) β V
β (varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆWord (πΌ Γ
2o)) |
157 | 137, 156 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β
(varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆWord (πΌ Γ
2o)) |
158 | 47 | feq3d 6698 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β
((varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆπ β
(varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆWord (πΌ Γ
2o))) |
159 | 157, 158 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β
(varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆπ) |
160 | | wrdco 14788 |
. . . . . . . . 9
β’ ((π‘ β Word (πΌ Γ 2o) β§
(varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆπ) β
((varFMndβ(πΌ Γ 2o)) β π‘) β Word π) |
161 | 48, 159, 160 | syl2anc 583 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β
((varFMndβ(πΌ Γ 2o)) β π‘) β Word π) |
162 | 33 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β π = (Baseβ(freeMndβ(πΌ Γ
2o)))) |
163 | 162 | mpteq1d 5236 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (π€ β π β¦ [π€] βΌ ) = (π€ β
(Baseβ(freeMndβ(πΌ Γ 2o))) β¦ [π€] βΌ )) |
164 | | eqid 2726 |
. . . . . . . . . . . . 13
β’ (π€ β
(Baseβ(freeMndβ(πΌ Γ 2o))) β¦ [π€] βΌ ) = (π€ β
(Baseβ(freeMndβ(πΌ Γ 2o))) β¦ [π€] βΌ ) |
165 | 20, 30, 14, 13, 164 | frgpmhm 19685 |
. . . . . . . . . . . 12
β’ (πΌ β π β (π€ β (Baseβ(freeMndβ(πΌ Γ 2o)))
β¦ [π€] βΌ )
β ((freeMndβ(πΌ
Γ 2o)) MndHom πΊ)) |
166 | 136, 165 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (π€ β (Baseβ(freeMndβ(πΌ Γ 2o)))
β¦ [π€] βΌ )
β ((freeMndβ(πΌ
Γ 2o)) MndHom πΊ)) |
167 | 163, 166 | eqeltrd 2827 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (π€ β π β¦ [π€] βΌ ) β
((freeMndβ(πΌ Γ
2o)) MndHom πΊ)) |
168 | 30, 2 | mhmf 18719 |
. . . . . . . . . 10
β’ ((π€ β π β¦ [π€] βΌ ) β
((freeMndβ(πΌ Γ
2o)) MndHom πΊ)
β (π€ β π β¦ [π€] βΌ
):(Baseβ(freeMndβ(πΌ Γ 2o)))βΆπ) |
169 | 167, 168 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (π€ β π β¦ [π€] βΌ
):(Baseβ(freeMndβ(πΌ Γ 2o)))βΆπ) |
170 | 162 | feq2d 6697 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((π€ β π β¦ [π€] βΌ ):πβΆπ β (π€ β π β¦ [π€] βΌ
):(Baseβ(freeMndβ(πΌ Γ 2o)))βΆπ)) |
171 | 169, 170 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π€ β π β¦ [π€] βΌ ):πβΆπ) |
172 | | wrdco 14788 |
. . . . . . . 8
β’
((((varFMndβ(πΌ Γ 2o)) β π‘) β Word π β§ (π€ β π β¦ [π€] βΌ ):πβΆπ) β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)) β Word π) |
173 | 161, 171,
172 | syl2anc 583 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)) β Word π) |
174 | 2 | gsumwmhm 18770 |
. . . . . . 7
β’ ((πΎ β (πΊ MndHom π») β§ ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)) β Word π) β (πΎβ(πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)))) = (π» Ξ£g (πΎ β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘))))) |
175 | 155, 173,
174 | syl2anc 583 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΎβ(πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)))) = (π» Ξ£g (πΎ β ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘))))) |
176 | 152, 153,
175 | 3eqtr4d 2776 |
. . . . 5
β’ ((π β§ π‘ β π) β (πΈβ[π‘] βΌ ) = (πΎβ(πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘))))) |
177 | 20, 138 | frmdgsum 18787 |
. . . . . . . . 9
β’ (((πΌ Γ 2o) β V
β§ π‘ β Word (πΌ Γ 2o)) β
((freeMndβ(πΌ Γ
2o)) Ξ£g
((varFMndβ(πΌ Γ 2o)) β π‘)) = π‘) |
178 | 25, 48, 177 | syl2an2r 682 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β ((freeMndβ(πΌ Γ 2o))
Ξ£g ((varFMndβ(πΌ Γ 2o)) β π‘)) = π‘) |
179 | 178 | fveq2d 6889 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π€ β π β¦ [π€] βΌ
)β((freeMndβ(πΌ
Γ 2o)) Ξ£g
((varFMndβ(πΌ Γ 2o)) β π‘))) = ((π€ β π β¦ [π€] βΌ )βπ‘)) |
180 | | wrdco 14788 |
. . . . . . . . . 10
β’ ((π‘ β Word (πΌ Γ 2o) β§
(varFMndβ(πΌ Γ 2o)):(πΌ Γ 2o)βΆWord (πΌ Γ 2o)) β
((varFMndβ(πΌ Γ 2o)) β π‘) β Word Word (πΌ Γ
2o)) |
181 | 48, 157, 180 | syl2anc 583 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β
((varFMndβ(πΌ Γ 2o)) β π‘) β Word Word (πΌ Γ
2o)) |
182 | 32 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (Baseβ(freeMndβ(πΌ Γ 2o))) = Word
(πΌ Γ
2o)) |
183 | | wrdeq 14492 |
. . . . . . . . . 10
β’
((Baseβ(freeMndβ(πΌ Γ 2o))) = Word (πΌ Γ 2o) β
Word (Baseβ(freeMndβ(πΌ Γ 2o))) = Word Word (πΌ Γ
2o)) |
184 | 182, 183 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β Word
(Baseβ(freeMndβ(πΌ Γ 2o))) = Word Word (πΌ Γ
2o)) |
185 | 181, 184 | eleqtrrd 2830 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β
((varFMndβ(πΌ Γ 2o)) β π‘) β Word
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
186 | 30 | gsumwmhm 18770 |
. . . . . . . 8
β’ (((π€ β π β¦ [π€] βΌ ) β
((freeMndβ(πΌ Γ
2o)) MndHom πΊ)
β§ ((varFMndβ(πΌ Γ 2o)) β π‘) β Word
(Baseβ(freeMndβ(πΌ Γ 2o)))) β ((π€ β π β¦ [π€] βΌ
)β((freeMndβ(πΌ
Γ 2o)) Ξ£g
((varFMndβ(πΌ Γ 2o)) β π‘))) = (πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)))) |
187 | 167, 185,
186 | syl2anc 583 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π€ β π β¦ [π€] βΌ
)β((freeMndβ(πΌ
Γ 2o)) Ξ£g
((varFMndβ(πΌ Γ 2o)) β π‘))) = (πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)))) |
188 | 12, 13 | efger 19638 |
. . . . . . . . 9
β’ βΌ Er
π |
189 | 188 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β βΌ Er π) |
190 | 12 | fvexi 6899 |
. . . . . . . . 9
β’ π β V |
191 | 190 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β π β V) |
192 | | eqid 2726 |
. . . . . . . 8
β’ (π€ β π β¦ [π€] βΌ ) = (π€ β π β¦ [π€] βΌ ) |
193 | 189, 191,
192 | divsfval 17502 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π€ β π β¦ [π€] βΌ )βπ‘) = [π‘] βΌ ) |
194 | 179, 187,
193 | 3eqtr3d 2774 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘))) = [π‘] βΌ ) |
195 | 194 | fveq2d 6889 |
. . . . 5
β’ ((π β§ π‘ β π) β (πΎβ(πΊ Ξ£g ((π€ β π β¦ [π€] βΌ ) β
((varFMndβ(πΌ Γ 2o)) β π‘)))) = (πΎβ[π‘] βΌ )) |
196 | 176, 195 | eqtr2d 2767 |
. . . 4
β’ ((π β§ π‘ β π) β (πΎβ[π‘] βΌ ) = (πΈβ[π‘] βΌ )) |
197 | 42, 45, 196 | ectocld 8780 |
. . 3
β’ ((π β§ π β (π / βΌ )) β (πΎβπ) = (πΈβπ)) |
198 | 41, 197 | syldan 590 |
. 2
β’ ((π β§ π β π) β (πΎβπ) = (πΈβπ)) |
199 | 6, 19, 198 | eqfnfvd 7029 |
1
β’ (π β πΎ = πΈ) |