| Step | Hyp | Ref
| Expression |
|---|
| 1 | | 0ex 5298 |
. . . . . . . . . . . 12
β’ β
β V |
| 2 | | 0frgp.g |
. . . . . . . . . . . . 13
β’ πΊ =
(freeGrpββ
) |
| 3 | 2 | frgpgrp 19678 |
. . . . . . . . . . . 12
β’ (β
β V β πΊ β
Grp) |
| 4 | 1, 3 | ax-mp 5 |
. . . . . . . . . . 11
β’ πΊ β Grp |
| 5 | | f0 6763 |
. . . . . . . . . . 11
β’
β
:β
βΆπ΅ |
| 6 | | 0frgp.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΊ) |
| 7 | | eqid 2724 |
. . . . . . . . . . . . . . . 16
β’ (
~FG ββ
) = ( ~FG
ββ
) |
| 8 | | eqid 2724 |
. . . . . . . . . . . . . . . 16
β’
(varFGrpββ
) =
(varFGrpββ
) |
| 9 | 7, 8, 2, 6 | vrgpf 19684 |
. . . . . . . . . . . . . . 15
β’ (β
β V β (varFGrpββ
):β
βΆπ΅) |
| 10 | | ffn 6708 |
. . . . . . . . . . . . . . 15
β’
((varFGrpββ
):β
βΆπ΅ β
(varFGrpββ
) Fn β
) |
| 11 | 1, 9, 10 | mp2b 10 |
. . . . . . . . . . . . . 14
β’
(varFGrpββ
) Fn β
|
| 12 | | fn0 6672 |
. . . . . . . . . . . . . 14
β’
((varFGrpββ
) Fn β
β
(varFGrpββ
) = β
) |
| 13 | 11, 12 | mpbi 229 |
. . . . . . . . . . . . 13
β’
(varFGrpββ
) = β
|
| 14 | 13 | eqcomi 2733 |
. . . . . . . . . . . 12
β’ β
=
(varFGrpββ
) |
| 15 | 2, 6, 14 | frgpup3 19694 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ β
β
V β§ β
:β
βΆπ΅) β β!π β (πΊ GrpHom πΊ)(π β β
) = β
) |
| 16 | 4, 1, 5, 15 | mp3an 1457 |
. . . . . . . . . 10
β’
β!π β
(πΊ GrpHom πΊ)(π β β
) = β
|
| 17 | | reurmo 3371 |
. . . . . . . . . 10
β’
(β!π β
(πΊ GrpHom πΊ)(π β β
) = β
β
β*π β (πΊ GrpHom πΊ)(π β β
) = β
) |
| 18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
β’
β*π β
(πΊ GrpHom πΊ)(π β β
) = β
|
| 19 | 6 | idghm 19152 |
. . . . . . . . . . 11
β’ (πΊ β Grp β ( I βΎ
π΅) β (πΊ GrpHom πΊ)) |
| 20 | 4, 19 | ax-mp 5 |
. . . . . . . . . 10
β’ ( I
βΎ π΅) β (πΊ GrpHom πΊ) |
| 21 | | tru 1537 |
. . . . . . . . . 10
β’
β€ |
| 22 | 20, 21 | pm3.2i 470 |
. . . . . . . . 9
β’ (( I
βΎ π΅) β (πΊ GrpHom πΊ) β§ β€) |
| 23 | | eqid 2724 |
. . . . . . . . . . . 12
β’
(0gβπΊ) = (0gβπΊ) |
| 24 | 23, 6 | 0ghm 19151 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ πΊ β Grp) β (π΅ Γ
{(0gβπΊ)})
β (πΊ GrpHom πΊ)) |
| 25 | 4, 4, 24 | mp2an 689 |
. . . . . . . . . 10
β’ (π΅ Γ
{(0gβπΊ)})
β (πΊ GrpHom πΊ) |
| 26 | 25, 21 | pm3.2i 470 |
. . . . . . . . 9
β’ ((π΅ Γ
{(0gβπΊ)})
β (πΊ GrpHom πΊ) β§
β€) |
| 27 | | co02 6250 |
. . . . . . . . . . . 12
β’ (π β β
) =
β
|
| 28 | 27 | bitru 1542 |
. . . . . . . . . . 11
β’ ((π β β
) = β
β β€) |
| 29 | 28 | a1i 11 |
. . . . . . . . . 10
β’ (π = ( I βΎ π΅) β ((π β β
) = β
β
β€)) |
| 30 | 28 | a1i 11 |
. . . . . . . . . 10
β’ (π = (π΅ Γ {(0gβπΊ)}) β ((π β β
) = β
β
β€)) |
| 31 | 29, 30 | rmoi 3878 |
. . . . . . . . 9
β’
((β*π β
(πΊ GrpHom πΊ)(π β β
) = β
β§ (( I
βΎ π΅) β (πΊ GrpHom πΊ) β§ β€) β§ ((π΅ Γ {(0gβπΊ)}) β (πΊ GrpHom πΊ) β§ β€)) β ( I βΎ π΅) = (π΅ Γ {(0gβπΊ)})) |
| 32 | 18, 22, 26, 31 | mp3an 1457 |
. . . . . . . 8
β’ ( I
βΎ π΅) = (π΅ Γ
{(0gβπΊ)}) |
| 33 | | mptresid 6041 |
. . . . . . . 8
β’ ( I
βΎ π΅) = (π₯ β π΅ β¦ π₯) |
| 34 | | fconstmpt 5729 |
. . . . . . . 8
β’ (π΅ Γ
{(0gβπΊ)})
= (π₯ β π΅ β¦
(0gβπΊ)) |
| 35 | 32, 33, 34 | 3eqtr3i 2760 |
. . . . . . 7
β’ (π₯ β π΅ β¦ π₯) = (π₯ β π΅ β¦ (0gβπΊ)) |
| 36 | | mpteqb 7008 |
. . . . . . . 8
β’
(βπ₯ β
π΅ π₯ β π΅ β ((π₯ β π΅ β¦ π₯) = (π₯ β π΅ β¦ (0gβπΊ)) β βπ₯ β π΅ π₯ = (0gβπΊ))) |
| 37 | | id 22 |
. . . . . . . 8
β’ (π₯ β π΅ β π₯ β π΅) |
| 38 | 36, 37 | mprg 3059 |
. . . . . . 7
β’ ((π₯ β π΅ β¦ π₯) = (π₯ β π΅ β¦ (0gβπΊ)) β βπ₯ β π΅ π₯ = (0gβπΊ)) |
| 39 | 35, 38 | mpbi 229 |
. . . . . 6
β’
βπ₯ β
π΅ π₯ = (0gβπΊ) |
| 40 | 39 | rspec 3239 |
. . . . 5
β’ (π₯ β π΅ β π₯ = (0gβπΊ)) |
| 41 | | velsn 4637 |
. . . . 5
β’ (π₯ β
{(0gβπΊ)}
β π₯ =
(0gβπΊ)) |
| 42 | 40, 41 | sylibr 233 |
. . . 4
β’ (π₯ β π΅ β π₯ β {(0gβπΊ)}) |
| 43 | 42 | ssriv 3979 |
. . 3
β’ π΅ β
{(0gβπΊ)} |
| 44 | 6, 23 | grpidcl 18891 |
. . . . 5
β’ (πΊ β Grp β
(0gβπΊ)
β π΅) |
| 45 | 4, 44 | ax-mp 5 |
. . . 4
β’
(0gβπΊ) β π΅ |
| 46 | | snssi 4804 |
. . . 4
β’
((0gβπΊ) β π΅ β {(0gβπΊ)} β π΅) |
| 47 | 45, 46 | ax-mp 5 |
. . 3
β’
{(0gβπΊ)} β π΅ |
| 48 | 43, 47 | eqssi 3991 |
. 2
β’ π΅ = {(0gβπΊ)} |
| 49 | | fvex 6895 |
. . 3
β’
(0gβπΊ) β V |
| 50 | 49 | ensn1 9014 |
. 2
β’
{(0gβπΊ)} β 1o |
| 51 | 48, 50 | eqbrtri 5160 |
1
β’ π΅ β
1o |
