This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrspunidl

Description: Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024)

Ref Expression
Hypotheses elrspunidl.n 
|- N = ( RSpan ` R )
elrspunidl.b 
|- B = ( Base ` R )
elrspunidl.1 
|- .0. = ( 0g ` R )
elrspunidl.x 
|- .x. = ( .r ` R )
elrspunidl.r 
|- ( ph -> R e. Ring )
elrspunidl.i 
|- ( ph -> S C_ ( LIdeal ` R ) )
Assertion elrspunidl 
|- ( ph -> ( X e. ( N ` U. S ) <-> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) ) )

Proof

Step Hyp Ref Expression
1 elrspunidl.n 
 |-  N = ( RSpan ` R )
2 elrspunidl.b 
 |-  B = ( Base ` R )
3 elrspunidl.1 
 |-  .0. = ( 0g ` R )
4 elrspunidl.x 
 |-  .x. = ( .r ` R )
5 elrspunidl.r 
 |-  ( ph -> R e. Ring )
6 elrspunidl.i 
 |-  ( ph -> S C_ ( LIdeal ` R ) )
7 6 sselda 
 |-  ( ( ph /\ i e. S ) -> i e. ( LIdeal ` R ) )
8 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
9 2 8 lidlss 
 |-  ( i e. ( LIdeal ` R ) -> i C_ B )
10 7 9 syl 
 |-  ( ( ph /\ i e. S ) -> i C_ B )
11 10 ralrimiva 
 |-  ( ph -> A. i e. S i C_ B )
12 unissb 
 |-  ( U. S C_ B <-> A. i e. S i C_ B )
13 11 12 sylibr 
 |-  ( ph -> U. S C_ B )
14 1 2 3 4 5 13 elrsp 
 |-  ( ph -> ( X e. ( N ` U. S ) <-> E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) ) )
15 fvexd 
 |-  ( ph -> ( LIdeal ` R ) e. _V )
16 15 6 ssexd 
 |-  ( ph -> S e. _V )
17 16 uniexd 
 |-  ( ph -> U. S e. _V )
18 eluni2 
 |-  ( j e. U. S <-> E. i e. S j e. i )
19 18 biimpi 
 |-  ( j e. U. S -> E. i e. S j e. i )
20 19 adantl 
 |-  ( ( ph /\ j e. U. S ) -> E. i e. S j e. i )
21 20 ralrimiva 
 |-  ( ph -> A. j e. U. S E. i e. S j e. i )
22 eleq2 
 |-  ( i = ( f ` j ) -> ( j e. i <-> j e. ( f ` j ) ) )
23 22 ac6sg 
 |-  ( U. S e. _V -> ( A. j e. U. S E. i e. S j e. i -> E. f ( f : U. S --> S /\ A. j e. U. S j e. ( f ` j ) ) ) )
24 17 21 23 sylc 
 |-  ( ph -> E. f ( f : U. S --> S /\ A. j e. U. S j e. ( f ` j ) ) )
25 24 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) -> E. f ( f : U. S --> S /\ A. j e. U. S j e. ( f ` j ) ) )
26 simp-5l 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ph )
27 26 adantr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ph )
28 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
29 27 5 28 3syl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> R e. CMnd )
30 vex 
 |-  f e. _V
31 cnvexg 
 |-  ( f e. _V -> `' f e. _V )
32 imaexg 
 |-  ( `' f e. _V -> ( `' f " { i } ) e. _V )
33 30 31 32 mp2b 
 |-  ( `' f " { i } ) e. _V
34 33 a1i 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( `' f " { i } ) e. _V )
35 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> R e. Ring )
36 elmapi 
 |-  ( b e. ( B ^m U. S ) -> b : U. S --> B )
37 36 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> b : U. S --> B )
38 cnvimass 
 |-  ( `' f " { i } ) C_ dom f
39 fdm 
 |-  ( f : U. S --> S -> dom f = U. S )
40 38 39 sseqtrid 
 |-  ( f : U. S --> S -> ( `' f " { i } ) C_ U. S )
41 40 ad3antlr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( `' f " { i } ) C_ U. S )
42 41 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> l e. U. S )
43 37 42 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> ( b ` l ) e. B )
44 13 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> U. S C_ B )
45 44 42 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> l e. B )
46 2 4 ringcl 
 |-  ( ( R e. Ring /\ ( b ` l ) e. B /\ l e. B ) -> ( ( b ` l ) .x. l ) e. B )
47 35 43 45 46 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ l e. ( `' f " { i } ) ) -> ( ( b ` l ) .x. l ) e. B )
48 fveq2 
 |-  ( j = l -> ( b ` j ) = ( b ` l ) )
49 id 
 |-  ( j = l -> j = l )
50 48 49 oveq12d 
 |-  ( j = l -> ( ( b ` j ) .x. j ) = ( ( b ` l ) .x. l ) )
51 50 cbvmptv 
 |-  ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) = ( l e. ( `' f " { i } ) |-> ( ( b ` l ) .x. l ) )
