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	$⊢ φ \to F : B ⟶ C$
	imasmhm.1	$⊢ \underset{˙}{+} = +_{W}$
	imasmhm.2	$⊢ (φ \land (a \in B \land b \in B) \land (p \in B \land q \in B)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
	imaslmhm.1	$⊢ D = Scalar (W)$
	imaslmhm.2	$⊢ K = {Base}_{D}$
	imaslmhm.3	$⊢ (φ \land (k \in K \land a \in B \land b \in B)) \to (F (a) = F (b) \to F (k \underset{˙}{\times} a) = F (k \underset{˙}{\times} b))$
	imaslmhm.w	$⊢ φ \to W \in LMod$
	imaslmhm.4	$⊢ \underset{˙}{\times} = \cdot_{W}$
Assertion	imaslmhm	$⊢ φ \to (F “_{𝑠} W \in LMod \land F \in (W LMHom (F “_{𝑠} W)))$

Proof

Step	Hyp	Ref	Expression
1		imasmhm.b	$⊢ B = {Base}_{W}$
2		imasmhm.f	$⊢ φ \to F : B ⟶ C$
3		imasmhm.1	$⊢ \underset{˙}{+} = +_{W}$
4		imasmhm.2	$⊢ (φ \land (a \in B \land b \in B) \land (p \in B \land q \in B)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
5		imaslmhm.1	$⊢ D = Scalar (W)$
6		imaslmhm.2	$⊢ K = {Base}_{D}$
7		imaslmhm.3	$⊢ (φ \land (k \in K \land a \in B \land b \in B)) \to (F (a) = F (b) \to F (k \underset{˙}{\times} a) = F (k \underset{˙}{\times} b))$
8		imaslmhm.w	$⊢ φ \to W \in LMod$
9		imaslmhm.4	$⊢ \underset{˙}{\times} = \cdot_{W}$
10		eqidd	$⊢ φ \to F “_{𝑠} W = F “_{𝑠} W$
11	5	fveq2i	$⊢ {Base}_{D} = {Base}_{Scalar (W)}$
12	6 11	eqtri	$⊢ K = {Base}_{Scalar (W)}$
13		eqid	$⊢ 0_{W} = 0_{W}$
14		fimadmfo	$⊢ F : B ⟶ C \to F : B \underset{onto}{⟶} F [B]$
15	2 14	syl	$⊢ φ \to F : B \underset{onto}{⟶} F [B]$
16	10 1 12 3 9 13 15 4 7 8	imaslmod	$⊢ φ \to F “_{𝑠} W \in LMod$
17		eqid	$⊢ \cdot_{(F “_{𝑠} W)} = \cdot_{(F “_{𝑠} W)}$
18		eqid	$⊢ Scalar (F “_{𝑠} W) = Scalar (F “_{𝑠} W)$
19	1	a1i	$⊢ φ \to B = {Base}_{W}$
20	10 19 15 8 5	imassca	$⊢ φ \to D = Scalar (F “_{𝑠} W)$
21	20	eqcomd	$⊢ φ \to Scalar (F “_{𝑠} W) = D$
22	8	lmodgrpd	$⊢ φ \to W \in Grp$
23	1 2 3 4 22	imasghm	$⊢ φ \to (F “_{𝑠} W \in Grp \land F \in (W GrpHom (F “_{𝑠} W)))$
24	23	simprd	$⊢ φ \to F \in (W GrpHom (F “_{𝑠} W))$
25	10 19 15 8 5 6 9 17 7	imasvscaval	$⊢ (φ \land u \in K \land x \in B) \to u \cdot_{(F “_{𝑠} W)} F (x) = F (u \underset{˙}{\times} x)$
26	25	3expb	$⊢ (φ \land (u \in K \land x \in B)) \to u \cdot_{(F “_{𝑠} W)} F (x) = F (u \underset{˙}{\times} x)$
27	26	eqcomd	$⊢ (φ \land (u \in K \land x \in B)) \to F (u \underset{˙}{\times} x) = u \cdot_{(F “_{𝑠} W)} F (x)$
28	1 9 17 5 18 6 8 16 21 24 27	islmhmd	$⊢ φ \to F \in (W LMHom (F “_{𝑠} W))$
29	16 28	jca	$⊢ φ \to (F “_{𝑠} W \in LMod \land F \in (W LMHom (F “_{𝑠} W)))$

Metamath Proof Explorer

Theorem imaslmhm

Proof