| Step |
Hyp |
Ref |
Expression |
| 1 |
|
idghm.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
| 2 |
|
id |
⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp ) |
| 3 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
| 4 |
1 3
|
grpcl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐵 ) |
| 5 |
4
|
3expb |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐵 ) |
| 6 |
|
fvresi |
⊢ ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) |
| 7 |
5 6
|
syl |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) |
| 8 |
|
fvresi |
⊢ ( 𝑎 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑎 ) = 𝑎 ) |
| 9 |
|
fvresi |
⊢ ( 𝑏 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑏 ) = 𝑏 ) |
| 10 |
8 9
|
oveqan12d |
⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) |
| 11 |
10
|
adantl |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) |
| 12 |
7 11
|
eqtr4d |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) |
| 13 |
12
|
ralrimivva |
⊢ ( 𝐺 ∈ Grp → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) |
| 14 |
|
f1oi |
⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 |
| 15 |
|
f1of |
⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ) |
| 16 |
14 15
|
ax-mp |
⊢ ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 |
| 17 |
13 16
|
jctil |
⊢ ( 𝐺 ∈ Grp → ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) ) |
| 18 |
1 1 3 3
|
isghm |
⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ Grp ) ∧ ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) ) ) |
| 19 |
2 2 17 18
|
syl21anbrc |
⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) ) |