52 47 51 fmptd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) : ( `' f " { i } ) --> B )
53 34 mptexd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) e. _V )
54 52 ffund 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> Fun ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) )
55 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> b finSupp .0. )
56 nfv 
 |-  F/ j ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. )
57 nfcv 
 |-  F/_ j R
58 nfcv 
 |-  F/_ j gsum
59 nfmpt1 
 |-  F/_ j ( j e. U. S |-> ( ( b ` j ) .x. j ) )
60 57 58 59 nfov 
 |-  F/_ j ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) )
61 60 nfeq2 
 |-  F/ j X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) )
62 56 61 nfan 
 |-  F/ j ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) )
63 nfv 
 |-  F/ j f : U. S --> S
64 62 63 nfan 
 |-  F/ j ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S )
65 nfra1 
 |-  F/ j A. j e. U. S j e. ( f ` j )
66 64 65 nfan 
 |-  F/ j ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) )
67 nfv 
 |-  F/ j i e. S
68 66 67 nfan 
 |-  F/ j ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S )
69 nfcv 
 |-  F/_ j ( `' f " { i } )
70 nfcv 
 |-  F/_ j ( b supp .0. )
71 36 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> b : U. S --> B )
72 71 ffnd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> b Fn U. S )
73 26 17 syl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> U. S e. _V )
74 73 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> U. S e. _V )
75 3 fvexi 
 |-  .0. e. _V
76 75 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> .0. e. _V )
77 41 ssdifd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( ( `' f " { i } ) \ ( b supp .0. ) ) C_ ( U. S \ ( b supp .0. ) ) )
78 77 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> j e. ( U. S \ ( b supp .0. ) ) )
79 72 74 76 78 fvdifsupp 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> ( b ` j ) = .0. )
80 79 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> ( ( b ` j ) .x. j ) = ( .0. .x. j ) )
81 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> R e. Ring )
82 13 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> U. S C_ B )
83 78 eldifad 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> j e. U. S )
84 82 83 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> j e. B )
85 2 4 3 ringlz 
 |-  ( ( R e. Ring /\ j e. B ) -> ( .0. .x. j ) = .0. )
86 81 84 85 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> ( .0. .x. j ) = .0. )
87 80 86 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) /\ j e. ( ( `' f " { i } ) \ ( b supp .0. ) ) ) -> ( ( b ` j ) .x. j ) = .0. )
88 68 69 70 87 34 suppss2f 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) supp .0. ) C_ ( b supp .0. ) )
89 fsuppsssupp 
 |-  ( ( ( ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) e. _V /\ Fun ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) /\ ( b finSupp .0. /\ ( ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) supp .0. ) C_ ( b supp .0. ) ) ) -> ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) finSupp .0. )
90 53 54 55 88 89 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) finSupp .0. )
91 2 3 29 34 52 90 gsumcl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) e. B )
92 91 fmpttd 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) : S --> B )
93 2 fvexi 
 |-  B e. _V
94 93 a1i 
 |-  ( ph -> B e. _V )
95 94 16 elmapd 
 |-  ( ph -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) e. ( B ^m S ) <-> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) : S --> B ) )
96 95 biimpar 
 |-  ( ( ph /\ ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) : S --> B ) -> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) e. ( B ^m S ) )
97 26 92 96 syl2anc 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) e. ( B ^m S ) )
98 breq1 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( a finSupp .0. <-> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. ) )
99 oveq2 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( R gsum a ) = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) )
100 99 eqeq2d 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( X = ( R gsum a ) <-> X = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) ) )
101 fveq1 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( a ` k ) = ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) )
102 101 eleq1d 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( ( a ` k ) e. k <-> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k ) )
103 102 ralbidv 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( A. k e. S ( a ` k ) e. k <-> A. k e. S ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k ) )
104 98 100 103 3anbi123d 
 |-  ( a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) -> ( ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) <-> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. /\ X = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) /\ A. k e. S ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k ) ) )
105 104 adantl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ a = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) -> ( ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) <-> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. /\ X = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) /\ A. k e. S ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k ) ) )
106 26 16 syl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> S e. _V )
107 106 mptexd 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) e. _V )
108 75 a1i 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> .0. e. _V )
109 funmpt 
 |-  Fun ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) )
110 109 a1i 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> Fun ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) )
111 simplr 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> f : U. S --> S )
112 111 ffund 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> Fun f )
113 simp-4r 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> b finSupp .0. )
114 113 fsuppimpd 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( b supp .0. ) e. Fin )
115 imafi 
 |-  ( ( Fun f /\ ( b supp .0. ) e. Fin ) -> ( f " ( b supp .0. ) ) e. Fin )
116 112 114 115 syl2anc 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( f " ( b supp .0. ) ) e. Fin )
117 nfv 
 |-  F/ j i e. ( S \ ( f " ( b supp .0. ) ) )
118 66 117 nfan 
 |-  F/ j ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) )
119 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> f : U. S --> S )
120 119 ffund 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> Fun f )
121 snssi 
 |-  ( i e. ( S \ ( f " ( b supp .0. ) ) ) -> { i } C_ ( S \ ( f " ( b supp .0. ) ) ) )
122 121 adantl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> { i } C_ ( S \ ( f " ( b supp .0. ) ) ) )
123 sspreima 
 |-  ( ( Fun f /\ { i } C_ ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " { i } ) C_ ( `' f " ( S \ ( f " ( b supp .0. ) ) ) ) )
124 120 122 123 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " { i } ) C_ ( `' f " ( S \ ( f " ( b supp .0. ) ) ) ) )
125 difpreima 
 |-  ( Fun f -> ( `' f " ( S \ ( f " ( b supp .0. ) ) ) ) = ( ( `' f " S ) \ ( `' f " ( f " ( b supp .0. ) ) ) ) )
126 120 125 syl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " ( S \ ( f " ( b supp .0. ) ) ) ) = ( ( `' f " S ) \ ( `' f " ( f " ( b supp .0. ) ) ) ) )
127 124 126 sseqtrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " { i } ) C_ ( ( `' f " S ) \ ( `' f " ( f " ( b supp .0. ) ) ) ) )
128 suppssdm 
 |-  ( b supp .0. ) C_ dom b
129 36 ad6antlr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> b : U. S --> B )
130 128 129 fssdm 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( b supp .0. ) C_ U. S )
131 119 fdmd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> dom f = U. S )
132 130 131 sseqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( b supp .0. ) C_ dom f )
133 sseqin2 
 |-  ( ( b supp .0. ) C_ dom f <-> ( dom f i^i ( b supp .0. ) ) = ( b supp .0. ) )
134 133 biimpi 
 |-  ( ( b supp .0. ) C_ dom f -> ( dom f i^i ( b supp .0. ) ) = ( b supp .0. ) )
135 dminss 
 |-  ( dom f i^i ( b supp .0. ) ) C_ ( `' f " ( f " ( b supp .0. ) ) )
136 134 135 eqsstrrdi 
 |-  ( ( b supp .0. ) C_ dom f -> ( b supp .0. ) C_ ( `' f " ( f " ( b supp .0. ) ) ) )
137 132 136 syl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( b supp .0. ) C_ ( `' f " ( f " ( b supp .0. ) ) ) )
138 137 sscond 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( ( `' f " S ) \ ( `' f " ( f " ( b supp .0. ) ) ) ) C_ ( ( `' f " S ) \ ( b supp .0. ) ) )
139 127 138 sstrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " { i } ) C_ ( ( `' f " S ) \ ( b supp .0. ) ) )
140 fimacnv 
 |-  ( f : U. S --> S -> ( `' f " S ) = U. S )
141 119 140 syl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " S ) = U. S )
142 141 difeq1d 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( ( `' f " S ) \ ( b supp .0. ) ) = ( U. S \ ( b supp .0. ) ) )
143 139 142 sseqtrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " { i } ) C_ ( U. S \ ( b supp .0. ) ) )
144 143 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> j e. ( U. S \ ( b supp .0. ) ) )
145 ssidd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( b supp .0. ) C_ ( b supp .0. ) )
146 73 adantr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> U. S e. _V )
147 75 a1i 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> .0. e. _V )
148 129 145 146 147 suppssr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> ( b ` j ) = .0. )
149 144 148 syldan 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> ( b ` j ) = .0. )
150 149 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> ( ( b ` j ) .x. j ) = ( .0. .x. j ) )
151 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> R e. Ring )
152 13 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> U. S C_ B )
153 40 ad3antlr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( `' f " { i } ) C_ U. S )
154 153 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> j e. U. S )
155 152 154 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> j e. B )
156 151 155 85 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> ( .0. .x. j ) = .0. )
157 150 156 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) /\ j e. ( `' f " { i } ) ) -> ( ( b ` j ) .x. j ) = .0. )
158 118 157 mpteq2da 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) = ( j e. ( `' f " { i } ) |-> .0. ) )
159 158 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) = ( R gsum ( j e. ( `' f " { i } ) |-> .0. ) ) )
160 5 28 syl 
 |-  ( ph -> R e. CMnd )
161 160 cmnmndd 
 |-  ( ph -> R e. Mnd )
162 161 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> R e. Mnd )
163 3 gsumz 
 |-  ( ( R e. Mnd /\ ( `' f " { i } ) e. _V ) -> ( R gsum ( j e. ( `' f " { i } ) |-> .0. ) ) = .0. )
164 162 33 163 sylancl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( R gsum ( j e. ( `' f " { i } ) |-> .0. ) ) = .0. )
165 159 164 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. ( S \ ( f " ( b supp .0. ) ) ) ) -> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) = .0. )
166 165 106 suppss2 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) supp .0. ) C_ ( f " ( b supp .0. ) ) )
167 116 166 ssfid 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) supp .0. ) e. Fin )
168 isfsupp 
 |-  ( ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) e. _V /\ .0. e. _V ) -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. <-> ( Fun ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) /\ ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) supp .0. ) e. Fin ) ) )
169 168 biimpar 
 |-  ( ( ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) e. _V /\ .0. e. _V ) /\ ( Fun ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) /\ ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) supp .0. ) e. Fin ) ) -> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. )
170 107 108 110 167 169 syl22anc 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. )
171 simpllr 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) )
172 26 160 syl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> R e. CMnd )
173 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. U. S ) -> R e. Ring )
174 36 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> b : U. S --> B )
175 174 ffvelcdmda 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. U. S ) -> ( b ` j ) e. B )
176 26 13 syl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> U. S C_ B )
177 176 sselda 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. U. S ) -> j e. B )
178 2 4 ringcl 
 |-  ( ( R e. Ring /\ ( b ` j ) e. B /\ j e. B ) -> ( ( b ` j ) .x. j ) e. B )
179 173 175 177 178 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. U. S ) -> ( ( b ` j ) .x. j ) e. B )
180 eqid 
 |-  ( j e. U. S |-> ( ( b ` j ) .x. j ) ) = ( j e. U. S |-> ( ( b ` j ) .x. j ) )
181 66 179 180 fmptdf 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( j e. U. S |-> ( ( b ` j ) .x. j ) ) : U. S --> B )
182 73 mptexd 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( j e. U. S |-> ( ( b ` j ) .x. j ) ) e. _V )
183 funmpt 
 |-  Fun ( j e. U. S |-> ( ( b ` j ) .x. j ) )
