Metamath Proof Explorer

Theorem ismhm0

Description: Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses ismhm0.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
ismhm0.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
ismhm0.p ⊢ + = ( +g ‘ 𝑆 )
ismhm0.q ⊢ ⨣ = ( +g ‘ 𝑇 )
ismhm0.z ⊢ 0 = ( 0g ‘ 𝑆 )
ismhm0.y ⊢ 𝑌 = ( 0g ‘ 𝑇 )
Assertion ismhm0 ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 ismhm0.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 ismhm0.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 ismhm0.p ⊢ + = ( +g ‘ 𝑆 )
4 ismhm0.q ⊢ ⨣ = ( +g ‘ 𝑇 )
5 ismhm0.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 ismhm0.y ⊢ 𝑌 = ( 0g ‘ 𝑇 )
7 1 2 3 4 5 6 ismhm ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
8 df-3an ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ↔ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) )
9 mndmgm ⊢ ( 𝑆 ∈ Mnd → 𝑆 ∈ Mgm )
10 mndmgm ⊢ ( 𝑇 ∈ Mnd → 𝑇 ∈ Mgm )
11 9 10 anim12i ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
12 11 biantrurd ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
13 1 2 3 4 ismgmhm ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) )
14 12 13 bitr4di ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ↔ 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) )
15 14 anbi1d ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
16 8 15 syl5bb ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
17 16 pm5.32i ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
18 7 17 bitri ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )