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