184 183 a1i 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> Fun ( j e. U. S |-> ( ( b ` j ) .x. j ) ) )
185 nfcv 
 |-  F/_ j U. S
186 174 adantr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> b : U. S --> B )
187 186 ffnd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> b Fn U. S )
188 73 adantr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> U. S e. _V )
189 75 a1i 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> .0. e. _V )
190 simpr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> j e. ( U. S \ ( b supp .0. ) ) )
191 187 188 189 190 fvdifsupp 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> ( b ` j ) = .0. )
192 191 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> ( ( b ` j ) .x. j ) = ( .0. .x. j ) )
193 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> R e. Ring )
194 176 adantr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> U. S C_ B )
195 190 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> j e. U. S )
196 194 195 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> j e. B )
197 193 196 85 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> ( .0. .x. j ) = .0. )
198 192 197 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ j e. ( U. S \ ( b supp .0. ) ) ) -> ( ( b ` j ) .x. j ) = .0. )
199 66 185 70 198 73 suppss2f 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) supp .0. ) C_ ( b supp .0. ) )
200 fsuppsssupp 
 |-  ( ( ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) e. _V /\ Fun ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) /\ ( b finSupp .0. /\ ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) supp .0. ) C_ ( b supp .0. ) ) ) -> ( j e. U. S |-> ( ( b ` j ) .x. j ) ) finSupp .0. )
201 182 184 113 199 200 syl22anc 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( j e. U. S |-> ( ( b ` j ) .x. j ) ) finSupp .0. )
202 sndisj 
 |-  Disj_ i e. S { i }
203 disjpreima 
 |-  ( ( Fun f /\ Disj_ i e. S { i } ) -> Disj_ i e. S ( `' f " { i } ) )
204 112 202 203 sylancl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> Disj_ i e. S ( `' f " { i } ) )
205 iunid 
 |-  U_ i e. S { i } = S
206 205 imaeq2i 
 |-  ( `' f " U_ i e. S { i } ) = ( `' f " S )
207 iunpreima 
 |-  ( Fun f -> ( `' f " U_ i e. S { i } ) = U_ i e. S ( `' f " { i } ) )
208 112 207 syl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( `' f " U_ i e. S { i } ) = U_ i e. S ( `' f " { i } ) )
209 140 ad2antlr 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( `' f " S ) = U. S )
210 206 208 209 3eqtr3a 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> U_ i e. S ( `' f " { i } ) = U. S )
211 2 3 172 73 106 181 201 204 210 gsumpart 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) = ( R gsum ( i e. S |-> ( R gsum ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) |` ( `' f " { i } ) ) ) ) ) )
212 41 resmptd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) |` ( `' f " { i } ) ) = ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) )
213 212 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ i e. S ) -> ( R gsum ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) |` ( `' f " { i } ) ) ) = ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) )
214 213 mpteq2dva 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( i e. S |-> ( R gsum ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) |` ( `' f " { i } ) ) ) ) = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) )
215 214 oveq2d 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( R gsum ( i e. S |-> ( R gsum ( ( j e. U. S |-> ( ( b ` j ) .x. j ) ) |` ( `' f " { i } ) ) ) ) ) = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) )
216 171 211 215 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> X = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) )
217 eqid 
 |-  ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) = ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) )
218 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ i = k ) -> i = k )
219 218 sneqd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ i = k ) -> { i } = { k } )
220 219 imaeq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ i = k ) -> ( `' f " { i } ) = ( `' f " { k } ) )
221 220 mpteq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ i = k ) -> ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) = ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) )
222 221 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ i = k ) -> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) = ( R gsum ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) ) )
223 simpr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> k e. S )
224 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( R gsum ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) ) e. _V )
225 217 222 223 224 fvmptd2 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) = ( R gsum ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) ) )
226 160 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> R e. CMnd )
227 30 cnvex 
 |-  `' f e. _V
228 227 imaex 
 |-  ( `' f " { k } ) e. _V
