Metamath Proof Explorer

Theorem uvcresum

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)

Ref Expression
Hypotheses uvcresum.u 
|- U = ( R unitVec I )
uvcresum.y 
|- Y = ( R freeLMod I )
uvcresum.b 
|- B = ( Base ` Y )
uvcresum.v 
|- .x. = ( .s ` Y )
Assertion uvcresum 
|- ( ( R e. Ring /\ I e. W /\ X e. B ) -> X = ( Y gsum ( X oF .x. U ) ) )

Proof

Step Hyp Ref Expression
1 uvcresum.u 
 |-  U = ( R unitVec I )
2 uvcresum.y 
 |-  Y = ( R freeLMod I )
3 uvcresum.b 
 |-  B = ( Base ` Y )
4 uvcresum.v 
 |-  .x. = ( .s ` Y )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 2 5 3 frlmbasf 
 |-  ( ( I e. W /\ X e. B ) -> X : I --> ( Base ` R ) )
7 6 3adant1 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X : I --> ( Base ` R ) )
8 7 feqmptd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X = ( a e. I |-> ( X ` a ) ) )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 simpl1 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> R e. Ring )
11 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
12 10 11 syl 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> R e. Mnd )
13 simpl2 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> I e. W )
14 simpr 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> a e. I )
15 simpl2 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> I e. W )
16 7 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( X ` b ) e. ( Base ` R ) )
17 1 2 3 uvcff 
 |-  ( ( R e. Ring /\ I e. W ) -> U : I --> B )
18 17 3adant3 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> U : I --> B )
19 18 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( U ` b ) e. B )
20 eqid 
 |-  ( .r ` R ) = ( .r ` R )
21 2 3 5 15 16 19 4 20 frlmvscafval 
 |-  ( ( ( 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 ) ) )
22 16 adantr 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) /\ a e. I ) -> ( X ` b ) e. ( Base ` R ) )
23 2 5 3 frlmbasf 
 |-  ( ( I e. W /\ ( U ` b ) e. B ) -> ( U ` b ) : I --> ( Base ` R ) )
24 15 19 23 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( U ` b ) : I --> ( Base ` R ) )
25 24 ffvelcdmda 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) /\ a e. I ) -> ( ( U ` b ) ` a ) e. ( Base ` R ) )
26 fconstmpt 
 |-  ( I X. { ( X ` b ) } ) = ( a e. I |-> ( X ` b ) )
27 26 a1i 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( I X. { ( X ` b ) } ) = ( a e. I |-> ( X ` b ) ) )
28 24 feqmptd 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( U ` b ) = ( a e. I |-> ( ( U ` b ) ` a ) ) )
29 15 22 25 27 28 offval2 
 |-  ( ( ( 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 ) ) ) )
30 21 29 eqtrd 
 |-  ( ( ( 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 ) ) ) )
31 2 frlmlmod 
 |-  ( ( R e. Ring /\ I e. W ) -> Y e. LMod )
32 31 3adant3 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> Y e. LMod )
33 32 adantr 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> Y e. LMod )
34 2 frlmsca 
 |-  ( ( R e. Ring /\ I e. W ) -> R = ( Scalar ` Y ) )
35 34 3adant3 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> R = ( Scalar ` Y ) )
36 35 fveq2d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
37 36 adantr 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
38 16 37 eleqtrd 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( X ` b ) e. ( Base ` ( Scalar ` Y ) ) )
39 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
40 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
41 3 39 4 40 lmodvscl 
 |-  ( ( Y e. LMod /\ ( X ` b ) e. ( Base ` ( Scalar ` Y ) ) /\ ( U ` b ) e. B ) -> ( ( X ` b ) .x. ( U ` b ) ) e. B )
42 33 38 19 41 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( ( X ` b ) .x. ( U ` b ) ) e. B )
43 30 42 eqeltrrd 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. I ) -> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) e. B )
44 2 5 3 frlmbasf 
 |-  ( ( 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 ) )
