Metamath Proof Explorer


Theorem resmgmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis resmgmhm2.u U = T 𝑠 X
Assertion resmgmhm2b X SubMgm T ran F X F S MgmHom T F S MgmHom U

Proof

Step Hyp Ref Expression
1 resmgmhm2.u U = T 𝑠 X
2 mgmhmrcl F S MgmHom T S Mgm T Mgm
3 2 simpld F S MgmHom T S Mgm
4 3 adantl X SubMgm T ran F X F S MgmHom T S Mgm
5 1 submgmmgm X SubMgm T U Mgm
6 5 ad2antrr X SubMgm T ran F X F S MgmHom T U Mgm
7 4 6 jca X SubMgm T ran F X F S MgmHom T S Mgm U Mgm
8 eqid Base S = Base S
9 eqid Base T = Base T
10 8 9 mgmhmf F S MgmHom T F : Base S Base T
11 10 adantl X SubMgm T ran F X F S MgmHom T F : Base S Base T
12 11 ffnd X SubMgm T ran F X F S MgmHom T F Fn Base S
13 simplr X SubMgm T ran F X F S MgmHom T ran F X
14 df-f F : Base S X F Fn Base S ran F X
15 12 13 14 sylanbrc X SubMgm T ran F X F S MgmHom T F : Base S X
16 1 submgmbas X SubMgm T X = Base U
17 16 ad2antrr X SubMgm T ran F X F S MgmHom T X = Base U
18 17 feq3d X SubMgm T ran F X F S MgmHom T F : Base S X F : Base S Base U
19 15 18 mpbid X SubMgm T ran F X F S MgmHom T F : Base S Base U
20 eqid + S = + S
21 eqid + T = + T
22 8 20 21 mgmhmlin F S MgmHom T x Base S y Base S F x + S y = F x + T F y
23 22 3expb F S MgmHom T x Base S y Base S F x + S y = F x + T F y
24 23 adantll X SubMgm T ran F X F S MgmHom T x Base S y Base S F x + S y = F x + T F y
25 1 21 ressplusg X SubMgm T + T = + U
26 25 ad3antrrr X SubMgm T ran F X F S MgmHom T x Base S y Base S + T = + U
27 26 oveqd X SubMgm T ran F X F S MgmHom T x Base S y Base S F x + T F y = F x + U F y
28 24 27 eqtrd X SubMgm T ran F X F S MgmHom T x Base S y Base S F x + S y = F x + U F y
29 28 ralrimivva X SubMgm T ran F X F S MgmHom T x Base S y Base S F x + S y = F x + U F y
30 19 29 jca X SubMgm T ran F X F S MgmHom T F : Base S Base U x Base S y Base S F x + S y = F x + U F y
31 eqid Base U = Base U
32 eqid + U = + U
33 8 31 20 32 ismgmhm F S MgmHom U S Mgm U Mgm F : Base S Base U x Base S y Base S F x + S y = F x + U F y
34 7 30 33 sylanbrc X SubMgm T ran F X F S MgmHom T F S MgmHom U
35 1 resmgmhm2 F S MgmHom U X SubMgm T F S MgmHom T
36 35 ancoms X SubMgm T F S MgmHom U F S MgmHom T
37 36 adantlr X SubMgm T ran F X F S MgmHom U F S MgmHom T
38 34 37 impbida X SubMgm T ran F X F S MgmHom T F S MgmHom U