229 228 a1i 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( `' f " { k } ) e. _V )
230 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> R e. Ring )
231 26 6 syl 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> S C_ ( LIdeal ` R ) )
232 231 sselda 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> k e. ( LIdeal ` R ) )
233 8 lidlsubg 
 |-  ( ( R e. Ring /\ k e. ( LIdeal ` R ) ) -> k e. ( SubGrp ` R ) )
234 subgsubm 
 |-  ( k e. ( SubGrp ` R ) -> k e. ( SubMnd ` R ) )
235 233 234 syl 
 |-  ( ( R e. Ring /\ k e. ( LIdeal ` R ) ) -> k e. ( SubMnd ` R ) )
236 230 232 235 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> k e. ( SubMnd ` R ) )
237 230 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> R e. Ring )
238 232 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> k e. ( LIdeal ` R ) )
239 36 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> b : U. S --> B )
240 cnvimass 
 |-  ( `' f " { k } ) C_ dom f
241 240 39 sseqtrid 
 |-  ( f : U. S --> S -> ( `' f " { k } ) C_ U. S )
242 241 ad3antlr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( `' f " { k } ) C_ U. S )
243 242 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> l e. U. S )
244 239 243 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> ( b ` l ) e. B )
245 fveq2 
 |-  ( j = l -> ( f ` j ) = ( f ` l ) )
246 49 245 eleq12d 
 |-  ( j = l -> ( j e. ( f ` j ) <-> l e. ( f ` l ) ) )
247 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> A. j e. U. S j e. ( f ` j ) )
248 246 247 243 rspcdva 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> l e. ( f ` l ) )
249 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> f : U. S --> S )
250 249 ffnd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> f Fn U. S )
251 elpreima 
 |-  ( f Fn U. S -> ( l e. ( `' f " { k } ) <-> ( l e. U. S /\ ( f ` l ) e. { k } ) ) )
252 251 biimpa 
 |-  ( ( f Fn U. S /\ l e. ( `' f " { k } ) ) -> ( l e. U. S /\ ( f ` l ) e. { k } ) )
253 elsni 
 |-  ( ( f ` l ) e. { k } -> ( f ` l ) = k )
254 252 253 simpl2im 
 |-  ( ( f Fn U. S /\ l e. ( `' f " { k } ) ) -> ( f ` l ) = k )
255 250 254 sylancom 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> ( f ` l ) = k )
256 248 255 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> l e. k )
257 8 2 4 lidlmcl 
 |-  ( ( ( R e. Ring /\ k e. ( LIdeal ` R ) ) /\ ( ( b ` l ) e. B /\ l e. k ) ) -> ( ( b ` l ) .x. l ) e. k )
258 237 238 244 256 257 syl22anc 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ l e. ( `' f " { k } ) ) -> ( ( b ` l ) .x. l ) e. k )
259 50 cbvmptv 
 |-  ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) = ( l e. ( `' f " { k } ) |-> ( ( b ` l ) .x. l ) )
260 258 259 fmptd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) : ( `' f " { k } ) --> k )
261 229 mptexd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) e. _V )
262 260 ffund 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> Fun ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) )
263 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> b finSupp .0. )
264 nfv 
 |-  F/ j k e. S
265 66 264 nfan 
 |-  F/ j ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S )
266 nfcv 
 |-  F/_ j ( `' f " { k } )
267 36 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> b : U. S --> B )
268 267 ffnd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> b Fn U. S )
269 73 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> U. S e. _V )
270 75 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> .0. e. _V )
271 242 ssdifd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( ( `' f " { k } ) \ ( b supp .0. ) ) C_ ( U. S \ ( b supp .0. ) ) )
272 271 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> j e. ( U. S \ ( b supp .0. ) ) )
273 268 269 270 272 fvdifsupp 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> ( b ` j ) = .0. )
274 273 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> ( ( b ` j ) .x. j ) = ( .0. .x. j ) )
275 13 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> U. S C_ B )
276 272 eldifad 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> j e. U. S )
277 275 276 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> j e. B )
278 230 277 85 syl2an2r 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> ( .0. .x. j ) = .0. )
279 274 278 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) /\ j e. ( ( `' f " { k } ) \ ( b supp .0. ) ) ) -> ( ( b ` j ) .x. j ) = .0. )
280 265 266 70 279 229 suppss2f 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) supp .0. ) C_ ( b supp .0. ) )
281 fsuppsssupp 
 |-  ( ( ( ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) e. _V /\ Fun ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) ) /\ ( b finSupp .0. /\ ( ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) supp .0. ) C_ ( b supp .0. ) ) ) -> ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) finSupp .0. )
282 261 262 263 280 281 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) finSupp .0. )
283 3 226 229 236 260 282 gsumsubmcl 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( R gsum ( j e. ( `' f " { k } ) |-> ( ( b ` j ) .x. j ) ) ) e. k )
284 225 283 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) /\ k e. S ) -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k )
285 284 ralrimiva 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> A. k e. S ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k )
286 170 216 285 3jca 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) finSupp .0. /\ X = ( R gsum ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ) /\ A. k e. S ( ( i e. S |-> ( R gsum ( j e. ( `' f " { i } ) |-> ( ( b ` j ) .x. j ) ) ) ) ` k ) e. k ) )
287 97 105 286 rspcedvd 
 |-  ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ f : U. S --> S ) /\ A. j e. U. S j e. ( f ` j ) ) -> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) )
