Theorem elrspunidl

Description: Elementhood to 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	ffvelrnd	|- ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ 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	ffvelrnda	|- ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ 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	ffvelrnd	|- ( ( ( ( ( ( ( ( ph /\ b e. ( B ^m U. S ) ) /\ b finSupp .0. ) /\ 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	ffvelrnd	|- ( ( ( ( ( ( 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	ffvelrnda	|- ( ( ( ( ( ( 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 ) ) )