Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Mnd) |
2 | 1 | ancri 547 |
. 2
⊢ (𝑀 ∈ Mnd → (𝑀 ∈ Mnd ∧ 𝑀 ∈ Mnd)) |
3 | | f1oi 6415 |
. . . 4
⊢ ( I
↾ 𝐵):𝐵–1-1-onto→𝐵 |
4 | | f1of 6378 |
. . . 4
⊢ (( I
↾ 𝐵):𝐵–1-1-onto→𝐵 → ( I ↾ 𝐵):𝐵⟶𝐵) |
5 | 3, 4 | mp1i 13 |
. . 3
⊢ (𝑀 ∈ Mnd → ( I ↾
𝐵):𝐵⟶𝐵) |
6 | | idmhm.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) |
7 | | eqid 2825 |
. . . . . . . 8
⊢
(+g‘𝑀) = (+g‘𝑀) |
8 | 6, 7 | mndcl 17654 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) |
9 | 8 | 3expb 1155 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) |
10 | | fvresi 6691 |
. . . . . 6
⊢ ((𝑎(+g‘𝑀)𝑏) ∈ 𝐵 → (( I ↾ 𝐵)‘(𝑎(+g‘𝑀)𝑏)) = (𝑎(+g‘𝑀)𝑏)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ 𝐵)‘(𝑎(+g‘𝑀)𝑏)) = (𝑎(+g‘𝑀)𝑏)) |
12 | | fvresi 6691 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑎) = 𝑎) |
13 | | fvresi 6691 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑏) = 𝑏) |
14 | 12, 13 | oveqan12d 6924 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ((( I ↾ 𝐵)‘𝑎)(+g‘𝑀)(( I ↾ 𝐵)‘𝑏)) = (𝑎(+g‘𝑀)𝑏)) |
15 | 14 | adantl 475 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((( I ↾ 𝐵)‘𝑎)(+g‘𝑀)(( I ↾ 𝐵)‘𝑏)) = (𝑎(+g‘𝑀)𝑏)) |
16 | 11, 15 | eqtr4d 2864 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ 𝐵)‘(𝑎(+g‘𝑀)𝑏)) = ((( I ↾ 𝐵)‘𝑎)(+g‘𝑀)(( I ↾ 𝐵)‘𝑏))) |
17 | 16 | ralrimivva 3180 |
. . 3
⊢ (𝑀 ∈ Mnd → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( I ↾ 𝐵)‘(𝑎(+g‘𝑀)𝑏)) = ((( I ↾ 𝐵)‘𝑎)(+g‘𝑀)(( I ↾ 𝐵)‘𝑏))) |
18 | | eqid 2825 |
. . . . 5
⊢
(0g‘𝑀) = (0g‘𝑀) |
19 | 6, 18 | mndidcl 17661 |
. . . 4
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ 𝐵) |
20 | | fvresi 6691 |
. . . 4
⊢
((0g‘𝑀) ∈ 𝐵 → (( I ↾ 𝐵)‘(0g‘𝑀)) = (0g‘𝑀)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (𝑀 ∈ Mnd → (( I ↾
𝐵)‘(0g‘𝑀)) = (0g‘𝑀)) |
22 | 5, 17, 21 | 3jca 1164 |
. 2
⊢ (𝑀 ∈ Mnd → (( I ↾
𝐵):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( I ↾ 𝐵)‘(𝑎(+g‘𝑀)𝑏)) = ((( I ↾ 𝐵)‘𝑎)(+g‘𝑀)(( I ↾ 𝐵)‘𝑏)) ∧ (( I ↾ 𝐵)‘(0g‘𝑀)) = (0g‘𝑀))) |
23 | 6, 6, 7, 7, 18, 18 | ismhm 17690 |
. 2
⊢ (( I
↾ 𝐵) ∈ (𝑀 MndHom 𝑀) ↔ ((𝑀 ∈ Mnd ∧ 𝑀 ∈ Mnd) ∧ (( I ↾ 𝐵):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( I ↾ 𝐵)‘(𝑎(+g‘𝑀)𝑏)) = ((( I ↾ 𝐵)‘𝑎)(+g‘𝑀)(( I ↾ 𝐵)‘𝑏)) ∧ (( I ↾ 𝐵)‘(0g‘𝑀)) = (0g‘𝑀)))) |
24 | 2, 22, 23 | sylanbrc 580 |
1
⊢ (𝑀 ∈ Mnd → ( I ↾
𝐵) ∈ (𝑀 MndHom 𝑀)) |