MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uvcresum Structured version   Unicode version

Theorem uvcresum 18932
Description: Any element of a free module can be expressed as a finite linear combination of unit vectors. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Jul-2015.)
Hypotheses
Ref Expression
uvcresum.u  |-  U  =  ( R unitVec  I )
uvcresum.y  |-  Y  =  ( R freeLMod  I )
uvcresum.b  |-  B  =  ( Base `  Y
)
uvcresum.v  |-  .x.  =  ( .s `  Y )
Assertion
Ref Expression
uvcresum  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X  =  ( Y  gsumg  ( X  oF  .x.  U
) ) )

Proof of Theorem uvcresum
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uvcresum.y . . . . . . 7  |-  Y  =  ( R freeLMod  I )
2 eqid 2392 . . . . . . 7  |-  ( Base `  R )  =  (
Base `  R )
3 uvcresum.b . . . . . . 7  |-  B  =  ( Base `  Y
)
41, 2, 3frlmbasf 18902 . . . . . 6  |-  ( ( I  e.  W  /\  X  e.  B )  ->  X : I --> ( Base `  R ) )
543adant1 1012 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X : I --> ( Base `  R ) )
65feqmptd 5840 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X  =  ( a  e.  I  |->  ( X `  a ) ) )
7 eqid 2392 . . . . . . 7  |-  ( 0g
`  R )  =  ( 0g `  R
)
8 simpl1 997 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  R  e.  Ring )
9 ringmnd 17339 . . . . . . . 8  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
108, 9syl 16 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  R  e.  Mnd )
11 simpl2 998 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  I  e.  W )
12 simpr 459 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  a  e.  I )
13 simpl2 998 . . . . . . . . . . . 12  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  I  e.  W )
145ffvelrnda 5946 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( X `  b )  e.  (
Base `  R )
)
15 uvcresum.u . . . . . . . . . . . . . . . . . 18  |-  U  =  ( R unitVec  I )
1615, 1, 3uvcff 18930 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Ring  /\  I  e.  W )  ->  U : I --> B )
17163adant3 1014 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  U : I --> B )
1817ffvelrnda 5946 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( U `  b )  e.  B
)
19 uvcresum.v . . . . . . . . . . . . . . 15  |-  .x.  =  ( .s `  Y )
20 eqid 2392 . . . . . . . . . . . . . . 15  |-  ( .r
`  R )  =  ( .r `  R
)
211, 3, 2, 13, 14, 18, 19, 20frlmvscafval 18907 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( ( X `  b )  .x.  ( U `  b
) )  =  ( ( I  X.  {
( X `  b
) } )  oF ( .r `  R ) ( U `
 b ) ) )
2214adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  b  e.  I )  /\  a  e.  I )  ->  ( X `  b )  e.  ( Base `  R
) )
231, 2, 3frlmbasf 18902 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  W  /\  ( U `  b )  e.  B )  -> 
( U `  b
) : I --> ( Base `  R ) )
2413, 18, 23syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( U `  b ) : I --> ( Base `  R
) )
2524ffvelrnda 5946 . . . . . . . . . . . . . . 15  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  b  e.  I )  /\  a  e.  I )  ->  (
( U `  b
) `  a )  e.  ( Base `  R
) )
26 fconstmpt 4970 . . . . . . . . . . . . . . . 16  |-  ( I  X.  { ( X `
 b ) } )  =  ( a  e.  I  |->  ( X `
 b ) )
2726a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( I  X.  { ( X `  b ) } )  =  ( a  e.  I  |->  ( X `  b ) ) )
2824feqmptd 5840 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( U `  b )  =  ( a  e.  I  |->  ( ( U `  b
) `  a )
) )
2913, 22, 25, 27, 28offval2 6473 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( (
I  X.  { ( X `  b ) } )  oF ( .r `  R
) ( U `  b ) )  =  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) )
3021, 29eqtrd 2433 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( ( X `  b )  .x.  ( U `  b
) )  =  ( a  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) )
311frlmlmod 18890 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  Ring  /\  I  e.  W )  ->  Y  e.  LMod )
32313adant3 1014 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  Y  e.  LMod )
3332adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  Y  e.  LMod )
341frlmsca 18894 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  Ring  /\  I  e.  W )  ->  R  =  (Scalar `  Y )
)
35343adant3 1014 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  R  =  (Scalar `  Y )
)
3635fveq2d 5791 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( Base `  R )  =  ( Base `  (Scalar `  Y ) ) )
3736adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( Base `  R )  =  (
Base `  (Scalar `  Y
) ) )
3814, 37eleqtrd 2482 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( X `  b )  e.  (
Base `  (Scalar `  Y
) ) )
39 eqid 2392 . . . . . . . . . . . . . . 15  |-  (Scalar `  Y )  =  (Scalar `  Y )
40 eqid 2392 . . . . . . . . . . . . . . 15  |-  ( Base `  (Scalar `  Y )
)  =  ( Base `  (Scalar `  Y )
)
413, 39, 19, 40lmodvscl 17661 . . . . . . . . . . . . . 14  |-  ( ( Y  e.  LMod  /\  ( X `  b )  e.  ( Base `  (Scalar `  Y ) )  /\  ( U `  b )  e.  B )  -> 
( ( X `  b )  .x.  ( U `  b )
)  e.  B )
4233, 38, 18, 41syl3anc 1226 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( ( X `  b )  .x.  ( U `  b
) )  e.  B
)
4330, 42eqeltrrd 2481 . . . . . . . . . . . 12  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) )  e.  B )
441, 2, 3frlmbasf 18902 . . . . . . . . . . . 12  |-  ( ( I  e.  W  /\  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) )  e.  B
)  ->  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) : I --> ( Base `  R ) )
4513, 43, 44syl2anc 659 . . . . . . . . . . 11  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) : I --> ( Base `  R ) )
46 eqid 2392 . . . . . . . . . . . 12  |-  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) )  =  ( a  e.  I  |->  ( ( X `
 b ) ( .r `  R ) ( ( U `  b ) `  a
) ) )
4746fmpt 5967 . . . . . . . . . . 11  |-  ( A. a  e.  I  (
( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) )  e.  ( Base `  R
)  <->  ( a  e.  I  |->  ( ( X `
 b ) ( .r `  R ) ( ( U `  b ) `  a
) ) ) : I --> ( Base `  R
) )
4845, 47sylibr 212 . . . . . . . . . 10  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  I
)  ->  A. a  e.  I  ( ( X `  b )
( .r `  R
) ( ( U `
 b ) `  a ) )  e.  ( Base `  R
) )
4948r19.21bi 2761 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  b  e.  I )  /\  a  e.  I )  ->  (
( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) )  e.  ( Base `  R
) )
5049an32s 802 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I )  ->  (
( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) )  e.  ( Base `  R
) )
51 eqid 2392 . . . . . . . 8  |-  ( b  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) )  =  ( b  e.  I  |->  ( ( X `
 b ) ( .r `  R ) ( ( U `  b ) `  a
) ) )
5250, 51fmptd 5970 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( b  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) : I --> ( Base `  R ) )
5383ad2ant1 1015 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  R  e.  Ring )
54113ad2ant1 1015 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  I  e.  W )
55 simp2 995 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  b  e.  I )
56123ad2ant1 1015 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  a  e.  I )
57 simp3 996 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  b  =/=  a )
5815, 53, 54, 55, 56, 57, 7uvcvv0 18929 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  (
( U `  b
) `  a )  =  ( 0g `  R ) )
5958oveq2d 6230 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  (
( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) )  =  ( ( X `
 b ) ( .r `  R ) ( 0g `  R
) ) )
6014adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I )  ->  ( X `  b )  e.  ( Base `  R
) )
61603adant3 1014 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  ( X `  b )  e.  ( Base `  R
) )
622, 20, 7ringrz 17368 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  ( X `  b )  e.  ( Base `  R
) )  ->  (
( X `  b
) ( .r `  R ) ( 0g
`  R ) )  =  ( 0g `  R ) )
6353, 61, 62syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  (
( X `  b
) ( .r `  R ) ( 0g
`  R ) )  =  ( 0g `  R ) )
6459, 63eqtrd 2433 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  I  e.  W  /\  X  e.  B
)  /\  a  e.  I )  /\  b  e.  I  /\  b  =/=  a )  ->  (
( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) )  =  ( 0g `  R ) )
6564, 11suppsssn 6871 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( (
b  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) supp  ( 0g `  R ) )  C_  { a } )
662, 7, 10, 11, 12, 52, 65gsumpt 17121 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( R  gsumg  ( b  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) )  =  ( ( b  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) `  a
) )
67 fveq2 5787 . . . . . . . . . 10  |-  ( b  =  a  ->  ( X `  b )  =  ( X `  a ) )
68 fveq2 5787 . . . . . . . . . . 11  |-  ( b  =  a  ->  ( U `  b )  =  ( U `  a ) )
6968fveq1d 5789 . . . . . . . . . 10  |-  ( b  =  a  ->  (
( U `  b
) `  a )  =  ( ( U `
 a ) `  a ) )
7067, 69oveq12d 6232 . . . . . . . . 9  |-  ( b  =  a  ->  (
( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) )  =  ( ( X `
 a ) ( .r `  R ) ( ( U `  a ) `  a
) ) )
71 ovex 6242 . . . . . . . . 9  |-  ( ( X `  a ) ( .r `  R
) ( ( U `
 a ) `  a ) )  e. 
_V
7270, 51, 71fvmpt 5870 . . . . . . . 8  |-  ( a  e.  I  ->  (
( b  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) `  a
)  =  ( ( X `  a ) ( .r `  R
) ( ( U `
 a ) `  a ) ) )
