Theorem ismhmd

Description: Deduction version of ismhm . (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	ismhmd.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	ismhmd.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
	ismhmd.p	⊢ + = ( +g ‘ 𝑆 )
	ismhmd.q	⊢ ⨣ = ( +g ‘ 𝑇 )
	ismhmd.0	⊢ 0 = ( 0g ‘ 𝑆 )
	ismhmd.z	⊢ 𝑍 = ( 0g ‘ 𝑇 )
	ismhmd.s	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
	ismhmd.t	⊢ ( 𝜑 → 𝑇 ∈ Mnd )
	ismhmd.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
	ismhmd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
	ismhmd.h	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝑍 )
Assertion	ismhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		ismhmd.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
2		ismhmd.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
3		ismhmd.p	⊢ + = ( +g ‘ 𝑆 )
4		ismhmd.q	⊢ ⨣ = ( +g ‘ 𝑇 )
5		ismhmd.0	⊢ 0 = ( 0g ‘ 𝑆 )
6		ismhmd.z	⊢ 𝑍 = ( 0g ‘ 𝑇 )
7		ismhmd.s	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
8		ismhmd.t	⊢ ( 𝜑 → 𝑇 ∈ Mnd )
9		ismhmd.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
10		ismhmd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
11		ismhmd.h	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝑍 )
12	10	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
13	9 12 11	3jca	⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑍 ) )
14	1 2 3 4 5 6	ismhm	⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑍 ) ) )
15	7 8 13 14	syl21anbrc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )