Step |
Hyp |
Ref |
Expression |
1 |
|
isghmd.x |
âĒ ð = ( Base â ð ) |
2 |
|
isghmd.y |
âĒ ð = ( Base â ð ) |
3 |
|
isghmd.a |
âĒ + = ( +g â ð ) |
4 |
|
isghmd.b |
âĒ âĻĢ = ( +g â ð ) |
5 |
|
isghmd.s |
âĒ ( ð â ð â Grp ) |
6 |
|
isghmd.t |
âĒ ( ð â ð â Grp ) |
7 |
|
isghmd.f |
âĒ ( ð â ðđ : ð âķ ð ) |
8 |
|
isghmd.l |
âĒ ( ( ð â§ ( ðĨ â ð â§ ðĶ â ð ) ) â ( ðđ â ( ðĨ + ðĶ ) ) = ( ( ðđ â ðĨ ) âĻĢ ( ðđ â ðĶ ) ) ) |
9 |
8
|
ralrimivva |
âĒ ( ð â â ðĨ â ð â ðĶ â ð ( ðđ â ( ðĨ + ðĶ ) ) = ( ( ðđ â ðĨ ) âĻĢ ( ðđ â ðĶ ) ) ) |
10 |
7 9
|
jca |
âĒ ( ð â ( ðđ : ð âķ ð â§ â ðĨ â ð â ðĶ â ð ( ðđ â ( ðĨ + ðĶ ) ) = ( ( ðđ â ðĨ ) âĻĢ ( ðđ â ðĶ ) ) ) ) |
11 |
1 2 3 4
|
isghm |
âĒ ( ðđ â ( ð GrpHom ð ) â ( ( ð â Grp â§ ð â Grp ) â§ ( ðđ : ð âķ ð â§ â ðĨ â ð â ðĶ â ð ( ðđ â ( ðĨ + ðĶ ) ) = ( ( ðđ â ðĨ ) âĻĢ ( ðđ â ðĶ ) ) ) ) ) |
12 |
5 6 10 11
|
syl21anbrc |
âĒ ( ð â ðđ â ( ð GrpHom ð ) ) |