7372adantl 464 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( (
b  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) `  a )  =  ( ( X `
 a ) ( .r `  R ) ( ( U `  a ) `  a
) ) )
74 eqid 2392 . . . . . . . . . 10  |-  ( 1r
`  R )  =  ( 1r `  R
)
7515, 8, 11, 12, 74uvcvv1 18928 . . . . . . . . 9  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( ( U `  a ) `  a )  =  ( 1r `  R ) )
7675oveq2d 6230 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( ( X `  a )
( .r `  R
) ( ( U `
 a ) `  a ) )  =  ( ( X `  a ) ( .r
`  R ) ( 1r `  R ) ) )
775ffvelrnda 5946 . . . . . . . . 9  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( X `  a )  e.  (
Base `  R )
)
782, 20, 74ringridm 17355 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  ( X `  a )  e.  ( Base `  R
) )  ->  (
( X `  a
) ( .r `  R ) ( 1r
`  R ) )  =  ( X `  a ) )
798, 77, 78syl2anc 659 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( ( X `  a )
( .r `  R
) ( 1r `  R ) )  =  ( X `  a
) )
8076, 79eqtrd 2433 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( ( X `  a )
( .r `  R
) ( ( U `
 a ) `  a ) )  =  ( X `  a
) )
8173, 80eqtrd 2433 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( (
b  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) `  a )  =  ( X `  a ) )
8266, 81eqtrd 2433 . . . . 5  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  a  e.  I
)  ->  ( R  gsumg  ( b  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) )  =  ( X `  a ) )
8382mpteq2dva 4466 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  (
a  e.  I  |->  ( R  gsumg  ( b  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) ) )  =  ( a  e.  I  |->  ( X `  a ) ) )
846, 83eqtr4d 2436 . . 3  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X  =  ( a  e.  I  |->  ( R  gsumg  ( b  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) ) ) )
85 eqid 2392 . . . 4  |-  ( 0g
`  Y )  =  ( 0g `  Y
)
86 simp2 995 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  I  e.  W )
87 simp1 994 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  R  e.  Ring )
88 mptexg 6059 . . . . . 6  |-  ( I  e.  W  ->  (
b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) )  e.  _V )
89883ad2ant2 1016 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  (
b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) )  e.  _V )
90 funmpt 5545 . . . . . 6  |-  Fun  (
b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) )
9190a1i 11 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  Fun  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) ) )
92 fvex 5797 . . . . . 6  |-  ( 0g
`  Y )  e. 
_V
9392a1i 11 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( 0g `  Y )  e. 
_V )
941, 7, 3frlmbasfsupp 18900 . . . . . . 7  |-  ( ( I  e.  W  /\  X  e.  B )  ->  X finSupp  ( 0g `  R ) )
95943adant1 1012 . . . . . 6  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X finSupp  ( 0g `  R ) )
9695fsuppimpd 7769 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( X supp  ( 0g `  R
) )  e.  Fin )
9735eqcomd 2400 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  (Scalar `  Y )  =  R )
9897fveq2d 5791 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( 0g `  (Scalar `  Y
) )  =  ( 0g `  R ) )
9998oveq2d 6230 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( X supp  ( 0g `  (Scalar `  Y ) ) )  =  ( X supp  ( 0g `  R ) ) )
100 ssid 3449 . . . . . . . . . 10  |-  ( X supp  ( 0g `  R
) )  C_  ( X supp  ( 0g `  R
) )
10199, 100syl6eqss 3480 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( X supp  ( 0g `  (Scalar `  Y ) ) ) 
C_  ( X supp  ( 0g `  R ) ) )
102 fvex 5797 . . . . . . . . . 10  |-  ( 0g
`  (Scalar `  Y )
)  e.  _V
103102a1i 11 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( 0g `  (Scalar `  Y
) )  e.  _V )
1045, 101, 86, 103suppssr 6867 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  -> 
( X `  b
)  =  ( 0g
`  (Scalar `  Y )
) )
105104oveq1d 6229 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  -> 
( ( X `  b )  .x.  ( U `  b )
)  =  ( ( 0g `  (Scalar `  Y ) )  .x.  ( U `  b ) ) )
106 eldifi 3553 . . . . . . . 8  |-  ( b  e.  ( I  \ 
( X supp  ( 0g `  R ) ) )  ->  b  e.  I
)
107106, 30sylan2 472 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  -> 
( ( X `  b )  .x.  ( U `  b )
)  =  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) )
10832adantr 463 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  ->  Y  e.  LMod )
109106, 18sylan2 472 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  -> 
( U `  b
)  e.  B )
110 eqid 2392 . . . . . . . . 9  |-  ( 0g
`  (Scalar `  Y )
)  =  ( 0g
`  (Scalar `  Y )
)
1113, 39, 19, 110, 85lmod0vs 17677 . . . . . . . 8  |-  ( ( Y  e.  LMod  /\  ( U `  b )  e.  B )  ->  (
( 0g `  (Scalar `  Y ) )  .x.  ( U `  b ) )  =  ( 0g
`  Y ) )
112108, 109, 111syl2anc 659 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  -> 
( ( 0g `  (Scalar `  Y ) ) 
.x.  ( U `  b ) )  =  ( 0g `  Y
) )
113105, 107, 1123eqtr3d 2441 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  /\  b  e.  (
I  \  ( X supp  ( 0g `  R ) ) ) )  -> 
( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) )  =  ( 0g `  Y ) )
114113, 86suppss2 6870 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  (
( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) ) supp  ( 0g `  Y ) ) 
C_  ( X supp  ( 0g `  R ) ) )
115 suppssfifsupp 7777 . . . . 5  |-  ( ( ( ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `
 b ) ( .r `  R ) ( ( U `  b ) `  a
) ) ) )  e.  _V  /\  Fun  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) )  /\  ( 0g `  Y )  e.  _V )  /\  ( ( X supp  ( 0g `  R ) )  e.  Fin  /\  (
( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) ) supp  ( 0g `  Y ) ) 
C_  ( X supp  ( 0g `  R ) ) ) )  ->  (
b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) ) finSupp  ( 0g
`  Y ) )
11689, 91, 93, 96, 114, 115syl32anc 1234 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  (
b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b
) ( .r `  R ) ( ( U `  b ) `
 a ) ) ) ) finSupp  ( 0g
`  Y ) )
1171, 3, 85, 86, 86, 87, 43, 116frlmgsum 18910 . . 3  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( Y  gsumg  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r
`  R ) ( ( U `  b
) `  a )
) ) ) )  =  ( a  e.  I  |->  ( R  gsumg  ( b  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) ) ) )
11884, 117eqtr4d 2436 . 2  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X  =  ( Y  gsumg  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) ) ) )
1195feqmptd 5840 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X  =  ( b  e.  I  |->  ( X `  b ) ) )
12017feqmptd 5840 . . . . 5  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  U  =  ( b  e.  I  |->  ( U `  b ) ) )
12186, 14, 18, 119, 120offval2 6473 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( X  oF  .x.  U
)  =  ( b  e.  I  |->  ( ( X `  b ) 
.x.  ( U `  b ) ) ) )
12230mpteq2dva 4466 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  (
b  e.  I  |->  ( ( X `  b
)  .x.  ( U `  b ) ) )  =  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `
 b ) ( .r `  R ) ( ( U `  b ) `  a
) ) ) ) )
123121, 122eqtrd 2433 . . 3  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( X  oF  .x.  U
)  =  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) ) )
124123oveq2d 6230 . 2  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  ( Y  gsumg  ( X  oF  .x.  U ) )  =  ( Y  gsumg  ( b  e.  I  |->  ( a  e.  I  |->  ( ( X `  b ) ( .r `  R
) ( ( U `
 b ) `  a ) ) ) ) ) )