288 287 anasss 
 |-  ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) /\ ( f : U. S --> S /\ A. j e. U. S j e. ( f ` j ) ) ) -> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) )
289 25 288 exlimddv 
 |-  ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) -> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) )
290 289 anasss 
 |-  ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) ) -> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) )
291 290 r19.29an 
 |-  ( ( ph /\ E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) ) -> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) )
292 5 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> R e. Ring )
293 292 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> R e. Ring )
294 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
295 294 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
296 zringbas 
 |-  ZZ = ( Base ` ZZring )
297 296 2 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> B )
298 293 295 297 3syl 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> ( ZRHom ` R ) : ZZ --> B )
299 simp-5r 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> a e. ( B ^m S ) )
300 75 a1i 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> .0. e. _V )
301 ssv 
 |-  ran a C_ _V
302 ssdif 
 |-  ( ran a C_ _V -> ( ran a \ { .0. } ) C_ ( _V \ { .0. } ) )
303 301 302 ax-mp 
 |-  ( ran a \ { .0. } ) C_ ( _V \ { .0. } )
304 303 sseli 
 |-  ( m e. ( ran a \ { .0. } ) -> m e. ( _V \ { .0. } ) )
305 304 adantl 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> m e. ( _V \ { .0. } ) )
306 simp-4r 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> a finSupp .0. )
307 299 300 305 306 fsuppinisegfi 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> ( `' a " { m } ) e. Fin )
308 hashcl 
 |-  ( ( `' a " { m } ) e. Fin -> ( # ` ( `' a " { m } ) ) e. NN0 )
309 307 308 syl 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> ( # ` ( `' a " { m } ) ) e. NN0 )
310 309 nn0zd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> ( # ` ( `' a " { m } ) ) e. ZZ )
311 298 310 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ m e. ( ran a \ { .0. } ) ) -> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) e. B )
312 eqid 
 |-  ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) = ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) )
313 311 312 fmptd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) : ( ran a \ { .0. } ) --> B )
314 2 3 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
315 fconst6g 
 |-  ( .0. e. B -> ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) : ( U. S \ ( ran a \ { .0. } ) ) --> B )
316 292 314 315 3syl 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) : ( U. S \ ( ran a \ { .0. } ) ) --> B )
317 disjdif 
 |-  ( ( ran a \ { .0. } ) i^i ( U. S \ ( ran a \ { .0. } ) ) ) = (/)
318 317 a1i 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( ran a \ { .0. } ) i^i ( U. S \ ( ran a \ { .0. } ) ) ) = (/) )
319 313 316 318 fun2d 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) : ( ( ran a \ { .0. } ) u. ( U. S \ ( ran a \ { .0. } ) ) ) --> B )
320 simplll 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ph /\ a e. ( B ^m S ) ) )
321 94 16 elmapd 
 |-  ( ph -> ( a e. ( B ^m S ) <-> a : S --> B ) )
322 321 biimpa 
 |-  ( ( ph /\ a e. ( B ^m S ) ) -> a : S --> B )
323 320 322 syl 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> a : S --> B )
324 323 ffnd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> a Fn S )
325 elssuni 
 |-  ( k e. S -> k C_ U. S )
326 325 adantl 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ k e. S ) -> k C_ U. S )
327 326 sseld 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ k e. S ) -> ( ( a ` k ) e. k -> ( a ` k ) e. U. S ) )
328 327 ralimdva 
 |-  ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) -> ( A. k e. S ( a ` k ) e. k -> A. k e. S ( a ` k ) e. U. S ) )
329 328 imp 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> A. k e. S ( a ` k ) e. U. S )
330 fnfvrnss 
 |-  ( ( a Fn S /\ A. k e. S ( a ` k ) e. U. S ) -> ran a C_ U. S )
331 324 329 330 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ran a C_ U. S )
332 331 ssdifssd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ran a \ { .0. } ) C_ U. S )
333 undif 
 |-  ( ( ran a \ { .0. } ) C_ U. S <-> ( ( ran a \ { .0. } ) u. ( U. S \ ( ran a \ { .0. } ) ) ) = U. S )
334 332 333 sylib 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( ran a \ { .0. } ) u. ( U. S \ ( ran a \ { .0. } ) ) ) = U. S )
335 334 feq2d 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) : ( ( ran a \ { .0. } ) u. ( U. S \ ( ran a \ { .0. } ) ) ) --> B <-> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) : U. S --> B ) )
336 319 335 mpbid 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) : U. S --> B )
337 93 a1i 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> B e. _V )
338 17 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> U. S e. _V )
339 337 338 elmapd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) e. ( B ^m U. S ) <-> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) : U. S --> B ) )
340 336 339 mpbird 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) e. ( B ^m U. S ) )
341 breq1 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( b finSupp .0. <-> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. ) )
342 fveq1 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( b ` j ) = ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) )
343 342 oveq1d 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( ( b ` j ) .x. j ) = ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) )
344 343 mpteq2dv 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( j e. U. S |-> ( ( b ` j ) .x. j ) ) = ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) )
345 344 oveq2d 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) = ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) )
346 345 eqeq2d 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) <-> X = ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) ) )
347 341 346 anbi12d 
 |-  ( b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) -> ( ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) <-> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) ) ) )
