Metamath Proof Explorer


Theorem resmgmhm2

Description: One direction of resmgmhm2b . (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 resmgmhm2.u U = T 𝑠 X
2 mgmhmrcl F S MgmHom U S Mgm U Mgm
3 2 simpld F S MgmHom U S Mgm
4 submgmrcl X SubMgm T T Mgm
5 3 4 anim12i F S MgmHom U X SubMgm T S Mgm T Mgm
6 eqid Base S = Base S
7 eqid Base U = Base U
8 6 7 mgmhmf F S MgmHom U F : Base S Base U
9 1 submgmbas X SubMgm T X = Base U
10 eqid Base T = Base T
11 10 submgmss X SubMgm T X Base T
12 9 11 eqsstrrd X SubMgm T Base U Base T
13 fss F : Base S Base U Base U Base T F : Base S Base T
14 8 12 13 syl2an F S MgmHom U X SubMgm T F : Base S Base T
15 eqid + S = + S
16 eqid + U = + U
17 6 15 16 mgmhmlin F S MgmHom U x Base S y Base S F x + S y = F x + U F y
18 17 3expb F S MgmHom U x Base S y Base S F x + S y = F x + U F y
19 18 adantlr F S MgmHom U X SubMgm T x Base S y Base S F x + S y = F x + U F y
20 eqid + T = + T
21 1 20 ressplusg X SubMgm T + T = + U
22 21 ad2antlr F S MgmHom U X SubMgm T x Base S y Base S + T = + U
23 22 oveqd F S MgmHom U X SubMgm T x Base S y Base S F x + T F y = F x + U F y
24 19 23 eqtr4d F S MgmHom U X SubMgm T x Base S y Base S F x + S y = F x + T F y
25 24 ralrimivva F S MgmHom U X SubMgm T x Base S y Base S F x + S y = F x + T F y
26 14 25 jca F S MgmHom U X SubMgm T F : Base S Base T x Base S y Base S F x + S y = F x + T F y
27 6 10 15 20 ismgmhm F S MgmHom T S Mgm T Mgm F : Base S Base T x Base S y Base S F x + S y = F x + T F y
28 5 26 27 sylanbrc F S MgmHom U X SubMgm T F S MgmHom T