125118, 124eqtr4d 2436 1  |-  ( ( R  e.  Ring  /\  I  e.  W  /\  X  e.  B )  ->  X  =  ( Y  gsumg  ( X  oF  .x.  U
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1836    =/= wne 2587   A.wral 2742   _Vcvv 3047    \ cdif 3399    C_ wss 3402   {csn 3957   class class class wbr 4380    |-> cmpt 4438    X. cxp 4924   Fun wfun 5503   -->wf 5505   ` cfv 5509  (class class class)co 6214    oFcof 6455   supp csupp 6835   Fincfn 7453   finSupp cfsupp 7762   Basecbs 14653   .rcmulr 14722  Scalarcsca 14724   .scvsca 14725   0gc0g 14866    gsumg cgsu 14867   Mndcmnd 16055   1rcur 17285   Ringcrg 17330   LModclmod 17644   freeLMod cfrlm 18887   unitVec cuvc 18921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-inf2 7990  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-iin 4259  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-se 4766  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-isom 5518  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-of 6457  df-om 6618  df-1st 6717  df-2nd 6718  df-supp 6836  df-recs 6978  df-rdg 7012  df-1o 7066  df-oadd 7070  df-er 7247  df-map 7358  df-ixp 7407  df-en 7454  df-dom 7455  df-sdom 7456  df-fin 7457  df-fsupp 7763  df-sup 7834  df-oi 7868  df-card 8251  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-nn 10471  df-2 10529  df-3 10530  df-4 10531  df-5 10532  df-6 10533  df-7 10534  df-8 10535  df-9 10536  df-10 10537  df-n0 10731  df-z 10800  df-dec 10914  df-uz 11020  df-fz 11612  df-fzo 11736  df-seq 12030  df-hash 12327  df-struct 14655  df-ndx 14656  df-slot 14657  df-base 14658  df-sets 14659  df-ress 14660  df-plusg 14734  df-mulr 14735  df-sca 14737  df-vsca 14738  df-ip 14739  df-tset 14740  df-ple 14741  df-ds 14743  df-hom 14745  df-cco 14746  df-0g 14868  df-gsum 14869  df-prds 14874  df-pws 14876  df-mre 15012  df-mrc 15013  df-acs 15015  df-mgm 16008  df-sgrp 16047  df-mnd 16057  df-mhm 16102  df-submnd 16103  df-grp 16193  df-minusg 16194  df-sbg 16195  df-mulg 16196  df-subg 16334  df-cntz 16491  df-cmn 16936  df-abl 16937  df-mgp 17274  df-ur 17286  df-ring 17332  df-subrg 17559  df-lmod 17646  df-lss 17711  df-sra 17950  df-rgmod 17951  df-dsmm 18873  df-frlm 18888  df-uvc 18922
This theorem is referenced by:  frlmsslsp  18935
  Copyright terms: Public domain W3C validator