This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Property of a group homomorphism, similar to ismhm . (Contributed by Mario Carneiro, 7-Mar-2015)
|
|
Ref |
Expression |
|
Hypotheses |
isghm.w |
⊢ 𝑋 = ( Base ‘ 𝑆 ) |
|
|
isghm.x |
⊢ 𝑌 = ( Base ‘ 𝑇 ) |
|
|
isghm.a |
⊢ + = ( +g ‘ 𝑆 ) |
|
|
isghm.b |
⊢ ⨣ = ( +g ‘ 𝑇 ) |
|
Assertion |
isghm3 |
⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isghm.w |
⊢ 𝑋 = ( Base ‘ 𝑆 ) |
| 2 |
|
isghm.x |
⊢ 𝑌 = ( Base ‘ 𝑇 ) |
| 3 |
|
isghm.a |
⊢ + = ( +g ‘ 𝑆 ) |
| 4 |
|
isghm.b |
⊢ ⨣ = ( +g ‘ 𝑇 ) |
| 5 |
1 2 3 4
|
isghm |
⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) ) |
| 6 |
5
|
baib |
⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) ) |