45 15 43 44 syl2anc 
 |-  ( ( ( 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 45 fvmptelcdm 
 |-  ( ( ( ( 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 ) )
47 46 an32s 
 |-  ( ( ( ( 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 ) )
48 47 fmpttd 
 |-  ( ( ( 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 ) )
49 10 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> R e. Ring )
50 13 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> I e. W )
51 simp2 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> b e. I )
52 14 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> a e. I )
53 simp3 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> b =/= a )
54 1 49 50 51 52 53 9 uvcvv0 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> ( ( U ` b ) ` a ) = ( 0g ` R ) )
55 54 oveq2d 
 |-  ( ( ( ( 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 ) ) )
56 16 adantlr 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I ) -> ( X ` b ) e. ( Base ` R ) )
57 56 3adant3 
 |-  ( ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) /\ b e. I /\ b =/= a ) -> ( X ` b ) e. ( Base ` R ) )
58 5 20 9 ringrz 
 |-  ( ( R e. Ring /\ ( X ` b ) e. ( Base ` R ) ) -> ( ( X ` b ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
59 49 57 58 syl2anc 
 |-  ( ( ( ( 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 ) )
60 55 59 eqtrd 
 |-  ( ( ( ( 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 ) )
61 60 13 suppsssn 
 |-  ( ( ( 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 } )
62 5 9 12 13 14 48 61 gsumpt 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> ( R gsum ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) = ( ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ` a ) )
63 fveq2 
 |-  ( b = a -> ( X ` b ) = ( X ` a ) )
64 fveq2 
 |-  ( b = a -> ( U ` b ) = ( U ` a ) )
65 64 fveq1d 
 |-  ( b = a -> ( ( U ` b ) ` a ) = ( ( U ` a ) ` a ) )
66 63 65 oveq12d 
 |-  ( b = a -> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) = ( ( X ` a ) ( .r ` R ) ( ( U ` a ) ` a ) ) )
67 eqid 
 |-  ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) = ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) )
68 ovex 
 |-  ( ( X ` a ) ( .r ` R ) ( ( U ` a ) ` a ) ) e. _V
69 66 67 68 fvmpt 
 |-  ( a e. I -> ( ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ` a ) = ( ( X ` a ) ( .r ` R ) ( ( U ` a ) ` a ) ) )
70 69 adantl 
 |-  ( ( ( 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 ) ) )
71 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
72 1 10 13 14 71 uvcvv1 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> ( ( U ` a ) ` a ) = ( 1r ` R ) )
73 72 oveq2d 
 |-  ( ( ( 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 ) ) )
74 7 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> ( X ` a ) e. ( Base ` R ) )
75 5 20 71 ringridm 
 |-  ( ( R e. Ring /\ ( X ` a ) e. ( Base ` R ) ) -> ( ( X ` a ) ( .r ` R ) ( 1r ` R ) ) = ( X ` a ) )
76 10 74 75 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> ( ( X ` a ) ( .r ` R ) ( 1r ` R ) ) = ( X ` a ) )
77 73 76 eqtrd 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> ( ( X ` a ) ( .r ` R ) ( ( U ` a ) ` a ) ) = ( X ` a ) )
78 70 77 eqtrd 
 |-  ( ( ( 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 ) )
79 62 78 eqtrd 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ a e. I ) -> ( R gsum ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) = ( X ` a ) )
80 79 mpteq2dva 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( a e. I |-> ( R gsum ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) ) = ( a e. I |-> ( X ` a ) ) )
81 8 80 eqtr4d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X = ( a e. I |-> ( R gsum ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) ) )
82 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
83 simp2 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> I e. W )
84 simp1 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> R e. Ring )
85 mptexg 
 |-  ( I e. W -> ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) e. _V )
86 85 3ad2ant2 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) e. _V )
87 funmpt 
 |-  Fun ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) )
