This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 𝑊 ) ) ) )