Metamath Proof Explorer


Theorem reslmhm2

Description: Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Hypotheses reslmhm2.u U=T𝑠X
reslmhm2.l L=LSubSpT
Assertion reslmhm2 FSLMHomUTLModXLFSLMHomT

Proof

Step Hyp Ref Expression
1 reslmhm2.u U=T𝑠X
2 reslmhm2.l L=LSubSpT
3 eqid BaseS=BaseS
4 eqid S=S
5 eqid T=T
6 eqid ScalarS=ScalarS
7 eqid ScalarT=ScalarT
8 eqid BaseScalarS=BaseScalarS
9 lmhmlmod1 FSLMHomUSLMod
10 9 3ad2ant1 FSLMHomUTLModXLSLMod
11 simp2 FSLMHomUTLModXLTLMod
12 1 7 resssca XLScalarT=ScalarU
13 12 3ad2ant3 FSLMHomUTLModXLScalarT=ScalarU
14 eqid ScalarU=ScalarU
15 6 14 lmhmsca FSLMHomUScalarU=ScalarS
16 15 3ad2ant1 FSLMHomUTLModXLScalarU=ScalarS
17 13 16 eqtrd FSLMHomUTLModXLScalarT=ScalarS
18 lmghm FSLMHomUFSGrpHomU
19 18 3ad2ant1 FSLMHomUTLModXLFSGrpHomU
20 2 lsssubg TLModXLXSubGrpT
21 20 3adant1 FSLMHomUTLModXLXSubGrpT
22 1 resghm2 FSGrpHomUXSubGrpTFSGrpHomT
23 19 21 22 syl2anc FSLMHomUTLModXLFSGrpHomT
24 eqid U=U
25 6 8 3 4 24 lmhmlin FSLMHomUxBaseScalarSyBaseSFxSy=xUFy
26 25 3expb FSLMHomUxBaseScalarSyBaseSFxSy=xUFy
27 26 3ad2antl1 FSLMHomUTLModXLxBaseScalarSyBaseSFxSy=xUFy
28 simpl3 FSLMHomUTLModXLxBaseScalarSyBaseSXL
29 1 5 ressvsca XLT=U
30 29 oveqd XLxTFy=xUFy
31 28 30 syl FSLMHomUTLModXLxBaseScalarSyBaseSxTFy=xUFy
32 27 31 eqtr4d FSLMHomUTLModXLxBaseScalarSyBaseSFxSy=xTFy
33 3 4 5 6 7 8 10 11 17 23 32 islmhmd FSLMHomUTLModXLFSLMHomT