88 87 a1i 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> Fun ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) )
89 fvexd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( 0g ` Y ) e. _V )
90 2 9 3 frlmbasfsupp 
 |-  ( ( I e. W /\ X e. B ) -> X finSupp ( 0g ` R ) )
91 90 3adant1 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X finSupp ( 0g ` R ) )
92 91 fsuppimpd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( X supp ( 0g ` R ) ) e. Fin )
93 35 eqcomd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( Scalar ` Y ) = R )
94 93 fveq2d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( 0g ` ( Scalar ` Y ) ) = ( 0g ` R ) )
95 94 oveq2d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( X supp ( 0g ` ( Scalar ` Y ) ) ) = ( X supp ( 0g ` R ) ) )
96 ssid 
 |-  ( X supp ( 0g ` R ) ) C_ ( X supp ( 0g ` R ) )
97 95 96 eqsstrdi 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( X supp ( 0g ` ( Scalar ` Y ) ) ) C_ ( X supp ( 0g ` R ) ) )
98 fvexd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( 0g ` ( Scalar ` Y ) ) e. _V )
99 7 97 83 98 suppssr 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. ( I \ ( X supp ( 0g ` R ) ) ) ) -> ( X ` b ) = ( 0g ` ( Scalar ` Y ) ) )
100 99 oveq1d 
 |-  ( ( ( 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 ) ) )
101 eldifi 
 |-  ( b e. ( I \ ( X supp ( 0g ` R ) ) ) -> b e. I )
102 101 30 sylan2 
 |-  ( ( ( 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 ) ) ) )
103 32 adantr 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. ( I \ ( X supp ( 0g ` R ) ) ) ) -> Y e. LMod )
104 101 19 sylan2 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. ( I \ ( X supp ( 0g ` R ) ) ) ) -> ( U ` b ) e. B )
105 eqid 
 |-  ( 0g ` ( Scalar ` Y ) ) = ( 0g ` ( Scalar ` Y ) )
106 3 39 4 105 82 lmod0vs 
 |-  ( ( Y e. LMod /\ ( U ` b ) e. B ) -> ( ( 0g ` ( Scalar ` Y ) ) .x. ( U ` b ) ) = ( 0g ` Y ) )
107 103 104 106 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. W /\ X e. B ) /\ b e. ( I \ ( X supp ( 0g ` R ) ) ) ) -> ( ( 0g ` ( Scalar ` Y ) ) .x. ( U ` b ) ) = ( 0g ` Y ) )
108 100 102 107 3eqtr3d 
 |-  ( ( ( 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 ) )
109 108 83 suppss2 
 |-  ( ( 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 ) ) )
110 suppssfifsupp 
 |-  ( ( ( ( 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 ) )
111 86 88 89 92 109 110 syl32anc 
 |-  ( ( 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 ) )
112 2 3 82 83 83 84 43 111 frlmgsum 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( Y gsum ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) ) = ( a e. I |-> ( R gsum ( b e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) ) )
113 81 112 eqtr4d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X = ( Y gsum ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) ) )
114 7 feqmptd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X = ( b e. I |-> ( X ` b ) ) )
115 18 feqmptd 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> U = ( b e. I |-> ( U ` b ) ) )
116 83 16 19 114 115 offval2 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( X oF .x. U ) = ( b e. I |-> ( ( X ` b ) .x. ( U ` b ) ) ) )
117 30 mpteq2dva 
 |-  ( ( 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 ) ) ) ) )
118 116 117 eqtrd 
 |-  ( ( 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 ) ) ) ) )
119 118 oveq2d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> ( Y gsum ( X oF .x. U ) ) = ( Y gsum ( b e. I |-> ( a e. I |-> ( ( X ` b ) ( .r ` R ) ( ( U ` b ) ` a ) ) ) ) ) )
120 113 119 eqtr4d 
 |-  ( ( R e. Ring /\ I e. W /\ X e. B ) -> X = ( Y gsum ( X oF .x. U ) ) )