Step | Hyp | Ref
| Expression |
1 | | frgpup.i |
. . . 4
β’ (π β πΌ β π) |
2 | | frgpup.y |
. . . 4
β’ (π β π΄ β πΌ) |
3 | | frgpup.r |
. . . . 5
β’ βΌ = (
~FG βπΌ) |
4 | | frgpup.u |
. . . . 5
β’ π =
(varFGrpβπΌ) |
5 | 3, 4 | vrgpval 19629 |
. . . 4
β’ ((πΌ β π β§ π΄ β πΌ) β (πβπ΄) = [β¨ββ¨π΄, β
β©ββ©] βΌ
) |
6 | 1, 2, 5 | syl2anc 584 |
. . 3
β’ (π β (πβπ΄) = [β¨ββ¨π΄, β
β©ββ©] βΌ
) |
7 | 6 | fveq2d 6892 |
. 2
β’ (π β (πΈβ(πβπ΄)) = (πΈβ[β¨ββ¨π΄, β
β©ββ©] βΌ
)) |
8 | | 0ex 5306 |
. . . . . . . 8
β’ β
β V |
9 | 8 | prid1 4765 |
. . . . . . 7
β’ β
β {β
, 1o} |
10 | | df2o3 8470 |
. . . . . . 7
β’
2o = {β
, 1o} |
11 | 9, 10 | eleqtrri 2832 |
. . . . . 6
β’ β
β 2o |
12 | | opelxpi 5712 |
. . . . . 6
β’ ((π΄ β πΌ β§ β
β 2o) β
β¨π΄, β
β©
β (πΌ Γ
2o)) |
13 | 2, 11, 12 | sylancl 586 |
. . . . 5
β’ (π β β¨π΄, β
β© β (πΌ Γ 2o)) |
14 | 13 | s1cld 14549 |
. . . 4
β’ (π β β¨ββ¨π΄, β
β©ββ©
β Word (πΌ Γ
2o)) |
15 | | frgpup.w |
. . . . 5
β’ π = ( I βWord (πΌ Γ
2o)) |
16 | | 2on 8476 |
. . . . . . 7
β’
2o β On |
17 | | xpexg 7733 |
. . . . . . 7
β’ ((πΌ β π β§ 2o β On) β
(πΌ Γ 2o)
β V) |
18 | 1, 16, 17 | sylancl 586 |
. . . . . 6
β’ (π β (πΌ Γ 2o) β
V) |
19 | | wrdexg 14470 |
. . . . . 6
β’ ((πΌ Γ 2o) β V
β Word (πΌ Γ
2o) β V) |
20 | | fvi 6964 |
. . . . . 6
β’ (Word
(πΌ Γ 2o)
β V β ( I βWord (πΌ Γ 2o)) = Word (πΌ Γ
2o)) |
21 | 18, 19, 20 | 3syl 18 |
. . . . 5
β’ (π β ( I βWord (πΌ Γ 2o)) = Word
(πΌ Γ
2o)) |
22 | 15, 21 | eqtrid 2784 |
. . . 4
β’ (π β π = Word (πΌ Γ 2o)) |
23 | 14, 22 | eleqtrrd 2836 |
. . 3
β’ (π β β¨ββ¨π΄, β
β©ββ©
β π) |
24 | | frgpup.b |
. . . 4
β’ π΅ = (Baseβπ») |
25 | | frgpup.n |
. . . 4
β’ π = (invgβπ») |
26 | | frgpup.t |
. . . 4
β’ π = (π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), (πβ(πΉβπ¦)))) |
27 | | frgpup.h |
. . . 4
β’ (π β π» β Grp) |
28 | | frgpup.a |
. . . 4
β’ (π β πΉ:πΌβΆπ΅) |
29 | | frgpup.g |
. . . 4
β’ πΊ = (freeGrpβπΌ) |
30 | | frgpup.x |
. . . 4
β’ π = (BaseβπΊ) |
31 | | frgpup.e |
. . . 4
β’ πΈ = ran (π β π β¦ β¨[π] βΌ , (π» Ξ£g
(π β π))β©) |
32 | 24, 25, 26, 27, 1, 28, 15, 3, 29, 30, 31 | frgpupval 19636 |
. . 3
β’ ((π β§ β¨ββ¨π΄, β
β©ββ©
β π) β (πΈβ[β¨ββ¨π΄, β
β©ββ©]
βΌ
) = (π»
Ξ£g (π β β¨ββ¨π΄,
β
β©ββ©))) |
33 | 23, 32 | mpdan 685 |
. 2
β’ (π β (πΈβ[β¨ββ¨π΄, β
β©ββ©] βΌ ) =
(π»
Ξ£g (π β β¨ββ¨π΄,
β
β©ββ©))) |
34 | 24, 25, 26, 27, 1, 28 | frgpuptf 19632 |
. . . . . 6
β’ (π β π:(πΌ Γ 2o)βΆπ΅) |
35 | | s1co 14780 |
. . . . . 6
β’
((β¨π΄,
β
β© β (πΌ
Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β β¨ββ¨π΄, β
β©ββ©) =
β¨β(πββ¨π΄,
β
β©)ββ©) |
36 | 13, 34, 35 | syl2anc 584 |
. . . . 5
β’ (π β (π β β¨ββ¨π΄, β
β©ββ©) =
β¨β(πββ¨π΄,
β
β©)ββ©) |
37 | | df-ov 7408 |
. . . . . . 7
β’ (π΄πβ
) = (πββ¨π΄, β
β©) |
38 | | iftrue 4533 |
. . . . . . . . . 10
β’ (π§ = β
β if(π§ = β
, (πΉβπ¦), (πβ(πΉβπ¦))) = (πΉβπ¦)) |
39 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π¦ = π΄ β (πΉβπ¦) = (πΉβπ΄)) |
40 | 38, 39 | sylan9eqr 2794 |
. . . . . . . . 9
β’ ((π¦ = π΄ β§ π§ = β
) β if(π§ = β
, (πΉβπ¦), (πβ(πΉβπ¦))) = (πΉβπ΄)) |
41 | | fvex 6901 |
. . . . . . . . 9
β’ (πΉβπ΄) β V |
42 | 40, 26, 41 | ovmpoa 7559 |
. . . . . . . 8
β’ ((π΄ β πΌ β§ β
β 2o) β
(π΄πβ
) = (πΉβπ΄)) |
43 | 2, 11, 42 | sylancl 586 |
. . . . . . 7
β’ (π β (π΄πβ
) = (πΉβπ΄)) |
44 | 37, 43 | eqtr3id 2786 |
. . . . . 6
β’ (π β (πββ¨π΄, β
β©) = (πΉβπ΄)) |
45 | 44 | s1eqd 14547 |
. . . . 5
β’ (π β β¨β(πββ¨π΄, β
β©)ββ© =
β¨β(πΉβπ΄)ββ©) |
46 | 36, 45 | eqtrd 2772 |
. . . 4
β’ (π β (π β β¨ββ¨π΄, β
β©ββ©) =
β¨β(πΉβπ΄)ββ©) |
47 | 46 | oveq2d 7421 |
. . 3
β’ (π β (π» Ξ£g (π β
β¨ββ¨π΄,
β
β©ββ©)) = (π» Ξ£g
β¨β(πΉβπ΄)ββ©)) |
48 | 28, 2 | ffvelcdmd 7084 |
. . . 4
β’ (π β (πΉβπ΄) β π΅) |
49 | 24 | gsumws1 18715 |
. . . 4
β’ ((πΉβπ΄) β π΅ β (π» Ξ£g
β¨β(πΉβπ΄)ββ©) = (πΉβπ΄)) |
50 | 48, 49 | syl 17 |
. . 3
β’ (π β (π» Ξ£g
β¨β(πΉβπ΄)ββ©) = (πΉβπ΄)) |
51 | 47, 50 | eqtrd 2772 |
. 2
β’ (π β (π» Ξ£g (π β
β¨ββ¨π΄,
β
β©ββ©)) = (πΉβπ΄)) |
52 | 7, 33, 51 | 3eqtrd 2776 |
1
β’ (π β (πΈβ(πβπ΄)) = (πΉβπ΄)) |