Step | Hyp | Ref
| Expression |
1 | | frgpup3.b |
. . 3
β’ π΅ = (Baseβπ») |
2 | | eqid 2732 |
. . 3
β’
(invgβπ») = (invgβπ») |
3 | | eqid 2732 |
. . 3
β’ (π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) = (π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) |
4 | | simp1 1136 |
. . 3
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β π» β Grp) |
5 | | simp2 1137 |
. . 3
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΌ β π) |
6 | | simp3 1138 |
. . 3
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΉ:πΌβΆπ΅) |
7 | | eqid 2732 |
. . 3
β’ ( I
βWord (πΌ Γ
2o)) = ( I βWord (πΌ Γ 2o)) |
8 | | eqid 2732 |
. . 3
β’ (
~FG βπΌ) = ( ~FG βπΌ) |
9 | | frgpup3.g |
. . 3
β’ πΊ = (freeGrpβπΌ) |
10 | | eqid 2732 |
. . 3
β’
(BaseβπΊ) =
(BaseβπΊ) |
11 | | eqid 2732 |
. . 3
β’ ran
(π β ( I βWord
(πΌ Γ 2o))
β¦ β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | frgpup1 19637 |
. 2
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β (πΊ GrpHom π»)) |
13 | 4 | adantr 481 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β π» β Grp) |
14 | 5 | adantr 481 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β πΌ β π) |
15 | 6 | adantr 481 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β πΉ:πΌβΆπ΅) |
16 | | frgpup3.u |
. . . . 5
β’ π =
(varFGrpβπΌ) |
17 | | simpr 485 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β π β πΌ) |
18 | 1, 2, 3, 13, 14, 15, 7, 8, 9,
10, 11, 16, 17 | frgpup2 19638 |
. . . 4
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©)β(πβπ)) = (πΉβπ)) |
19 | 18 | mpteq2dva 5247 |
. . 3
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (π β πΌ β¦ (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©)β(πβπ))) = (π β πΌ β¦ (πΉβπ))) |
20 | 10, 1 | ghmf 19090 |
. . . . 5
β’ (ran
(π β ( I βWord
(πΌ Γ 2o))
β¦ β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β (πΊ GrpHom π») β ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©):(BaseβπΊ)βΆπ΅) |
21 | 12, 20 | syl 17 |
. . . 4
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©):(BaseβπΊ)βΆπ΅) |
22 | 8, 16, 9, 10 | vrgpf 19630 |
. . . . 5
β’ (πΌ β π β π:πΌβΆ(BaseβπΊ)) |
23 | 5, 22 | syl 17 |
. . . 4
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β π:πΌβΆ(BaseβπΊ)) |
24 | | fcompt 7127 |
. . . 4
β’ ((ran
(π β ( I βWord
(πΌ Γ 2o))
β¦ β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©):(BaseβπΊ)βΆπ΅ β§ π:πΌβΆ(BaseβπΊ)) β (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β π) = (π β πΌ β¦ (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©)β(πβπ)))) |
25 | 21, 23, 24 | syl2anc 584 |
. . 3
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β π) = (π β πΌ β¦ (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©)β(πβπ)))) |
26 | 6 | feqmptd 6957 |
. . 3
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΉ = (π β πΌ β¦ (πΉβπ))) |
27 | 19, 25, 26 | 3eqtr4d 2782 |
. 2
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β π) = πΉ) |
28 | 4 | adantr 481 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ (π β (πΊ GrpHom π») β§ (π β π) = πΉ)) β π» β Grp) |
29 | 5 | adantr 481 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ (π β (πΊ GrpHom π») β§ (π β π) = πΉ)) β πΌ β π) |
30 | 6 | adantr 481 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ (π β (πΊ GrpHom π») β§ (π β π) = πΉ)) β πΉ:πΌβΆπ΅) |
31 | | simprl 769 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ (π β (πΊ GrpHom π») β§ (π β π) = πΉ)) β π β (πΊ GrpHom π»)) |
32 | | simprr 771 |
. . . . 5
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ (π β (πΊ GrpHom π») β§ (π β π) = πΉ)) β (π β π) = πΉ) |
33 | 1, 2, 3, 28, 29, 30, 7, 8, 9,
10, 11, 16, 31, 32 | frgpup3lem 19639 |
. . . 4
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ (π β (πΊ GrpHom π») β§ (π β π) = πΉ)) β π = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©)) |
34 | 33 | expr 457 |
. . 3
β’ (((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β (πΊ GrpHom π»)) β ((π β π) = πΉ β π = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©))) |
35 | 34 | ralrimiva 3146 |
. 2
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β βπ β (πΊ GrpHom π»)((π β π) = πΉ β π = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©))) |
36 | | coeq1 5855 |
. . . 4
β’ (π = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β (π β π) = (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β π)) |
37 | 36 | eqeq1d 2734 |
. . 3
β’ (π = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β ((π β π) = πΉ β (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β π) = πΉ)) |
38 | 37 | eqreu 3724 |
. 2
β’ ((ran
(π β ( I βWord
(πΌ Γ 2o))
β¦ β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β (πΊ GrpHom π») β§ (ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©) β π) = πΉ β§ βπ β (πΊ GrpHom π»)((π β π) = πΉ β π = ran (π β ( I βWord (πΌ Γ 2o)) β¦
β¨[π](
~FG βπΌ), (π» Ξ£g ((π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), ((invgβπ»)β(πΉβπ¦)))) β π))β©))) β β!π β (πΊ GrpHom π»)(π β π) = πΉ) |
39 | 12, 27, 35, 38 | syl3anc 1371 |
1
β’ ((π» β Grp β§ πΌ β π β§ πΉ:πΌβΆπ΅) β β!π β (πΊ GrpHom π»)(π β π) = πΉ) |