Metamath Proof Explorer

Theorem c0snmgmhm

Description: The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
zrrhm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
zrrhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
Assertion c0snmgmhm ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) )

Proof

Step Hyp Ref Expression
1 zrrhm.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
2 zrrhm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
3 zrrhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 mndmgm ⊢ ( 𝑆 ∈ Mnd → 𝑆 ∈ Mgm )
5 4 anim1i ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
6 5 3adant3 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
7 6 ancomd ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑇 ∈ Mgm ∧ 𝑆 ∈ Mgm ) )
8 1 fvexi ⊢ 𝐵 ∈ V
9 hash1snb ⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 1 ↔ ∃ 𝑏 𝐵 = { 𝑏 } ) )
10 8 9 ax-mp ⊢ ( ( ♯ ‘ 𝐵 ) = 1 ↔ ∃ 𝑏 𝐵 = { 𝑏 } )
11 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
12 11 2 mndidcl ⊢ ( 𝑆 ∈ Mnd → 0 ∈ ( Base ‘ 𝑆 ) )
13 12 adantr ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → 0 ∈ ( Base ‘ 𝑆 ) )
14 13 adantr ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 0 ∈ ( Base ‘ 𝑆 ) )
15 14 adantr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑥 ∈ 𝐵 ) → 0 ∈ ( Base ‘ 𝑆 ) )
16 15 3 fmptd ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
17 3 a1i ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 ) )
18 eqidd ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑥 = 𝑏 ) → 0 = 0 )
19 vsnid ⊢ 𝑏 ∈ { 𝑏 }
20 19 a1i ⊢ ( 𝐵 = { 𝑏 } → 𝑏 ∈ { 𝑏 } )
21 eleq2 ⊢ ( 𝐵 = { 𝑏 } → ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ { 𝑏 } ) )
22 20 21 mpbird ⊢ ( 𝐵 = { 𝑏 } → 𝑏 ∈ 𝐵 )
23 22 adantl ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝑏 ∈ 𝐵 )
24 17 18 23 14 fvmptd ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 ‘ 𝑏 ) = 0 )
25 simpr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 𝐻 ‘ 𝑏 ) = 0 )
26 25 25 oveq12d ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) = ( 0 ( +g ‘ 𝑆 ) 0 ) )
27 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
28 11 27 2 mndlid ⊢ ( ( 𝑆 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑆 ) ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 )
29 12 28 mpdan ⊢ ( 𝑆 ∈ Mnd → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 )
30 29 adantr ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 )
31 30 adantr ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 )
32 31 adantr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 )
33 simpr ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → 𝑇 ∈ Mgm )
34 33 adantr ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝑇 ∈ Mgm )
35 34 adantr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → 𝑇 ∈ Mgm )
36 simpr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
37 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
38 1 37 mgmcl ⊢ ( ( 𝑇 ∈ Mgm ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 )
39 35 36 36 38 syl3anc ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 )
40 eleq2 ⊢ ( 𝐵 = { 𝑏 } → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 ↔ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ { 𝑏 } ) )
41 elsni ⊢ ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ { 𝑏 } → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 )
42 40 41 biimtrdi ⊢ ( 𝐵 = { 𝑏 } → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) )
43 42 adantl ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) )
44 43 adantr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) )
45 39 44 mpd ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 )
46 23 45 mpdan ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 )
47 46 fveq2d ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( 𝐻 ‘ 𝑏 ) )
48 47 adantr ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( 𝐻 ‘ 𝑏 ) )
49 48 25 eqtr2d ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → 0 = ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) )
50 26 32 49 3eqtrrd ⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
51 24 50 mpdan ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
52 id ⊢ ( 𝐵 = { 𝑏 } → 𝐵 = { 𝑏 } )
53 52 raleqdv ⊢ ( 𝐵 = { 𝑏 } → ( ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) )
54 52 53 raleqbidv ⊢ ( 𝐵 = { 𝑏 } → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) )
55 54 adantl ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) )
56 fvoveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) )
57 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) )
58 57 oveq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) )
59 56 58 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) )
60 oveq2 ⊢ ( 𝑐 = 𝑏 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) = ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) )
61 60 fveq2d ⊢ ( 𝑐 = 𝑏 → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) )
62 fveq2 ⊢ ( 𝑐 = 𝑏 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑏 ) )
63 62 oveq2d ⊢ ( 𝑐 = 𝑏 → ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
64 61 63 eqeq12d ⊢ ( 𝑐 = 𝑏 → ( ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) )
65 59 64 2ralsng ⊢ ( ( 𝑏 ∈ V ∧ 𝑏 ∈ V ) → ( ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) )
66 65 el2v ⊢ ( ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
67 55 66 bitrdi ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) )
68 51 67 mpbird ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) )
69 16 68 jca ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) )
70 69 ex ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( 𝐵 = { 𝑏 } → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) )
71 70 exlimdv ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( ∃ 𝑏 𝐵 = { 𝑏 } → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) )
72 10 71 biimtrid ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( ( ♯ ‘ 𝐵 ) = 1 → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) )
73 72 3impia ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) )
74 1 11 37 27 ismgmhm ⊢ ( 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) ↔ ( ( 𝑇 ∈ Mgm ∧ 𝑆 ∈ Mgm ) ∧ ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) )
75 7 73 74 sylanbrc ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) )