This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑇 ) )