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 21 grpmndd ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
23 22 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑀 ∈ Mnd )
24 fvsng ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑌 )
25 24 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑌 )
26 25 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
27 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
28 1 2 27 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
29 28 3com23 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
30 26 29 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
31 fveq2 ⊢ ( 𝑣 = 𝑉 → ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) = ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) )
32 id ⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
33 31 32 oveq12d ⊢ ( 𝑣 = 𝑉 → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
34 1 33 gsumsn ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝐵 ∧ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
35 23 6 30 34 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
36 4 eqcomi ⊢ ( ·𝑠 ‘ 𝑀 ) = ·
37 36 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ·𝑠 ‘ 𝑀 ) = · )
38 eqidd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑉 = 𝑉 )
39 37 25 38 oveq123d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { ⟨ 𝑉 , 𝑌 ⟩ } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑌 · 𝑉 ) )
40 20 35 39 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) )