Metamath Proof Explorer

Theorem lincvalsng

Description: The linear combination over a singleton. (Contributed by AV, 25-May-2019)

Ref Expression
Hypotheses lincvalsn.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincvalsn.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lincvalsn.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
lincvalsn.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
Assertion lincvalsng ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) )

Proof

Step Hyp Ref Expression
1 lincvalsn.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincvalsn.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 lincvalsn.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
4 lincvalsn.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
5 simp1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑀 ∈ LMod )
6 simp2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑉 ∈ 𝐵 )
7 2 fveq2i ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
8 3 7 eqtri ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
9 8 eleq2i ⊢ ( 𝑌 ∈ 𝑅 ↔ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
10 9 biimpi ⊢ ( 𝑌 ∈ 𝑅 → 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
11 10 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12 fvexd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
13 eqid ⊢ { ⟨ 𝑉 , 𝑌 ⟩ } = { ⟨ 𝑉 , 𝑌 ⟩ }
14 13 mapsnop ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) → { ⟨ 𝑉 , 𝑌 ⟩ } ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 } ) )
15 6 11 12 14 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → { ⟨ 𝑉 , 𝑌 ⟩ } ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 } ) )
16 snelpwi ⊢ ( 𝑉 ∈ ( Base ‘ 𝑀 ) → { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
17 16 1 eleq2s ⊢ ( 𝑉 ∈ 𝐵 → { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
18 17 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
19 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ { ⟨ 𝑉 , 𝑌 ⟩ } ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 } ) ∧ { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
20 5 15 18 19 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
21 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
22 grpmnd ⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
23 21 22 syl ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
24 23 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑀 ∈ Mnd )
25 fvsng ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑌 )
26 25 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑌 )
27 26 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
28 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
29 1 2 28 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
30 29 3com23 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
31 27 30 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
32 fveq2 ⊢ ( 𝑣 = 𝑉 → ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) = ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) )
33 id ⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
34 32 33 oveq12d ⊢ ( 𝑣 = 𝑉 → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
35 1 34 gsumsn ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝐵 ∧ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
36 24 6 31 35 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
37 4 eqcomi ⊢ ( ·𝑠 ‘ 𝑀 ) = ·
38 37 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ·𝑠 ‘ 𝑀 ) = · )
39 eqidd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑉 = 𝑉 )
40 38 26 39 oveq123d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑌 · 𝑉 ) )
41 20 36 40 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) )