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 grpmnd 
 |-  ( M e. Grp -> M e. Mnd )
33 31 32 syl 
 |-  ( M e. LMod -> M e. Mnd )
34 33 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> M e. Mnd )
35 simp3 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> X e. V )
36 6 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> M e. LMod )
37 eqeq1 
 |-  ( x = y -> ( x = X <-> y = X ) )
38 37 ifbid 
 |-  ( x = y -> if ( x = X , .1. , .0. ) = if ( y = X , .1. , .0. ) )
39 simpr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> y e. V )
40 eqid 
 |-  ( Base ` S ) = ( Base ` S )
41 2 40 4 lmod1cl 
 |-  ( M e. LMod -> .1. e. ( Base ` S ) )
42 41 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> .1. e. ( Base ` S ) )
43 42 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> .1. e. ( Base ` S ) )
44 2 40 3 lmod0cl 
 |-  ( M e. LMod -> .0. e. ( Base ` S ) )
45 44 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> .0. e. ( Base ` S ) )
46 45 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> .0. e. ( Base ` S ) )
47 43 46 ifcld 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> if ( y = X , .1. , .0. ) e. ( Base ` S ) )
48 5 38 39 47 fvmptd3 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> ( F ` y ) = if ( y = X , .1. , .0. ) )
49 48 47 eqeltrd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> ( F ` y ) e. ( Base ` S ) )
50 elelpwi 
 |-  ( ( y e. V /\ V e. ~P B ) -> y e. B )
51 50 expcom 
 |-  ( V e. ~P B -> ( y e. V -> y e. B ) )
52 51 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( y e. V -> y e. B ) )
53 52 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> y e. B )
54 eqid 
 |-  ( .s ` M ) = ( .s ` M )
55 1 2 54 40 lmodvscl 
 |-  ( ( M e. LMod /\ ( F ` y ) e. ( Base ` S ) /\ y e. B ) -> ( ( F ` y ) ( .s ` M ) y ) e. B )
56 36 49 53 55 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ y e. V ) -> ( ( F ` y ) ( .s ` M ) y ) e. B )
57 eqid 
 |-  ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) = ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) )
58 56 57 fmptd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) : V --> B )
59 fveq2 
 |-  ( y = v -> ( F ` y ) = ( F ` v ) )
60 id 
 |-  ( y = v -> y = v )
61 59 60 oveq12d 
 |-  ( y = v -> ( ( F ` y ) ( .s ` M ) y ) = ( ( F ` v ) ( .s ` M ) v ) )
62 61 cbvmptv 
 |-  ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) = ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) )
63 fvexd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( 0g ` M ) e. _V )
64 ovexd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) e. _V )
65 62 20 63 64 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 ) } )
66 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 ) ) )
67 simprr 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> v e. V )
68 4 fvexi 
 |-  .1. e. _V
69 3 fvexi 
 |-  .0. e. _V
70 68 69 ifex 
 |-  if ( v = X , .1. , .0. ) e. _V
71 eqeq1 
 |-  ( x = v -> ( x = X <-> v = X ) )
72 71 ifbid 
 |-  ( x = v -> if ( x = X , .1. , .0. ) = if ( v = X , .1. , .0. ) )
73 72 5 fvmptg 
 |-  ( ( v e. V /\ if ( v = X , .1. , .0. ) e. _V ) -> ( F ` v ) = if ( v = X , .1. , .0. ) )
74 67 70 73 sylancl 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( F ` v ) = if ( v = X , .1. , .0. ) )
75 iffalse 
 |-  ( -. v = X -> if ( v = X , .1. , .0. ) = .0. )
76 75 adantr 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> if ( v = X , .1. , .0. ) = .0. )
77 74 76 eqtrd 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( F ` v ) = .0. )
78 77 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 ) )
79 6 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> M e. LMod )
80 79 adantl 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> M e. LMod )
81 elelpwi 
 |-  ( ( v e. V /\ V e. ~P B ) -> v e. B )
82 81 expcom 
 |-  ( V e. ~P B -> ( v e. V -> v e. B ) )
83 82 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( v e. V -> v e. B ) )
84 83 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> v e. B )
85 84 adantl 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> v e. B )
86 1 2 54 3 30 lmod0vs 
 |-  ( ( M e. LMod /\ v e. B ) -> ( .0. ( .s ` M ) v ) = ( 0g ` M ) )
87 80 85 86 syl2anc 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( .0. ( .s ` M ) v ) = ( 0g ` M ) )
88 78 87 eqtrd 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( ( F ` v ) ( .s ` M ) v ) = ( 0g ` M ) )
89 88 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 ) ) )
90 eqneqall 
 |-  ( ( 0g ` M ) = ( 0g ` M ) -> ( ( 0g ` M ) =/= ( 0g ` M ) -> v = X ) )
91 30 90 ax-mp 
 |-  ( ( 0g ` M ) =/= ( 0g ` M ) -> v = X )
92 89 91 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 ) )
93 92 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 ) ) )
94 66 93 pm2.61i 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) )
95 94 ralrimiva 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> A. v e. V ( ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) -> v = X ) )
96 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 ) )
97 95 96 sylibr 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> { v e. V | ( ( F ` v ) ( .s ` M ) v ) =/= ( 0g ` M ) } C_ { X } )
98 65 97 eqsstrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) supp ( 0g ` M ) ) C_ { X } )
99 1 30 34 20 35 58 98 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 ) )
100 ovex 
 |-  ( ( F ` X ) ( .s ` M ) X ) e. _V
101 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
102 id 
 |-  ( y = X -> y = X )
103 101 102 oveq12d 
 |-  ( y = X -> ( ( F ` y ) ( .s ` M ) y ) = ( ( F ` X ) ( .s ` M ) X ) )
104 103 57 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 ) )
105 35 100 104 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 ) )
106 iftrue 
 |-  ( x = X -> if ( x = X , .1. , .0. ) = .1. )
107 106 5 fvmptg 
 |-  ( ( X e. V /\ .1. e. _V ) -> ( F ` X ) = .1. )
108 35 68 107 sylancl 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ` X ) = .1. )
109 108 oveq1d 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( F ` X ) ( .s ` M ) X ) = ( .1. ( .s ` M ) X ) )
110 elelpwi 
 |-  ( ( X e. V /\ V e. ~P B ) -> X e. B )
111 110 ancoms 
 |-  ( ( V e. ~P B /\ X e. V ) -> X e. B )
112 111 3adant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> X e. B )
113 1 2 54 4 lmodvs1 
 |-  ( ( M e. LMod /\ X e. B ) -> ( .1. ( .s ` M ) X ) = X )
114 6 112 113 syl2anc 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( .1. ( .s ` M ) X ) = X )
115 105 109 114 3eqtrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( ( y e. V |-> ( ( F ` y ) ( .s ` M ) y ) ) ` X ) = X )
116 29 99 115 3eqtrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ( linC ` M ) V ) = X )