Step | Hyp | Ref
| Expression |
1 | | 0ex 5268 |
. . . . . . . . . . . 12
β’ β
β V |
2 | | 0frgp.g |
. . . . . . . . . . . . 13
β’ πΊ =
(freeGrpββ
) |
3 | 2 | frgpgrp 19552 |
. . . . . . . . . . . 12
β’ (β
β V β πΊ β
Grp) |
4 | 1, 3 | ax-mp 5 |
. . . . . . . . . . 11
β’ πΊ β Grp |
5 | | f0 6727 |
. . . . . . . . . . 11
β’
β
:β
βΆπ΅ |
6 | | 0frgp.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΊ) |
7 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (
~FG ββ
) = ( ~FG
ββ
) |
8 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(varFGrpββ
) =
(varFGrpββ
) |
9 | 7, 8, 2, 6 | vrgpf 19558 |
. . . . . . . . . . . . . . 15
β’ (β
β V β (varFGrpββ
):β
βΆπ΅) |
10 | | ffn 6672 |
. . . . . . . . . . . . . . 15
β’
((varFGrpββ
):β
βΆπ΅ β
(varFGrpββ
) Fn β
) |
11 | 1, 9, 10 | mp2b 10 |
. . . . . . . . . . . . . 14
β’
(varFGrpββ
) Fn β
|
12 | | fn0 6636 |
. . . . . . . . . . . . . 14
β’
((varFGrpββ
) Fn β
β
(varFGrpββ
) = β
) |
13 | 11, 12 | mpbi 229 |
. . . . . . . . . . . . 13
β’
(varFGrpββ
) = β
|
14 | 13 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ β
=
(varFGrpββ
) |
15 | 2, 6, 14 | frgpup3 19568 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ β
β
V β§ β
:β
βΆπ΅) β β!π β (πΊ GrpHom πΊ)(π β β
) = β
) |
16 | 4, 1, 5, 15 | mp3an 1462 |
. . . . . . . . . 10
β’
β!π β
(πΊ GrpHom πΊ)(π β β
) = β
|
17 | | reurmo 3355 |
. . . . . . . . . 10
β’
(β!π β
(πΊ GrpHom πΊ)(π β β
) = β
β
β*π β (πΊ GrpHom πΊ)(π β β
) = β
) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
β’
β*π β
(πΊ GrpHom πΊ)(π β β
) = β
|
19 | 6 | idghm 19031 |
. . . . . . . . . . 11
β’ (πΊ β Grp β ( I βΎ
π΅) β (πΊ GrpHom πΊ)) |
20 | 4, 19 | ax-mp 5 |
. . . . . . . . . 10
β’ ( I
βΎ π΅) β (πΊ GrpHom πΊ) |
21 | | tru 1546 |
. . . . . . . . . 10
β’
β€ |
22 | 20, 21 | pm3.2i 472 |
. . . . . . . . 9
β’ (( I
βΎ π΅) β (πΊ GrpHom πΊ) β§ β€) |
23 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβπΊ) = (0gβπΊ) |
24 | 23, 6 | 0ghm 19030 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ πΊ β Grp) β (π΅ Γ
{(0gβπΊ)})
β (πΊ GrpHom πΊ)) |
25 | 4, 4, 24 | mp2an 691 |
. . . . . . . . . 10
β’ (π΅ Γ
{(0gβπΊ)})
β (πΊ GrpHom πΊ) |
26 | 25, 21 | pm3.2i 472 |
. . . . . . . . 9
β’ ((π΅ Γ
{(0gβπΊ)})
β (πΊ GrpHom πΊ) β§
β€) |
27 | | co02 6216 |
. . . . . . . . . . . 12
β’ (π β β
) =
β
|
28 | 27 | bitru 1551 |
. . . . . . . . . . 11
β’ ((π β β
) = β
β β€) |
29 | 28 | a1i 11 |
. . . . . . . . . 10
β’ (π = ( I βΎ π΅) β ((π β β
) = β
β
β€)) |
30 | 28 | a1i 11 |
. . . . . . . . . 10
β’ (π = (π΅ Γ {(0gβπΊ)}) β ((π β β
) = β
β
β€)) |
31 | 29, 30 | rmoi 3851 |
. . . . . . . . 9
β’
((β*π β
(πΊ GrpHom πΊ)(π β β
) = β
β§ (( I
βΎ π΅) β (πΊ GrpHom πΊ) β§ β€) β§ ((π΅ Γ {(0gβπΊ)}) β (πΊ GrpHom πΊ) β§ β€)) β ( I βΎ π΅) = (π΅ Γ {(0gβπΊ)})) |
32 | 18, 22, 26, 31 | mp3an 1462 |
. . . . . . . 8
β’ ( I
βΎ π΅) = (π΅ Γ
{(0gβπΊ)}) |
33 | | mptresid 6008 |
. . . . . . . 8
β’ ( I
βΎ π΅) = (π₯ β π΅ β¦ π₯) |
34 | | fconstmpt 5698 |
. . . . . . . 8
β’ (π΅ Γ
{(0gβπΊ)})
= (π₯ β π΅ β¦
(0gβπΊ)) |
35 | 32, 33, 34 | 3eqtr3i 2769 |
. . . . . . 7
β’ (π₯ β π΅ β¦ π₯) = (π₯ β π΅ β¦ (0gβπΊ)) |
36 | | mpteqb 6971 |
. . . . . . . 8
β’
(βπ₯ β
π΅ π₯ β π΅ β ((π₯ β π΅ β¦ π₯) = (π₯ β π΅ β¦ (0gβπΊ)) β βπ₯ β π΅ π₯ = (0gβπΊ))) |
37 | | id 22 |
. . . . . . . 8
β’ (π₯ β π΅ β π₯ β π΅) |
38 | 36, 37 | mprg 3067 |
. . . . . . 7
β’ ((π₯ β π΅ β¦ π₯) = (π₯ β π΅ β¦ (0gβπΊ)) β βπ₯ β π΅ π₯ = (0gβπΊ)) |
39 | 35, 38 | mpbi 229 |
. . . . . 6
β’
βπ₯ β
π΅ π₯ = (0gβπΊ) |
40 | 39 | rspec 3232 |
. . . . 5
β’ (π₯ β π΅ β π₯ = (0gβπΊ)) |
41 | | velsn 4606 |
. . . . 5
β’ (π₯ β
{(0gβπΊ)}
β π₯ =
(0gβπΊ)) |
42 | 40, 41 | sylibr 233 |
. . . 4
β’ (π₯ β π΅ β π₯ β {(0gβπΊ)}) |
43 | 42 | ssriv 3952 |
. . 3
β’ π΅ β
{(0gβπΊ)} |
44 | 6, 23 | grpidcl 18786 |
. . . . 5
β’ (πΊ β Grp β
(0gβπΊ)
β π΅) |
45 | 4, 44 | ax-mp 5 |
. . . 4
β’
(0gβπΊ) β π΅ |
46 | | snssi 4772 |
. . . 4
β’
((0gβπΊ) β π΅ β {(0gβπΊ)} β π΅) |
47 | 45, 46 | ax-mp 5 |
. . 3
β’
{(0gβπΊ)} β π΅ |
48 | 43, 47 | eqssi 3964 |
. 2
β’ π΅ = {(0gβπΊ)} |
49 | | fvex 6859 |
. . 3
β’
(0gβπΊ) β V |
50 | 49 | ensn1 8967 |
. 2
β’
{(0gβπΊ)} β 1o |
51 | 48, 50 | eqbrtri 5130 |
1
β’ π΅ β
1o |