Metamath Proof Explorer

Theorem lmhmimasvsca

Description: Value of the scalar product of the surjective image of a module. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses lmhmimasvsca.w ⊢ 𝑊 = ( 𝐹 “s 𝑉 )
lmhmimasvsca.b ⊢ 𝐵 = ( Base ‘ 𝑉 )
lmhmimasvsca.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
lmhmimasvsca.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
lmhmimasvsca.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
lmhmimasvsca.1 ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ 𝐶 )
lmhmimasvsca.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 LMHom 𝑊 ) )
lmhmimasvsca.2 ⊢ · = ( ·𝑠 ‘ 𝑉 )
lmhmimasvsca.3 ⊢ × = ( ·𝑠 ‘ 𝑊 )
lmhmimasvsca.k ⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑉 ) )
Assertion lmhmimasvsca ( 𝜑 → ( 𝑋 × ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lmhmimasvsca.w ⊢ 𝑊 = ( 𝐹 “s 𝑉 )
2 lmhmimasvsca.b ⊢ 𝐵 = ( Base ‘ 𝑉 )
3 lmhmimasvsca.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
4 lmhmimasvsca.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
5 lmhmimasvsca.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 lmhmimasvsca.1 ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ 𝐶 )
7 lmhmimasvsca.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 LMHom 𝑊 ) )
8 lmhmimasvsca.2 ⊢ · = ( ·𝑠 ‘ 𝑉 )
9 lmhmimasvsca.3 ⊢ × = ( ·𝑠 ‘ 𝑊 )
10 lmhmimasvsca.k ⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑉 ) )
11 1 a1i ⊢ ( 𝜑 → 𝑊 = ( 𝐹 “s 𝑉 ) )
12 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑉 ) )
13 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑊 ) → 𝑉 ∈ LMod )
14 7 13 syl ⊢ ( 𝜑 → 𝑉 ∈ LMod )
15 eqid ⊢ ( Scalar ‘ 𝑉 ) = ( Scalar ‘ 𝑉 )
16 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) )
17 16 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑝 × ( 𝐹 ‘ 𝑎 ) ) = ( 𝑝 × ( 𝐹 ‘ 𝑞 ) ) )
18 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝐹 ∈ ( 𝑉 LMHom 𝑊 ) )
19 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑝 ∈ 𝐾 )
20 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑎 ∈ 𝐵 )
21 15 10 2 8 9 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑉 LMHom 𝑊 ) ∧ 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝑝 × ( 𝐹 ‘ 𝑎 ) ) )
22 18 19 20 21 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝑝 × ( 𝐹 ‘ 𝑎 ) ) )
23 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑞 ∈ 𝐵 )
24 15 10 2 8 9 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑉 LMHom 𝑊 ) ∧ 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝑝 × ( 𝐹 ‘ 𝑞 ) ) )
25 18 19 23 24 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝑝 × ( 𝐹 ‘ 𝑞 ) ) )
26 17 22 25 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
27 26 ex ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
28 11 12 6 14 15 10 8 9 27 imasvscaval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 × ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
29 4 5 28 mpd3an23 ⊢ ( 𝜑 → ( 𝑋 × ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )