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 U=S𝑠X
Assertion resmgmhm FSMgmHomTXSubMgmSFXUMgmHomT

Proof

Step Hyp Ref Expression
1 resmgmhm.u U=S𝑠X
2 mgmhmrcl FSMgmHomTSMgmTMgm
3 2 simprd FSMgmHomTTMgm
4 1 submgmmgm XSubMgmSUMgm
5 3 4 anim12ci FSMgmHomTXSubMgmSUMgmTMgm
6 eqid BaseS=BaseS
7 eqid BaseT=BaseT
8 6 7 mgmhmf FSMgmHomTF:BaseSBaseT
9 6 submgmss XSubMgmSXBaseS
10 fssres F:BaseSBaseTXBaseSFX:XBaseT
11 8 9 10 syl2an FSMgmHomTXSubMgmSFX:XBaseT
12 9 adantl FSMgmHomTXSubMgmSXBaseS
13 1 6 ressbas2 XBaseSX=BaseU
14 12 13 syl FSMgmHomTXSubMgmSX=BaseU
15 14 feq2d FSMgmHomTXSubMgmSFX:XBaseTFX:BaseUBaseT
16 11 15 mpbid FSMgmHomTXSubMgmSFX:BaseUBaseT
17 simpll FSMgmHomTXSubMgmSxXyXFSMgmHomT
18 9 ad2antlr FSMgmHomTXSubMgmSxXyXXBaseS
19 simprl FSMgmHomTXSubMgmSxXyXxX
20 18 19 sseldd FSMgmHomTXSubMgmSxXyXxBaseS
21 simprr FSMgmHomTXSubMgmSxXyXyX
22 18 21 sseldd FSMgmHomTXSubMgmSxXyXyBaseS
23 eqid +S=+S
24 eqid +T=+T
25 6 23 24 mgmhmlin FSMgmHomTxBaseSyBaseSFx+Sy=Fx+TFy
26 17 20 22 25 syl3anc FSMgmHomTXSubMgmSxXyXFx+Sy=Fx+TFy
27 23 submgmcl XSubMgmSxXyXx+SyX
28 27 3expb XSubMgmSxXyXx+SyX
29 28 adantll FSMgmHomTXSubMgmSxXyXx+SyX
30 fvres x+SyXFXx+Sy=Fx+Sy
31 29 30 syl FSMgmHomTXSubMgmSxXyXFXx+Sy=Fx+Sy
32 fvres xXFXx=Fx
33 fvres yXFXy=Fy
34 32 33 oveqan12d xXyXFXx+TFXy=Fx+TFy
35 34 adantl FSMgmHomTXSubMgmSxXyXFXx+TFXy=Fx+TFy
36 26 31 35 3eqtr4d FSMgmHomTXSubMgmSxXyXFXx+Sy=FXx+TFXy
37 36 ralrimivva FSMgmHomTXSubMgmSxXyXFXx+Sy=FXx+TFXy
38 1 23 ressplusg XSubMgmS+S=+U
39 38 adantl FSMgmHomTXSubMgmS+S=+U
40 39 oveqd FSMgmHomTXSubMgmSx+Sy=x+Uy
41 40 fveqeq2d FSMgmHomTXSubMgmSFXx+Sy=FXx+TFXyFXx+Uy=FXx+TFXy
42 14 41 raleqbidv FSMgmHomTXSubMgmSyXFXx+Sy=FXx+TFXyyBaseUFXx+Uy=FXx+TFXy
43 14 42 raleqbidv FSMgmHomTXSubMgmSxXyXFXx+Sy=FXx+TFXyxBaseUyBaseUFXx+Uy=FXx+TFXy
44 37 43 mpbid FSMgmHomTXSubMgmSxBaseUyBaseUFXx+Uy=FXx+TFXy
45 16 44 jca FSMgmHomTXSubMgmSFX:BaseUBaseTxBaseUyBaseUFXx+Uy=FXx+TFXy
46 eqid BaseU=BaseU
47 eqid +U=+U
48 46 7 47 24 ismgmhm FXUMgmHomTUMgmTMgmFX:BaseUBaseTxBaseUyBaseUFXx+Uy=FXx+TFXy
49 5 45 48 sylanbrc FSMgmHomTXSubMgmSFXUMgmHomT