348 347 adantl 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ b = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ) -> ( ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) <-> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) ) ) )
349 319 ffund 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> Fun ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) )
350 340 elexd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) e. _V )
351 75 a1i 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> .0. e. _V )
352 323 ffund 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> Fun a )
353 320 simprd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> a e. ( B ^m S ) )
354 simpllr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> a finSupp .0. )
355 fsupprnfi 
 |-  ( ( ( Fun a /\ a e. ( B ^m S ) ) /\ ( .0. e. _V /\ a finSupp .0. ) ) -> ran a e. Fin )
356 diffi 
 |-  ( ran a e. Fin -> ( ran a \ { .0. } ) e. Fin )
357 355 356 syl 
 |-  ( ( ( Fun a /\ a e. ( B ^m S ) ) /\ ( .0. e. _V /\ a finSupp .0. ) ) -> ( ran a \ { .0. } ) e. Fin )
358 352 353 351 354 357 syl22anc 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ran a \ { .0. } ) e. Fin )
359 313 358 351 fdmfifsupp 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) finSupp .0. )
360 13 ssdifssd 
 |-  ( ph -> ( U. S \ ( ran a \ { .0. } ) ) C_ B )
361 360 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( U. S \ ( ran a \ { .0. } ) ) C_ B )
362 337 361 ssexd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( U. S \ ( ran a \ { .0. } ) ) e. _V )
363 362 351 fczfsuppd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) finSupp .0. )
364 359 363 fsuppun 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) supp .0. ) e. Fin )
365 funisfsupp 
 |-  ( ( Fun ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) /\ ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) e. _V /\ .0. e. _V ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. <-> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) supp .0. ) e. Fin ) )
366 365 biimpar 
 |-  ( ( ( Fun ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) /\ ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) e. _V /\ .0. e. _V ) /\ ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) supp .0. ) e. Fin ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. )
367 349 350 351 364 366 syl31anc 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. )
368 fvex 
 |-  ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) e. _V
369 368 312 fnmpti 
 |-  ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) Fn ( ran a \ { .0. } )
370 369 a1i 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) Fn ( ran a \ { .0. } ) )
371 fnconstg 
 |-  ( .0. e. _V -> ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) Fn ( U. S \ ( ran a \ { .0. } ) ) )
372 75 371 ax-mp 
 |-  ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) Fn ( U. S \ ( ran a \ { .0. } ) )
373 372 a1i 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) Fn ( U. S \ ( ran a \ { .0. } ) ) )
374 317 a1i 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( ran a \ { .0. } ) i^i ( U. S \ ( ran a \ { .0. } ) ) ) = (/) )
375 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> j e. ( ran a \ { .0. } ) )
376 370 373 374 375 fvun1d 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) = ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) ` j ) )
377 sneq 
 |-  ( m = j -> { m } = { j } )
378 377 imaeq2d 
 |-  ( m = j -> ( `' a " { m } ) = ( `' a " { j } ) )
379 378 fveq2d 
 |-  ( m = j -> ( # ` ( `' a " { m } ) ) = ( # ` ( `' a " { j } ) ) )
380 379 fveq2d 
 |-  ( m = j -> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) = ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) )
381 fvexd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) e. _V )
382 312 380 375 381 fvmptd3 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) ` j ) = ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) )
383 376 382 eqtrd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) = ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) )
384 383 oveq1d 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) = ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) )
385 384 mpteq2dva 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( j e. ( ran a \ { .0. } ) |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) = ( j e. ( ran a \ { .0. } ) |-> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) ) )
386 385 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) = ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) ) ) )
387 292 28 syl 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> R e. CMnd )
388 317 a1i 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ran a \ { .0. } ) i^i ( U. S \ ( ran a \ { .0. } ) ) ) = (/) )
389 fvun2 
 |-  ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) Fn ( ran a \ { .0. } ) /\ ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) Fn ( U. S \ ( ran a \ { .0. } ) ) /\ ( ( ( ran a \ { .0. } ) i^i ( U. S \ ( ran a \ { .0. } ) ) ) = (/) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) = ( ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ` j ) )
390 369 372 389 mp3an12 
 |-  ( ( ( ( ran a \ { .0. } ) i^i ( U. S \ ( ran a \ { .0. } ) ) ) = (/) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) = ( ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ` j ) )
391 388 390 sylancom 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) = ( ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ` j ) )
392 75 fvconst2 
 |-  ( j e. ( U. S \ ( ran a \ { .0. } ) ) -> ( ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ` j ) = .0. )
393 392 adantl 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ` j ) = .0. )
394 391 393 eqtrd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) = .0. )
395 394 oveq1d 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) = ( .0. .x. j ) )
396 361 sselda 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> j e. B )
397 292 396 85 syl2an2r 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( .0. .x. j ) = .0. )
398 395 397 eqtrd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( U. S \ ( ran a \ { .0. } ) ) ) -> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) = .0. )
399 292 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. U. S ) -> R e. Ring )
400 336 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. U. S ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) e. B )
401 13 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> U. S C_ B )
402 401 sselda 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. U. S ) -> j e. B )
403 2 4 ringcl 
 |-  ( ( R e. Ring /\ ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) e. B /\ j e. B ) -> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) e. B )
