Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
2 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) |
4 |
1 2 3
|
isrnghm |
⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
5 |
|
simprl |
⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) |
6 |
4 5
|
sylbi |
⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) |