Metamath Proof Explorer

Theorem linc1

Description: A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypotheses linc1.b 
|- B = ( Base ` M )
linc1.s 
|- S = ( Scalar ` M )
linc1.0 
|- .0. = ( 0g ` S )
linc1.1 
|- .1. = ( 1r ` S )
linc1.f 
|- F = ( x e. V |-> if ( x = X , .1. , .0. ) )
Assertion linc1 
|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ( linC ` M ) V ) = X )

Proof

Step Hyp Ref Expression
1 linc1.b 
 |-  B = ( Base ` M )
2 linc1.s 
 |-  S = ( Scalar ` M )
3 linc1.0 
 |-  .0. = ( 0g ` S )
4 linc1.1 
 |-  .1. = ( 1r ` S )
5 linc1.f 
 |-  F = ( x e. V |-> if ( x = X , .1. , .0. ) )
6 simp1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> M e. LMod )
7 2 lmodring 
 |-  ( M e. LMod -> S e. Ring )
8 2 eqcomi 
 |-  ( Scalar ` M ) = S
9 8 fveq2i 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` S )
10 9 4 ringidcl 
 |-  ( S e. Ring -> .1. e. ( Base ` ( Scalar ` M ) ) )
11 9 3 ring0cl 
 |-  ( S e. Ring -> .0. e. ( Base ` ( Scalar ` M ) ) )
12 10 11 jca 
 |-  ( S e. Ring -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
13 7 12 syl 
 |-  ( M e. LMod -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
14 13 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
15 14 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ x e. V ) -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
16 ifcl 
 |-  ( ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) -> if ( x = X , .1. , .0. ) e. ( Base ` ( Scalar ` M ) ) )
17 15 16 syl 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ x e. V ) -> if ( x = X , .1. , .0. ) e. ( Base ` ( Scalar ` M ) ) )
18 17 5 fmptd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
19 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
20 simp2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> V e. ~P B )
21 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ V e. ~P B ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
22 19 20 21 sylancr 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
23 18 22 mpbird 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
24 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
25 24 eleq2i 
 |-  ( V e. ~P B <-> V e. ~P ( Base ` M ) )
26 25 biimpi 
 |-  ( V e. ~P B -> V e. ~P ( Base ` M ) )
27 26 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> V e. ~P ( Base ` M ) )
28 lincval 
 |-  ( ( M e. LMod /\ F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ) )
29 6 23 27 28 syl3anc 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ( linC ` M ) V ) = ( M gsum ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ) )
30 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
31 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
32 31 grpmndd 
 |-  ( M e. LMod -> M e. Mnd )
33 32 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> M e. Mnd )
34 simp3 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> X e. V )
35 6 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> M e. LMod )
36 eqeq1 
 |-  ( x = y -> ( x = X <-> y = X ) )
37 36 ifbid 
 |-  ( x = y -> if ( x = X , .1. , .0. ) = if ( y = X , .1. , .0. ) )
38 simpr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> y e. V )
39 eqid 
 |-  ( Base ` S ) = ( Base ` S )
40 2 39 4 lmod1cl 
 |-  ( M e. LMod -> .1. e. ( Base ` S ) )
41 40 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> .1. e. ( Base ` S ) )
42 41 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> .1. e. ( Base ` S ) )
43 2 39 3 lmod0cl 
 |-  ( M e. LMod -> .0. e. ( Base ` S ) )
44 43 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> .0. e. ( Base ` S ) )
45 44 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> .0. e. ( Base ` S ) )
46 42 45 ifcld 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> if ( y = X , .1. , .0. ) e. ( Base ` S ) )
47 5 37 38 46 fvmptd3 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> ( F ` y ) = if ( y = X , .1. , .0. ) )
48 47 46 eqeltrd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> ( F ` y ) e. ( Base ` S ) )
49 elelpwi 
 |-  ( ( y e. V /\ V e. ~P B ) -> y e. B )
50 49 expcom 
 |-  ( V e. ~P B -> ( y e. V -> y e. B ) )
51 50 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( y e. V -> y e. B ) )
52 51 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> y e. B )
53 eqid 
 |-  ( .s ` M ) = ( .s ` M )
54 1 2 53 39 lmodvscl 
 |-  ( ( M e. LMod /\ ( F ` y ) e. ( Base ` S ) /\ y e. B ) -> ( ( F ` y ) ( .s ` M ) y ) e. B )
55 35 48 52 54 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> ( ( F ` y ) ( .s ` M ) y ) e. B )
56 eqid 
 |-  ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) = ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) )
57 55 56 fmptd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) : V --> B )
58 fveq2 
 |-  ( y = v -> ( F ` y ) = ( F ` v ) )
59 id 
 |-  ( y = v -> y = v )
60 58 59 oveq12d 
 |-  ( y = v -> ( ( F ` y ) ( .s ` M ) y ) = ( ( F ` v ) ( .s ` M ) v ) )
61 60 cbvmptv 
 |-  ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) = ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) )
62 fvexd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( 0g ` M ) e. _V )
63 ovexd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) e. _V )
64 61 20 62 63 mptsuppd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) supp ( 0g ` M ) ) = { v e. V | ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) } )
65 2a1 
 |-  ( v = X -> ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) ) )
66 simprr 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> v e. V )
67 4 fvexi 
 |-  .1. e. _V
68 3 fvexi 
 |-  .0. e. _V
69 67 68 ifex 
 |-  if ( v = X , .1. , .0. ) e. _V
70 eqeq1 
 |-  ( x = v -> ( x = X <-> v = X ) )
71 70 ifbid 
 |-  ( x = v -> if ( x = X , .1. , .0. ) = if ( v = X , .1. , .0. ) )
72 71 5 fvmptg 
 |-  ( ( v e. V /\ if ( v = X , .1. , .0. ) e. _V ) -> ( F ` v ) = if ( v = X , .1. , .0. ) )
