Metamath Proof Explorer

Theorem imaslmhm

Description: Given a function F with homomorphic properties, build the image of a left module. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses imasmhm.b 
|- B = ( Base ` W )
imasmhm.f 
|- ( ph -> F : B --> C )
imasmhm.1 
|- .+ = ( +g ` W )
imasmhm.2 
|- ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imaslmhm.1 
|- D = ( Scalar ` W )
imaslmhm.2 
|- K = ( Base ` D )
imaslmhm.3 
|- ( ( ph /\ ( k e. K /\ a e. B /\ b e. B ) ) -> ( ( F ` a ) = ( F ` b ) -> ( F ` ( k .X. a ) ) = ( F ` ( k .X. b ) ) ) )
imaslmhm.w 
|- ( ph -> W e. LMod )
imaslmhm.4 
|- .X. = ( .s ` W )
Assertion imaslmhm 
|- ( ph -> ( ( F "s W ) e. LMod /\ F e. ( W LMHom ( F "s W ) ) ) )

Proof

Step Hyp Ref Expression
1 imasmhm.b 
 |-  B = ( Base ` W )
2 imasmhm.f 
 |-  ( ph -> F : B --> C )
3 imasmhm.1 
 |-  .+ = ( +g ` W )
4 imasmhm.2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
5 imaslmhm.1 
 |-  D = ( Scalar ` W )
6 imaslmhm.2 
 |-  K = ( Base ` D )
7 imaslmhm.3 
 |-  ( ( ph /\ ( k e. K /\ a e. B /\ b e. B ) ) -> ( ( F ` a ) = ( F ` b ) -> ( F ` ( k .X. a ) ) = ( F ` ( k .X. b ) ) ) )
8 imaslmhm.w 
 |-  ( ph -> W e. LMod )
9 imaslmhm.4 
 |-  .X. = ( .s ` W )
10 eqidd 
 |-  ( ph -> ( F "s W ) = ( F "s W ) )
11 5 fveq2i 
 |-  ( Base ` D ) = ( Base ` ( Scalar ` W ) )
12 6 11 eqtri 
 |-  K = ( Base ` ( Scalar ` W ) )
13 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
14 fimadmfo 
 |-  ( F : B --> C -> F : B -onto-> ( F " B ) )
15 2 14 syl 
 |-  ( ph -> F : B -onto-> ( F " B ) )
16 10 1 12 3 9 13 15 4 7 8 imaslmod 
 |-  ( ph -> ( F "s W ) e. LMod )
17 eqid 
 |-  ( .s ` ( F "s W ) ) = ( .s ` ( F "s W ) )
18 eqid 
 |-  ( Scalar ` ( F "s W ) ) = ( Scalar ` ( F "s W ) )
19 1 a1i 
 |-  ( ph -> B = ( Base ` W ) )
20 10 19 15 8 5 imassca 
 |-  ( ph -> D = ( Scalar ` ( F "s W ) ) )
21 20 eqcomd 
 |-  ( ph -> ( Scalar ` ( F "s W ) ) = D )
22 8 lmodgrpd 
 |-  ( ph -> W e. Grp )
23 1 2 3 4 22 imasghm 
 |-  ( ph -> ( ( F "s W ) e. Grp /\ F e. ( W GrpHom ( F "s W ) ) ) )
24 23 simprd 
 |-  ( ph -> F e. ( W GrpHom ( F "s W ) ) )
25 10 19 15 8 5 6 9 17 7 imasvscaval 
 |-  ( ( ph /\ u e. K /\ x e. B ) -> ( u ( .s ` ( F "s W ) ) ( F ` x ) ) = ( F ` ( u .X. x ) ) )
26 25 3expb 
 |-  ( ( ph /\ ( u e. K /\ x e. B ) ) -> ( u ( .s ` ( F "s W ) ) ( F ` x ) ) = ( F ` ( u .X. x ) ) )
27 26 eqcomd 
 |-  ( ( ph /\ ( u e. K /\ x e. B ) ) -> ( F ` ( u .X. x ) ) = ( u ( .s ` ( F "s W ) ) ( F ` x ) ) )
28 1 9 17 5 18 6 8 16 21 24 27 islmhmd 
 |-  ( ph -> F e. ( W LMHom ( F "s W ) ) )
29 16 28 jca 
 |-  ( ph -> ( ( F "s W ) e. LMod /\ F e. ( W LMHom ( F "s W ) ) ) )