Metamath Proof Explorer

Theorem lincvalsng

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

Ref Expression
Hypotheses lincvalsn.b 
|- B = ( Base ` M )
lincvalsn.s 
|- S = ( Scalar ` M )
lincvalsn.r 
|- R = ( Base ` S )
lincvalsn.t 
|- .x. = ( .s ` M )
Assertion lincvalsng 
|- ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( { <. V , Y >. } ( linC ` M ) { V } ) = ( Y .x. V ) )

Proof

Step Hyp Ref Expression
1 lincvalsn.b 
 |-  B = ( Base ` M )
2 lincvalsn.s 
 |-  S = ( Scalar ` M )
3 lincvalsn.r 
 |-  R = ( Base ` S )
4 lincvalsn.t 
 |-  .x. = ( .s ` M )
5 simp1 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> M e. LMod )
6 simp2 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> V e. B )
7 2 fveq2i 
 |-  ( Base ` S ) = ( Base ` ( Scalar ` M ) )
8 3 7 eqtri 
 |-  R = ( Base ` ( Scalar ` M ) )
9 8 eleq2i 
 |-  ( Y e. R <-> Y e. ( Base ` ( Scalar ` M ) ) )
10 9 biimpi 
 |-  ( Y e. R -> Y e. ( Base ` ( Scalar ` M ) ) )
11 10 3ad2ant3 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> Y e. ( Base ` ( Scalar ` M ) ) )
12 fvexd 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( Base ` ( Scalar ` M ) ) e. _V )
13 eqid 
 |-  { <. V , Y >. } = { <. V , Y >. }
14 13 mapsnop 
 |-  ( ( V e. B /\ Y e. ( Base ` ( Scalar ` M ) ) /\ ( Base ` ( Scalar ` M ) ) e. _V ) -> { <. V , Y >. } e. ( ( Base ` ( Scalar ` M ) ) ^m { V } ) )
15 6 11 12 14 syl3anc 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> { <. V , Y >. } e. ( ( Base ` ( Scalar ` M ) ) ^m { V } ) )
16 snelpwi 
 |-  ( V e. ( Base ` M ) -> { V } e. ~P ( Base ` M ) )
17 16 1 eleq2s 
 |-  ( V e. B -> { V } e. ~P ( Base ` M ) )
18 17 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> { V } e. ~P ( Base ` M ) )
19 lincval 
 |-  ( ( M e. LMod /\ { <. V , Y >. } e. ( ( Base ` ( Scalar ` M ) ) ^m { V } ) /\ { V } e. ~P ( Base ` M ) ) -> ( { <. V , Y >. } ( linC ` M ) { V } ) = ( M gsum ( v e. { V } |-> ( ( { <. V , Y >. } ` v ) ( .s ` M ) v ) ) ) )
20 5 15 18 19 syl3anc 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( { <. V , Y >. } ( linC ` M ) { V } ) = ( M gsum ( v e. { V } |-> ( ( { <. V , Y >. } ` v ) ( .s ` M ) v ) ) ) )
21 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
22 grpmnd 
 |-  ( M e. Grp -> M e. Mnd )
23 21 22 syl 
 |-  ( M e. LMod -> M e. Mnd )
24 23 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> M e. Mnd )
25 fvsng 
 |-  ( ( V e. B /\ Y e. R ) -> ( { <. V , Y >. } ` V ) = Y )
26 25 3adant1 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( { <. V , Y >. } ` V ) = Y )
27 26 oveq1d 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) = ( Y ( .s ` M ) V ) )
28 eqid 
 |-  ( .s ` M ) = ( .s ` M )
29 1 2 28 3 lmodvscl 
 |-  ( ( M e. LMod /\ Y e. R /\ V e. B ) -> ( Y ( .s ` M ) V ) e. B )
30 29 3com23 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( Y ( .s ` M ) V ) e. B )
31 27 30 eqeltrd 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) e. B )
32 fveq2 
 |-  ( v = V -> ( { <. V , Y >. } ` v ) = ( { <. V , Y >. } ` V ) )
33 id 
 |-  ( v = V -> v = V )
34 32 33 oveq12d 
 |-  ( v = V -> ( ( { <. V , Y >. } ` v ) ( .s ` M ) v ) = ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) )
35 1 34 gsumsn 
 |-  ( ( M e. Mnd /\ V e. B /\ ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) e. B ) -> ( M gsum ( v e. { V } |-> ( ( { <. V , Y >. } ` v ) ( .s ` M ) v ) ) ) = ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) )
36 24 6 31 35 syl3anc 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( M gsum ( v e. { V } |-> ( ( { <. V , Y >. } ` v ) ( .s ` M ) v ) ) ) = ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) )
37 4 eqcomi 
 |-  ( .s ` M ) = .x.
38 37 a1i 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( .s ` M ) = .x. )
39 eqidd 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> V = V )
40 38 26 39 oveq123d 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( ( { <. V , Y >. } ` V ) ( .s ` M ) V ) = ( Y .x. V ) )
41 20 36 40 3eqtrd 
 |-  ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( { <. V , Y >. } ( linC ` M ) { V } ) = ( Y .x. V ) )