Step |
Hyp |
Ref |
Expression |
1 |
|
idrnghm.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
id |
⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Rng ) |
3 |
2 2
|
jca |
⊢ ( 𝑅 ∈ Rng → ( 𝑅 ∈ Rng ∧ 𝑅 ∈ Rng ) ) |
4 |
|
rngabl |
⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel ) |
5 |
|
ablgrp |
⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ Grp ) |
6 |
1
|
idghm |
⊢ ( 𝑅 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝑅 GrpHom 𝑅 ) ) |
7 |
4 5 6
|
3syl |
⊢ ( 𝑅 ∈ Rng → ( I ↾ 𝐵 ) ∈ ( 𝑅 GrpHom 𝑅 ) ) |
8 |
|
eqid |
⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) |
9 |
8
|
rngmgp |
⊢ ( 𝑅 ∈ Rng → ( mulGrp ‘ 𝑅 ) ∈ Smgrp ) |
10 |
|
sgrpmgm |
⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Smgrp → ( mulGrp ‘ 𝑅 ) ∈ Mgm ) |
11 |
8 1
|
mgpbas |
⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) |
12 |
11
|
idmgmhm |
⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mgm → ( I ↾ 𝐵 ) ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) |
13 |
9 10 12
|
3syl |
⊢ ( 𝑅 ∈ Rng → ( I ↾ 𝐵 ) ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) |
14 |
7 13
|
jca |
⊢ ( 𝑅 ∈ Rng → ( ( I ↾ 𝐵 ) ∈ ( 𝑅 GrpHom 𝑅 ) ∧ ( I ↾ 𝐵 ) ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) ) |
15 |
8 8
|
isrnghmmul |
⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝑅 RngHomo 𝑅 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑅 ∈ Rng ) ∧ ( ( I ↾ 𝐵 ) ∈ ( 𝑅 GrpHom 𝑅 ) ∧ ( I ↾ 𝐵 ) ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) ) ) |
16 |
3 14 15
|
sylanbrc |
⊢ ( 𝑅 ∈ Rng → ( I ↾ 𝐵 ) ∈ ( 𝑅 RngHomo 𝑅 ) ) |