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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	imasmhm.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
	imasmhm.1	⊢ + = ( +g ‘ 𝑊 )
	imasmhm.2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
	imaslmhm.1	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	imaslmhm.2	⊢ 𝐾 = ( Base ‘ 𝐷 )
	imaslmhm.3	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝑘 × 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 × 𝑏 ) ) ) )
	imaslmhm.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	imaslmhm.4	⊢ × = ( ·𝑠 ‘ 𝑊 )
Assertion	imaslmhm	⊢ ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ LMod ∧ 𝐹 ∈ ( 𝑊 LMHom ( 𝐹 “s 𝑊 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		imasmhm.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		imasmhm.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
3		imasmhm.1	⊢ + = ( +g ‘ 𝑊 )
4		imasmhm.2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
5		imaslmhm.1	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
6		imaslmhm.2	⊢ 𝐾 = ( Base ‘ 𝐷 )
7		imaslmhm.3	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝑘 × 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 × 𝑏 ) ) ) )
8		imaslmhm.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
9		imaslmhm.4	⊢ × = ( ·𝑠 ‘ 𝑊 )
10		eqidd	⊢ ( 𝜑 → ( 𝐹 “s 𝑊 ) = ( 𝐹 “s 𝑊 ) )
11	5	fveq2i	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
12	6 11	eqtri	⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
14		fimadmfo	⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 → 𝐹 : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) )
15	2 14	syl	⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) )
16	10 1 12 3 9 13 15 4 7 8	imaslmod	⊢ ( 𝜑 → ( 𝐹 “s 𝑊 ) ∈ LMod )
17		eqid	⊢ ( ·𝑠 ‘ ( 𝐹 “s 𝑊 ) ) = ( ·𝑠 ‘ ( 𝐹 “s 𝑊 ) )
18		eqid	⊢ ( Scalar ‘ ( 𝐹 “s 𝑊 ) ) = ( Scalar ‘ ( 𝐹 “s 𝑊 ) )
19	1	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑊 ) )
20	10 19 15 8 5	imassca	⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ ( 𝐹 “s 𝑊 ) ) )
21	20	eqcomd	⊢ ( 𝜑 → ( Scalar ‘ ( 𝐹 “s 𝑊 ) ) = 𝐷 )
22	8	lmodgrpd	⊢ ( 𝜑 → 𝑊 ∈ Grp )
23	1 2 3 4 22	imasghm	⊢ ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ Grp ∧ 𝐹 ∈ ( 𝑊 GrpHom ( 𝐹 “s 𝑊 ) ) ) )
24	23	simprd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑊 GrpHom ( 𝐹 “s 𝑊 ) ) )
25	10 19 15 8 5 6 9 17 7	imasvscaval	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑢 ( ·𝑠 ‘ ( 𝐹 “s 𝑊 ) ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑢 × 𝑥 ) ) )
26	25	3expb	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑢 ( ·𝑠 ‘ ( 𝐹 “s 𝑊 ) ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑢 × 𝑥 ) ) )
27	26	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑢 × 𝑥 ) ) = ( 𝑢 ( ·𝑠 ‘ ( 𝐹 “s 𝑊 ) ) ( 𝐹 ‘ 𝑥 ) ) )
28	1 9 17 5 18 6 8 16 21 24 27	islmhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑊 LMHom ( 𝐹 “s 𝑊 ) ) )
29	16 28	jca	⊢ ( 𝜑 → ( ( 𝐹 “s 𝑊 ) ∈ LMod ∧ 𝐹 ∈ ( 𝑊 LMHom ( 𝐹 “s 𝑊 ) ) ) )