404 399 400 402 403 syl3anc 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. U. S ) -> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) e. B )
405 2 3 387 338 398 358 404 332 gsummptres2 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) = ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) )
406 eqid 
 |-  ( .g ` R ) = ( .g ` R )
407 2 3 406 387 323 354 gsumhashmul 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( R gsum a ) = ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( # ` ( `' a " { j } ) ) ( .g ` R ) j ) ) ) )
408 simplr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> X = ( R gsum a ) )
409 292 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> R e. Ring )
410 353 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> a e. ( B ^m S ) )
411 75 a1i 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> .0. e. _V )
412 303 375 sselid 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> j e. ( _V \ { .0. } ) )
413 354 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> a finSupp .0. )
414 410 411 412 413 fsuppinisegfi 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( `' a " { j } ) e. Fin )
415 hashcl 
 |-  ( ( `' a " { j } ) e. Fin -> ( # ` ( `' a " { j } ) ) e. NN0 )
416 414 415 syl 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( # ` ( `' a " { j } ) ) e. NN0 )
417 416 nn0zd 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( # ` ( `' a " { j } ) ) e. ZZ )
418 332 401 sstrd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ran a \ { .0. } ) C_ B )
419 418 sselda 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> j e. B )
420 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
421 294 406 420 zrhmulg 
 |-  ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) -> ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( 1r ` R ) ) )
422 421 adantr 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( 1r ` R ) ) )
423 422 oveq1d 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) = ( ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( 1r ` R ) ) .x. j ) )
424 simpll 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> R e. Ring )
425 simplr 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( # ` ( `' a " { j } ) ) e. ZZ )
426 2 420 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
427 426 ad2antrr 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( 1r ` R ) e. B )
428 simpr 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> j e. B )
429 2 406 4 mulgass2 
 |-  ( ( R e. Ring /\ ( ( # ` ( `' a " { j } ) ) e. ZZ /\ ( 1r ` R ) e. B /\ j e. B ) ) -> ( ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( 1r ` R ) ) .x. j ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( ( 1r ` R ) .x. j ) ) )
430 424 425 427 428 429 syl13anc 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( 1r ` R ) ) .x. j ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( ( 1r ` R ) .x. j ) ) )
431 2 4 420 ringlidm 
 |-  ( ( R e. Ring /\ j e. B ) -> ( ( 1r ` R ) .x. j ) = j )
432 424 431 sylancom 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( ( 1r ` R ) .x. j ) = j )
433 432 oveq2d 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( ( # ` ( `' a " { j } ) ) ( .g ` R ) ( ( 1r ` R ) .x. j ) ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) j ) )
434 423 430 433 3eqtrd 
 |-  ( ( ( R e. Ring /\ ( # ` ( `' a " { j } ) ) e. ZZ ) /\ j e. B ) -> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) j ) )
435 409 417 419 434 syl21anc 
 |-  ( ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) /\ j e. ( ran a \ { .0. } ) ) -> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) = ( ( # ` ( `' a " { j } ) ) ( .g ` R ) j ) )
436 435 mpteq2dva 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( j e. ( ran a \ { .0. } ) |-> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) ) = ( j e. ( ran a \ { .0. } ) |-> ( ( # ` ( `' a " { j } ) ) ( .g ` R ) j ) ) )
437 436 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) ) ) = ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( # ` ( `' a " { j } ) ) ( .g ` R ) j ) ) ) )
438 407 408 437 3eqtr4d 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> X = ( R gsum ( j e. ( ran a \ { .0. } ) |-> ( ( ( ZRHom ` R ) ` ( # ` ( `' a " { j } ) ) ) .x. j ) ) ) )
439 386 405 438 3eqtr4rd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> X = ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) )
440 367 439 jca 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( ( ( m e. ( ran a \ { .0. } ) |-> ( ( ZRHom ` R ) ` ( # ` ( `' a " { m } ) ) ) ) u. ( ( U. S \ ( ran a \ { .0. } ) ) X. { .0. } ) ) ` j ) .x. j ) ) ) ) )
441 340 348 440 rspcedvd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m S ) ) /\ a finSupp .0. ) /\ X = ( R gsum a ) ) /\ A. k e. S ( a ` k ) e. k ) -> E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) )
442 441 exp41 
 |-  ( ( ph /\ a e. ( B ^m S ) ) -> ( a finSupp .0. -> ( X = ( R gsum a ) -> ( A. k e. S ( a ` k ) e. k -> E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) ) ) ) )
443 442 3imp2 
 |-  ( ( ( ph /\ a e. ( B ^m S ) ) /\ ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) ) -> E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) )
444 443 r19.29an 
 |-  ( ( ph /\ E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) ) -> E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) )
445 291 444 impbida 
 |-  ( ph -> ( E. b e. ( B ^m U. S ) ( b finSupp .0. /\ X = ( R gsum ( j e. U. S |-> ( ( b ` j ) .x. j ) ) ) ) <-> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) ) )
446 14 445 bitrd 
 |-  ( ph -> ( X e. ( N ` U. S ) <-> E. a e. ( B ^m S ) ( a finSupp .0. /\ X = ( R gsum a ) /\ A. k e. S ( a ` k ) e. k ) ) )