| Step |
Hyp |
Ref |
Expression |
| 1 |
|
idmgmhm.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
| 2 |
|
id |
⊢ ( 𝑀 ∈ Mgm → 𝑀 ∈ Mgm ) |
| 3 |
2
|
ancri |
⊢ ( 𝑀 ∈ Mgm → ( 𝑀 ∈ Mgm ∧ 𝑀 ∈ Mgm ) ) |
| 4 |
|
f1oi |
⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 |
| 5 |
|
f1of |
⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ) |
| 6 |
4 5
|
mp1i |
⊢ ( 𝑀 ∈ Mgm → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ) |
| 7 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
| 8 |
1 7
|
mgmcl |
⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) |
| 9 |
8
|
3expb |
⊢ ( ( 𝑀 ∈ Mgm ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) |
| 10 |
|
fvresi |
⊢ ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) |
| 11 |
9 10
|
syl |
⊢ ( ( 𝑀 ∈ Mgm ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) |
| 12 |
|
fvresi |
⊢ ( 𝑎 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑎 ) = 𝑎 ) |
| 13 |
|
fvresi |
⊢ ( 𝑏 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑏 ) = 𝑏 ) |
| 14 |
12 13
|
oveqan12d |
⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) |
| 15 |
14
|
adantl |
⊢ ( ( 𝑀 ∈ Mgm ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) |
| 16 |
11 15
|
eqtr4d |
⊢ ( ( 𝑀 ∈ Mgm ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) |
| 17 |
16
|
ralrimivva |
⊢ ( 𝑀 ∈ Mgm → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) |
| 18 |
6 17
|
jca |
⊢ ( 𝑀 ∈ Mgm → ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) ) |
| 19 |
1 1 7 7
|
ismgmhm |
⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝑀 MgmHom 𝑀 ) ↔ ( ( 𝑀 ∈ Mgm ∧ 𝑀 ∈ Mgm ) ∧ ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) ) ) |
| 20 |
3 18 19
|
sylanbrc |
⊢ ( 𝑀 ∈ Mgm → ( I ↾ 𝐵 ) ∈ ( 𝑀 MgmHom 𝑀 ) ) |