73 66 69 72 sylancl 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( F ` v ) = if ( v = X , .1. , .0. ) )
74 iffalse 
 |-  ( -. v = X -> if ( v = X , .1. , .0. ) = .0. )
75 74 adantr 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> if ( v = X , .1. , .0. ) = .0. )
76 73 75 eqtrd 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( F ` v ) = .0. )
77 76 oveq1d 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( ( F ` v ) ( .s ` M ) v ) = ( .0. ( .s ` M ) v ) )
78 6 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> M e. LMod )
79 78 adantl 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> M e. LMod )
80 elelpwi 
 |-  ( ( v e. V /\ V e. ~P B ) -> v e. B )
81 80 expcom 
 |-  ( V e. ~P B -> ( v e. V -> v e. B ) )
82 81 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( v e. V -> v e. B ) )
83 82 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> v e. B )
84 83 adantl 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> v e. B )
85 1 2 53 3 30 lmod0vs 
 |-  ( ( M e. LMod /\ v e. B ) -> ( .0. ( .s ` M ) v ) = ( 0g ` M ) )
86 79 84 85 syl2anc 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( .0. ( .s ` M ) v ) = ( 0g ` M ) )
87 77 86 eqtrd 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( ( F ` v ) ( .s ` M ) v ) = ( 0g ` M ) )
88 87 neeq1d 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) <-> ( 0g ` M ) =/= ( 0g ` M ) ) )
89 eqneqall 
 |-  ( ( 0g ` M ) = ( 0g ` M ) -> ( ( 0g ` M ) =/= ( 0g ` M ) -> v = X ) )
90 30 89 ax-mp 
 |-  ( ( 0g ` M ) =/= ( 0g ` M ) -> v = X )
91 88 90 syl6bi 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) )
92 91 ex 
 |-  ( -. v = X -> ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) ) )
93 65 92 pm2.61i 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) )
94 93 ralrimiva 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> A. v e. V ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) )
95 rabsssn 
 |-  ( { v e. V | ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) } C_ { X } <-> A. v e. V ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) )
96 94 95 sylibr 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> { v e. V | ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) } C_ { X } )
97 64 96 eqsstrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) supp ( 0g ` M ) ) C_ { X } )
98 1 30 33 20 34 57 97 gsumpt 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( M gsum ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ) = ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ` X ) )
99 ovex 
 |-  ( ( F ` X ) ( .s ` M ) X ) e. _V
100 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
101 id 
 |-  ( y = X -> y = X )
102 100 101 oveq12d 
 |-  ( y = X -> ( ( F ` y ) ( .s ` M ) y ) = ( ( F ` X ) ( .s ` M ) X ) )
103 102 56 fvmptg 
 |-  ( ( X e. V /\ ( ( F ` X ) ( .s ` M ) X ) e. _V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ` X ) = ( ( F ` X ) ( .s ` M ) X ) )
104 34 99 103 sylancl 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ` X ) = ( ( F ` X ) ( .s ` M ) X ) )
105 iftrue 
 |-  ( x = X -> if ( x = X , .1. , .0. ) = .1. )
106 105 5 fvmptg 
 |-  ( ( X e. V /\ .1. e. _V ) -> ( F ` X ) = .1. )
107 34 67 106 sylancl 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ` X ) = .1. )
108 107 oveq1d 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( F ` X ) ( .s ` M ) X ) = ( .1. ( .s ` M ) X ) )
109 elelpwi 
 |-  ( ( X e. V /\ V e. ~P B ) -> X e. B )
110 109 ancoms 
 |-  ( ( V e. ~P B /\ X e. V ) -> X e. B )
111 110 3adant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> X e. B )
112 1 2 53 4 lmodvs1 
 |-  ( ( M e. LMod /\ X e. B ) -> ( .1. ( .s ` M ) X ) = X )
113 6 111 112 syl2anc 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( .1. ( .s ` M ) X ) = X )
114 104 108 113 3eqtrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ` X ) = X )
115 29 98 114 3eqtrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ( linC ` M ) V ) = X )