Metamath Proof Explorer


Theorem resmgmhm

Description: Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis resmgmhm.u 𝑈 = ( 𝑆s 𝑋 )
Assertion resmgmhm ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 resmgmhm.u 𝑈 = ( 𝑆s 𝑋 )
2 mgmhmrcl ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
3 2 simprd ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝑇 ∈ Mgm )
4 1 submgmmgm ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → 𝑈 ∈ Mgm )
5 3 4 anim12ci ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝑈 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
6 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
8 6 7 mgmhmf ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
9 6 submgmss ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
10 fssres ( ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) )
11 8 9 10 syl2an ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) )
12 9 adantl ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
13 1 6 ressbas2 ( 𝑋 ⊆ ( Base ‘ 𝑆 ) → 𝑋 = ( Base ‘ 𝑈 ) )
14 12 13 syl ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → 𝑋 = ( Base ‘ 𝑈 ) )
15 14 feq2d ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( 𝐹𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) ↔ ( 𝐹𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ) )
16 11 15 mpbid ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) )
17 simpll ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )
18 9 ad2antlr ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
19 simprl ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑥𝑋 )
20 18 19 sseldd ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
21 simprr ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑦𝑋 )
22 18 21 sseldd ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
23 eqid ( +g𝑆 ) = ( +g𝑆 )
24 eqid ( +g𝑇 ) = ( +g𝑇 )
25 6 23 24 mgmhmlin ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
26 17 20 22 25 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
27 23 submgmcl ( ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ∧ 𝑥𝑋𝑦𝑋 ) → ( 𝑥 ( +g𝑆 ) 𝑦 ) ∈ 𝑋 )
28 27 3expb ( ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 ( +g𝑆 ) 𝑦 ) ∈ 𝑋 )
29 28 adantll ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 ( +g𝑆 ) 𝑦 ) ∈ 𝑋 )
30 fvres ( ( 𝑥 ( +g𝑆 ) 𝑦 ) ∈ 𝑋 → ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) )
31 29 30 syl ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) )
32 fvres ( 𝑥𝑋 → ( ( 𝐹𝑋 ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
33 fvres ( 𝑦𝑋 → ( ( 𝐹𝑋 ) ‘ 𝑦 ) = ( 𝐹𝑦 ) )
34 32 33 oveqan12d ( ( 𝑥𝑋𝑦𝑋 ) → ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
35 34 adantl ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
36 26 31 35 3eqtr4d ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) )
37 36 ralrimivva ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ∀ 𝑥𝑋𝑦𝑋 ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) )
38 1 23 ressplusg ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → ( +g𝑆 ) = ( +g𝑈 ) )
39 38 adantl ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( +g𝑆 ) = ( +g𝑈 ) )
40 39 oveqd ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝑥 ( +g𝑆 ) 𝑦 ) = ( 𝑥 ( +g𝑈 ) 𝑦 ) )
41 40 fveqeq2d ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ↔ ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑈 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ) )
42 14 41 raleqbidv ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ∀ 𝑦𝑋 ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑈 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ) )
43 14 42 raleqbidv ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ∀ 𝑥𝑋𝑦𝑋 ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑈 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ) )
44 37 43 mpbid ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑈 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) )
45 16 44 jca ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( 𝐹𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑈 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ) )
46 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
47 eqid ( +g𝑈 ) = ( +g𝑈 )
48 46 7 47 24 ismgmhm ( ( 𝐹𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) ↔ ( ( 𝑈 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( ( 𝐹𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹𝑋 ) ‘ ( 𝑥 ( +g𝑈 ) 𝑦 ) ) = ( ( ( 𝐹𝑋 ) ‘ 𝑥 ) ( +g𝑇 ) ( ( 𝐹𝑋 ) ‘ 𝑦 ) ) ) ) )
49 5 45 48 sylanbrc ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) )