Description: Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | mhmrcl1 | ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mhm | ⊢ MndHom = ( 𝑠 ∈ Mnd , 𝑡 ∈ Mnd ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) } ) | |
2 | 1 | elmpocl1 | ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd ) |