Theorem gsummptfidmsplit 14254

Description: Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019.)

Hypotheses

Ref	Expression
gsummptfidmsplit.b	|- B = ( Base ` G )
gsummptfidmsplit.p	|- .+ = ( +g ` G )
gsummptfidmsplit.g	|- ( ph -> G e. CMnd )
gsummptfidmsplit.a	|- ( ph -> A e. Fin )
gsummptfidmsplit.y	|- ( ( ph /\ k e. A ) -> Y e. B )
gsummptfidmsplit.i	|- ( ph -> ( C i^i D ) = (/) )
gsummptfidmsplit.u	|- ( ph -> A = ( C u. D ) )

Assertion

Ref	Expression
gsummptfidmsplit	|- ( ph -> ( G gsumg ( k e. A |-> Y ) ) = ( ( G gsumg ( k e. C |-> Y ) ) .+ ( G gsumg ( k e. D |-> Y ) ) ) )

Distinct variable groups:   A, k   B, k   C, k   D, k   ph, k

Allowed substitution hints:   .+ ( k)   G( k)   Y( k)

Proof of Theorem gsummptfidmsplit

Dummy variables w y z q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpteq1 4216	. . . . 5 |- ( w = (/) -> ( k e. w |-> Y ) = ( k e. (/) |-> Y ) )
2	1	oveq2d 6104	. . . 4 |- ( w = (/) -> ( G gsumg ( k e. w |-> Y ) ) = ( G gsumg ( k e. (/) |-> Y ) ) )
3		ineq2 3426	. . . . . . 7 |- ( w = (/) -> ( C i^i w ) = ( C i^i (/) ) )
4	3	mpteq1d 4217	. . . . . 6 |- ( w = (/) -> ( k e. ( C i^i w ) |-> Y ) = ( k e. ( C i^i (/) ) |-> Y ) )
5	4	oveq2d 6104	. . . . 5 |- ( w = (/) -> ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) )
6		ineq2 3426	. . . . . . 7 |- ( w = (/) -> ( D i^i w ) = ( D i^i (/) ) )
7	6	mpteq1d 4217	. . . . . 6 |- ( w = (/) -> ( k e. ( D i^i w ) |-> Y ) = ( k e. ( D i^i (/) ) |-> Y ) )
8	7	oveq2d 6104	. . . . 5 |- ( w = (/) -> ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) )
9	5, 8	oveq12d 6106	. . . 4 |- ( w = (/) -> ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) ) )
10	2, 9	eqeq12d 2253	. . 3 |- ( w = (/) -> ( ( G gsumg ( k e. w |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) <-> ( G gsumg ( k e. (/) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) ) ) )
11		mpteq1 4216	. . . . 5 |- ( w = y -> ( k e. w |-> Y ) = ( k e. y |-> Y ) )
12	11	oveq2d 6104	. . . 4 |- ( w = y -> ( G gsumg ( k e. w |-> Y ) ) = ( G gsumg ( k e. y |-> Y ) ) )
13		ineq2 3426	. . . . . . 7 |- ( w = y -> ( C i^i w ) = ( C i^i y ) )
14	13	mpteq1d 4217	. . . . . 6 |- ( w = y -> ( k e. ( C i^i w ) |-> Y ) = ( k e. ( C i^i y ) |-> Y ) )
15	14	oveq2d 6104	. . . . 5 |- ( w = y -> ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) )
16		ineq2 3426	. . . . . . 7 |- ( w = y -> ( D i^i w ) = ( D i^i y ) )
17	16	mpteq1d 4217	. . . . . 6 |- ( w = y -> ( k e. ( D i^i w ) |-> Y ) = ( k e. ( D i^i y ) |-> Y ) )
18	17	oveq2d 6104	. . . . 5 |- ( w = y -> ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) )
19	15, 18	oveq12d 6106	. . . 4 |- ( w = y -> ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
20	12, 19	eqeq12d 2253	. . 3 |- ( w = y -> ( ( G gsumg ( k e. w |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) <-> ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) )
21		mpteq1 4216	. . . . 5 |- ( w = ( y u. { z } ) -> ( k e. w |-> Y ) = ( k e. ( y u. { z } ) |-> Y ) )
22	21	oveq2d 6104	. . . 4 |- ( w = ( y u. { z } ) -> ( G gsumg ( k e. w |-> Y ) ) = ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) )
23		ineq2 3426	. . . . . . 7 |- ( w = ( y u. { z } ) -> ( C i^i w ) = ( C i^i ( y u. { z } ) ) )
24	23	mpteq1d 4217	. . . . . 6 |- ( w = ( y u. { z } ) -> ( k e. ( C i^i w ) |-> Y ) = ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) )
25	24	oveq2d 6104	. . . . 5 |- ( w = ( y u. { z } ) -> ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) )
26		ineq2 3426	. . . . . . 7 |- ( w = ( y u. { z } ) -> ( D i^i w ) = ( D i^i ( y u. { z } ) ) )
27	26	mpteq1d 4217	. . . . . 6 |- ( w = ( y u. { z } ) -> ( k e. ( D i^i w ) |-> Y ) = ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) )
28	27	oveq2d 6104	. . . . 5 |- ( w = ( y u. { z } ) -> ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) )
29	25, 28	oveq12d 6106	. . . 4 |- ( w = ( y u. { z } ) -> ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) )
30	22, 29	eqeq12d 2253	. . 3 |- ( w = ( y u. { z } ) -> ( ( G gsumg ( k e. w |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) <-> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) ) )
31		mpteq1 4216	. . . . 5 |- ( w = A -> ( k e. w |-> Y ) = ( k e. A |-> Y ) )
32	31	oveq2d 6104	. . . 4 |- ( w = A -> ( G gsumg ( k e. w |-> Y ) ) = ( G gsumg ( k e. A |-> Y ) ) )
33		ineq2 3426	. . . . . . 7 |- ( w = A -> ( C i^i w ) = ( C i^i A ) )
34	33	mpteq1d 4217	. . . . . 6 |- ( w = A -> ( k e. ( C i^i w ) |-> Y ) = ( k e. ( C i^i A ) |-> Y ) )
35	34	oveq2d 6104	. . . . 5 |- ( w = A -> ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( C i^i A ) |-> Y ) ) )
36		ineq2 3426	. . . . . . 7 |- ( w = A -> ( D i^i w ) = ( D i^i A ) )
37	36	mpteq1d 4217	. . . . . 6 |- ( w = A -> ( k e. ( D i^i w ) |-> Y ) = ( k e. ( D i^i A ) |-> Y ) )
38	37	oveq2d 6104	. . . . 5 |- ( w = A -> ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) = ( G gsumg ( k e. ( D i^i A ) |-> Y ) ) )
39	35, 38	oveq12d 6106	. . . 4 |- ( w = A -> ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i A ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i A ) |-> Y ) ) ) )
40	32, 39	eqeq12d 2253	. . 3 |- ( w = A -> ( ( G gsumg ( k e. w |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i w ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i w ) |-> Y ) ) ) <-> ( G gsumg ( k e. A |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i A ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i A ) |-> Y ) ) ) ) )
41		gsummptfidmsplit.g	. . . . . 6 |- ( ph -> G e. CMnd )
42	41	cmnmndd 14201	. . . . 5 |- ( ph -> G e. Mnd )
43		gsummptfidmsplit.b	. . . . . 6 |- B = ( Base ` G )
44		eqid 2238	. . . . . 6 |- ( 0g ` G ) = ( 0g ` G )
45	43, 44	mndidcl 13802	. . . . 5 |- ( G e. Mnd -> ( 0g ` G ) e. B )
46		gsummptfidmsplit.p	. . . . . 6 |- .+ = ( +g ` G )
47	43, 46, 44	mndlid 13807	. . . . 5 |- ( ( G e. Mnd /\ ( 0g ` G ) e. B ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
48	42, 45, 47	syl2anc2 416	. . . 4 |- ( ph -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
49		in0 3557	. . . . . . . 8 |- ( C i^i (/) ) = (/)
50		mpteq1 4216	. . . . . . . 8 |- ( ( C i^i (/) ) = (/) -> ( k e. ( C i^i (/) ) |-> Y ) = ( k e. (/) |-> Y ) )
51	49, 50	ax-mp 5	. . . . . . 7 |- ( k e. ( C i^i (/) ) |-> Y ) = ( k e. (/) |-> Y )
52	51	oveq2i 6099	. . . . . 6 |- ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) = ( G gsumg ( k e. (/) |-> Y ) )
53		mpt0 5514	. . . . . . . 8 |- ( k e. (/) |-> Y ) = (/)
54	53	oveq2i 6099	. . . . . . 7 |- ( G gsumg ( k e. (/) |-> Y ) ) = ( G gsumg (/) )
55		gsum0cmn 14244	. . . . . . . 8 |- ( G e. CMnd -> ( G gsumg (/) ) = ( 0g ` G ) )
56	41, 55	syl 14	. . . . . . 7 |- ( ph -> ( G gsumg (/) ) = ( 0g ` G ) )
57	54, 56	eqtrid 2283	. . . . . 6 |- ( ph -> ( G gsumg ( k e. (/) |-> Y ) ) = ( 0g ` G ) )
58	52, 57	eqtrid 2283	. . . . 5 |- ( ph -> ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) = ( 0g ` G ) )
59		in0 3557	. . . . . . . 8 |- ( D i^i (/) ) = (/)
60		mpteq1 4216	. . . . . . . 8 |- ( ( D i^i (/) ) = (/) -> ( k e. ( D i^i (/) ) |-> Y ) = ( k e. (/) |-> Y ) )
61	59, 60	ax-mp 5	. . . . . . 7 |- ( k e. ( D i^i (/) ) |-> Y ) = ( k e. (/) |-> Y )
62	61	oveq2i 6099	. . . . . 6 |- ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) = ( G gsumg ( k e. (/) |-> Y ) )
63	62, 57	eqtrid 2283	. . . . 5 |- ( ph -> ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) = ( 0g ` G ) )
64	58, 63	oveq12d 6106	. . . 4 |- ( ph -> ( ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) ) = ( ( 0g ` G ) .+ ( 0g ` G ) ) )
65	48, 64, 57	3eqtr4rd 2282	. . 3 |- ( ph -> ( G gsumg ( k e. (/) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i (/) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i (/) ) |-> Y ) ) ) )
66	41	ad2antrr 492	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> G e. CMnd )
67		simplll 539	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> ph )
68		simprl 535	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y C_ A )
69	68	ad2antrr 492	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) /\ k e. y ) -> y C_ A )
70		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) /\ k e. y ) -> k e. y )
71	69, 70	sseldd 3249	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) /\ k e. y ) -> k e. A )
72		simprr 537	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. ( A \ y ) )
73	72	eldifad 3231	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. A )
74	73	ad2antrr 492	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) /\ k e. { z } ) -> z e. A )
75		elsni 3727	. . . . . . . . . . . . . . . . 17 |- ( k e. { z } -> k = z )
76	75	eleq1d 2307	. . . . . . . . . . . . . . . 16 |- ( k e. { z } -> ( k e. A <-> z e. A ) )
77	76	adantl 277	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) /\ k e. { z } ) -> ( k e. A <-> z e. A ) )
78	74, 77	mpbird 167	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) /\ k e. { z } ) -> k e. A )
79		elun 3370	. . . . . . . . . . . . . . 15 |- ( k e. ( y u. { z } ) <-> ( k e. y \/ k e. { z } ) )
80	79	bilani 387	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> ( k e. y \/ k e. { z } ) )
81	71, 78, 80	mpjaodan 810	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> k e. A )
82		gsummptfidmsplit.y	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. A ) -> Y e. B )
83	67, 81, 82	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> Y e. B )
84	83	fmpttd 5866	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. ( y u. { z } ) |-> Y ) : ( y u. { z } ) --> B )
85		simplr 533	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y e. Fin )
86	72	eldifbd 3232	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. y )
87	43, 46, 66, 84, 85, 73, 86	gsump1 14247	. . . . . . . . . 10 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( ( k e. ( y u. { z } ) |-> Y ) |` y ) ) .+ ( ( k e. ( y u. { z } ) |-> Y ) ` z ) ) )
88		ssun1 3392	. . . . . . . . . . . . . 14 |- y C_ ( y u. { z } )
89	88	a1i 9	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y C_ ( y u. { z } ) )
90	89	resmptd 5117	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( k e. ( y u. { z } ) |-> Y ) |` y ) = ( k e. y |-> Y ) )
91	90	oveq2d 6104	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( ( k e. ( y u. { z } ) |-> Y ) |` y ) ) = ( G gsumg ( k e. y |-> Y ) ) )
92		vsnid 3741	. . . . . . . . . . . . 13 |- z e. { z }
93		elun2 3397	. . . . . . . . . . . . 13 |- ( z e. { z } -> z e. ( y u. { z } ) )
94	92, 93	ax-mp 5	. . . . . . . . . . . 12 |- z e. ( y u. { z } )
95	82	ralrimiva 2623	. . . . . . . . . . . . . 14 |- ( ph -> A. k e. A Y e. B )
96	95	ad2antrr 492	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. k e. A Y e. B )
97		nfcsb1v 3180	. . . . . . . . . . . . . . 15 |- F/_ k [_ z / k ]_ Y
98	97	nfel1 2403	. . . . . . . . . . . . . 14 |- F/ k [_ z / k ]_ Y e. B
99		csbeq1a 3156	. . . . . . . . . . . . . . 15 |- ( k = z -> Y = [_ z / k ]_ Y )
100	99	eleq1d 2307	. . . . . . . . . . . . . 14 |- ( k = z -> ( Y e. B <-> [_ z / k ]_ Y e. B ) )
101	98, 100	rspc 2923	. . . . . . . . . . . . 13 |- ( z e. A -> ( A. k e. A Y e. B -> [_ z / k ]_ Y e. B ) )
102	73, 96, 101	sylc 62	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> [_ z / k ]_ Y e. B )
103		eqid 2238	. . . . . . . . . . . . 13 |- ( k e. ( y u. { z } ) |-> Y ) = ( k e. ( y u. { z } ) |-> Y )
104	103	fvmpts 5786	. . . . . . . . . . . 12 |- ( ( z e. ( y u. { z } ) /\ [_ z / k ]_ Y e. B ) -> ( ( k e. ( y u. { z } ) |-> Y ) ` z ) = [_ z / k ]_ Y )
105	94, 102, 104	sylancr 418	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( k e. ( y u. { z } ) |-> Y ) ` z ) = [_ z / k ]_ Y )
106	91, 105	oveq12d 6106	. . . . . . . . . 10 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( G gsumg ( ( k e. ( y u. { z } ) |-> Y ) |` y ) ) .+ ( ( k e. ( y u. { z } ) |-> Y ) ` z ) ) = ( ( G gsumg ( k e. y |-> Y ) ) .+ [_ z / k ]_ Y ) )
107	87, 106	eqtrd 2271	. . . . . . . . 9 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. y |-> Y ) ) .+ [_ z / k ]_ Y ) )
108	107	adantr 276	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. y |-> Y ) ) .+ [_ z / k ]_ Y ) )
109		simpr 110	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
110	109	oveq1d 6103	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( ( G gsumg ( k e. y |-> Y ) ) .+ [_ z / k ]_ Y ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) .+ [_ z / k ]_ Y ) )
111	66	adantr 276	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> G e. CMnd )
112		gsummptfidmsplit.a	. . . . . . . . . . . . 13 |- ( ph -> A e. Fin )
113	112	ad2antrr 492	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A e. Fin )
114		inss2 3452	. . . . . . . . . . . . 13 |- ( C i^i y ) C_ y
115	114, 68	sstrid 3259	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( C i^i y ) C_ A )
116		gsummptfidmsplit.i	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( C i^i D ) = (/) )
117	116	ad3antrrr 496	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> ( C i^i D ) = (/) )
118		ineqcom 3422	. . . . . . . . . . . . . . . . 17 |- ( ( C i^i D ) = (/) <-> ( D i^i C ) = (/) )
119	117, 118	sylib 122	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> ( D i^i C ) = (/) )
120		gsummptfidmsplit.u	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A = ( C u. D ) )
121	120	eleq2d 2308	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( q e. A <-> q e. ( C u. D ) ) )
122	121	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( q e. A <-> q e. ( C u. D ) ) )
123	122	biimpa 296	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> q e. ( C u. D ) )
124		elun 3370	. . . . . . . . . . . . . . . . 17 |- ( q e. ( C u. D ) <-> ( q e. C \/ q e. D ) )
125	123, 124	sylib 122	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> ( q e. C \/ q e. D ) )
126		orc 724	. . . . . . . . . . . . . . . . . . 19 |- ( q e. C -> ( q e. C \/ -. q e. C ) )
127		df-dc 847	. . . . . . . . . . . . . . . . . . 19 |- (DECID q e. C <-> ( q e. C \/ -. q e. C ) )
128	126, 127	sylibr 134	. . . . . . . . . . . . . . . . . 18 |- ( q e. C -> DECID q e. C )
129	128	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( ( D i^i C ) = (/) -> ( q e. C -> DECID q e. C ) )
130		disjel 3579	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( D i^i C ) = (/) /\ q e. D ) -> -. q e. C )
131	130	olcd 746	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( D i^i C ) = (/) /\ q e. D ) -> ( q e. C \/ -. q e. C ) )
132	131, 127	sylibr 134	. . . . . . . . . . . . . . . . . 18 |- ( ( ( D i^i C ) = (/) /\ q e. D ) -> DECID q e. C )
133	132	ex 115	. . . . . . . . . . . . . . . . 17 |- ( ( D i^i C ) = (/) -> ( q e. D -> DECID q e. C ) )
134	129, 133	jaod 729	. . . . . . . . . . . . . . . 16 |- ( ( D i^i C ) = (/) -> ( ( q e. C \/ q e. D ) -> DECID q e. C ) )
135	119, 125, 134	sylc 62	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID q e. C )
136		fissfi 7267	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ A /\ A e. Fin /\ y e. Fin ) -> A. q e. A DECID q e. y )
137	68, 113, 85, 136	syl3anc 1278	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. q e. A DECID q e. y )
138	137	r19.21bi 2638	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID q e. y )
139	135, 138	dcand 945	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID ( q e. C /\ q e. y ) )
140		elin 3412	. . . . . . . . . . . . . . 15 |- ( q e. ( C i^i y ) <-> ( q e. C /\ q e. y ) )
141	140	dcbii 852	. . . . . . . . . . . . . 14 |- (DECID q e. ( C i^i y ) <-> DECID ( q e. C /\ q e. y ) )
142	139, 141	sylibr 134	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID q e. ( C i^i y ) )
143	142	ralrimiva 2623	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. q e. A DECID q e. ( C i^i y ) )
144		ssfidc 7249	. . . . . . . . . . . 12 |- ( ( A e. Fin /\ ( C i^i y ) C_ A /\ A. q e. A DECID q e. ( C i^i y ) ) -> ( C i^i y ) e. Fin )
145	113, 115, 143, 144	syl3anc 1278	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( C i^i y ) e. Fin )
146		simplll 539	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( C i^i y ) ) -> ph )
147	115	sselda 3248	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( C i^i y ) ) -> k e. A )
148	146, 147, 82	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( C i^i y ) ) -> Y e. B )
149	148	fmpttd 5866	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. ( C i^i y ) |-> Y ) : ( C i^i y ) --> B )
150	43, 44, 66, 145, 149	gsumclfi 14249	. . . . . . . . . 10 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) e. B )
151	150	adantr 276	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) e. B )
152		inss2 3452	. . . . . . . . . . . . 13 |- ( D i^i y ) C_ y
153	152, 68	sstrid 3259	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( D i^i y ) C_ A )
154		disjel 3579	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C i^i D ) = (/) /\ q e. C ) -> -. q e. D )
155	154	olcd 746	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C i^i D ) = (/) /\ q e. C ) -> ( q e. D \/ -. q e. D ) )
156		df-dc 847	. . . . . . . . . . . . . . . . . . 19 |- (DECID q e. D <-> ( q e. D \/ -. q e. D ) )
157	155, 156	sylibr 134	. . . . . . . . . . . . . . . . . 18 |- ( ( ( C i^i D ) = (/) /\ q e. C ) -> DECID q e. D )
158	157	ex 115	. . . . . . . . . . . . . . . . 17 |- ( ( C i^i D ) = (/) -> ( q e. C -> DECID q e. D ) )
159		orc 724	. . . . . . . . . . . . . . . . . . 19 |- ( q e. D -> ( q e. D \/ -. q e. D ) )
160	159, 156	sylibr 134	. . . . . . . . . . . . . . . . . 18 |- ( q e. D -> DECID q e. D )
161	160	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( ( C i^i D ) = (/) -> ( q e. D -> DECID q e. D ) )
162	158, 161	jaod 729	. . . . . . . . . . . . . . . 16 |- ( ( C i^i D ) = (/) -> ( ( q e. C \/ q e. D ) -> DECID q e. D ) )
163	117, 125, 162	sylc 62	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID q e. D )
164	163, 138	dcand 945	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID ( q e. D /\ q e. y ) )
165		elin 3412	. . . . . . . . . . . . . . 15 |- ( q e. ( D i^i y ) <-> ( q e. D /\ q e. y ) )
166	165	dcbii 852	. . . . . . . . . . . . . 14 |- (DECID q e. ( D i^i y ) <-> DECID ( q e. D /\ q e. y ) )
167	164, 166	sylibr 134	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ q e. A ) -> DECID q e. ( D i^i y ) )
168	167	ralrimiva 2623	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. q e. A DECID q e. ( D i^i y ) )
169		ssfidc 7249	. . . . . . . . . . . 12 |- ( ( A e. Fin /\ ( D i^i y ) C_ A /\ A. q e. A DECID q e. ( D i^i y ) ) -> ( D i^i y ) e. Fin )
170	113, 153, 168, 169	syl3anc 1278	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( D i^i y ) e. Fin )
171		simplll 539	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( D i^i y ) ) -> ph )
172	153	sselda 3248	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( D i^i y ) ) -> k e. A )
173	171, 172, 82	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( D i^i y ) ) -> Y e. B )
174	173	fmpttd 5866	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. ( D i^i y ) |-> Y ) : ( D i^i y ) --> B )
175	43, 44, 66, 170, 174	gsumclfi 14249	. . . . . . . . . 10 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) e. B )
176	175	adantr 276	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) e. B )
177	102	adantr 276	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> [_ z / k ]_ Y e. B )
178	43, 46	cmn32 14197	. . . . . . . . 9 |- ( ( G e. CMnd /\ ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) e. B /\ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) e. B /\ [_ z / k ]_ Y e. B ) ) -> ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) .+ [_ z / k ]_ Y ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
179	111, 151, 176, 177, 178	syl13anc 1280	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) .+ [_ z / k ]_ Y ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
180	108, 110, 179	3eqtrd 2275	. . . . . . 7 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
181	180	adantlr 481	. . . . . 6 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
182	66	adantr 276	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> G e. CMnd )
183		simp-4l 547	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ k e. ( C i^i ( y u. { z } ) ) ) -> ph )
184		ssun1 3392	. . . . . . . . . . . . . . . 16 |- C C_ ( C u. D )
185	184, 120	sseqtrrid 3299	. . . . . . . . . . . . . . 15 |- ( ph -> C C_ A )
186	185	ad4antr 498	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ k e. ( C i^i ( y u. { z } ) ) ) -> C C_ A )
187		elinel1 3415	. . . . . . . . . . . . . . 15 |- ( k e. ( C i^i ( y u. { z } ) ) -> k e. C )
188	187	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ k e. ( C i^i ( y u. { z } ) ) ) -> k e. C )
189	186, 188	sseldd 3249	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ k e. ( C i^i ( y u. { z } ) ) ) -> k e. A )
190	183, 189, 82	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ k e. ( C i^i ( y u. { z } ) ) ) -> Y e. B )
191	190	fmpttd 5866	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) : ( C i^i ( y u. { z } ) ) --> B )
192		indi 3478	. . . . . . . . . . . . . 14 |- ( C i^i ( y u. { z } ) ) = ( ( C i^i y ) u. ( C i^i { z } ) )
193		snssi 3859	. . . . . . . . . . . . . . . 16 |- ( z e. C -> { z } C_ C )
194		dfss1 3435	. . . . . . . . . . . . . . . 16 |- ( { z } C_ C <-> ( C i^i { z } ) = { z } )
195	193, 194	sylib 122	. . . . . . . . . . . . . . 15 |- ( z e. C -> ( C i^i { z } ) = { z } )
196	195	uneq2d 3383	. . . . . . . . . . . . . 14 |- ( z e. C -> ( ( C i^i y ) u. ( C i^i { z } ) ) = ( ( C i^i y ) u. { z } ) )
197	192, 196	eqtrid 2283	. . . . . . . . . . . . 13 |- ( z e. C -> ( C i^i ( y u. { z } ) ) = ( ( C i^i y ) u. { z } ) )
198	197	feq2d 5524	. . . . . . . . . . . 12 |- ( z e. C -> ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) : ( C i^i ( y u. { z } ) ) --> B <-> ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) : ( ( C i^i y ) u. { z } ) --> B ) )
199	198	adantl 277	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) : ( C i^i ( y u. { z } ) ) --> B <-> ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) : ( ( C i^i y ) u. { z } ) --> B ) )
200	191, 199	mpbid 147	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) : ( ( C i^i y ) u. { z } ) --> B )
201	145	adantr 276	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( C i^i y ) e. Fin )
202		simpr 110	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> z e. C )
203		simpr 110	. . . . . . . . . . . . . 14 |- ( ( z e. C /\ z e. y ) -> z e. y )
204	203	con3i 641	. . . . . . . . . . . . 13 |- ( -. z e. y -> -. ( z e. C /\ z e. y ) )
205		elin 3412	. . . . . . . . . . . . 13 |- ( z e. ( C i^i y ) <-> ( z e. C /\ z e. y ) )
206	204, 205	sylnibr 688	. . . . . . . . . . . 12 |- ( -. z e. y -> -. z e. ( C i^i y ) )
207	86, 206	syl 14	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. ( C i^i y ) )
208	207	adantr 276	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> -. z e. ( C i^i y ) )
209	43, 46, 182, 200, 201, 202, 208	gsump1 14247	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) = ( ( G gsumg ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) |` ( C i^i y ) ) ) .+ ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ` z ) ) )
210		ssun1 3392	. . . . . . . . . . . . . . 15 |- ( C i^i y ) C_ ( ( C i^i y ) u. ( C i^i { z } ) )
211	210, 192	sseqtrri 3283	. . . . . . . . . . . . . 14 |- ( C i^i y ) C_ ( C i^i ( y u. { z } ) )
212	211	a1i 9	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( C i^i y ) C_ ( C i^i ( y u. { z } ) ) )
213	212	resmptd 5117	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) |` ( C i^i y ) ) = ( k e. ( C i^i y ) |-> Y ) )
214	213	oveq2d 6104	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) |` ( C i^i y ) ) ) = ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) )
215	214	adantr 276	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( G gsumg ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) |` ( C i^i y ) ) ) = ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) )
216		elin 3412	. . . . . . . . . . . 12 |- ( z e. ( C i^i ( y u. { z } ) ) <-> ( z e. C /\ z e. ( y u. { z } ) ) )
217	202, 94, 216	sylanblrc 420	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> z e. ( C i^i ( y u. { z } ) ) )
218	102	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> [_ z / k ]_ Y e. B )
219		eqid 2238	. . . . . . . . . . . 12 |- ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) = ( k e. ( C i^i ( y u. { z } ) ) |-> Y )
220	219	fvmpts 5786	. . . . . . . . . . 11 |- ( ( z e. ( C i^i ( y u. { z } ) ) /\ [_ z / k ]_ Y e. B ) -> ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ` z ) = [_ z / k ]_ Y )
221	217, 218, 220	syl2anc 415	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ` z ) = [_ z / k ]_ Y )
222	215, 221	oveq12d 6106	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( ( G gsumg ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) |` ( C i^i y ) ) ) .+ ( ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ` z ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) )
223	209, 222	eqtrd 2271	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) )
224	116	ad3antrrr 496	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( C i^i D ) = (/) )
225		disjel 3579	. . . . . . . . . . . 12 |- ( ( ( C i^i D ) = (/) /\ z e. C ) -> -. z e. D )
226	224, 202, 225	syl2anc 415	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> -. z e. D )
227		indi 3478	. . . . . . . . . . . 12 |- ( D i^i ( y u. { z } ) ) = ( ( D i^i y ) u. ( D i^i { z } ) )
228		disjsn 3771	. . . . . . . . . . . . . . 15 |- ( ( D i^i { z } ) = (/) <-> -. z e. D )
229	228	biimpri 133	. . . . . . . . . . . . . 14 |- ( -. z e. D -> ( D i^i { z } ) = (/) )
230	229	uneq2d 3383	. . . . . . . . . . . . 13 |- ( -. z e. D -> ( ( D i^i y ) u. ( D i^i { z } ) ) = ( ( D i^i y ) u. (/) ) )
231		un0 3556	. . . . . . . . . . . . 13 |- ( ( D i^i y ) u. (/) ) = ( D i^i y )
232	230, 231	eqtrdi 2287	. . . . . . . . . . . 12 |- ( -. z e. D -> ( ( D i^i y ) u. ( D i^i { z } ) ) = ( D i^i y ) )
233	227, 232	eqtrid 2283	. . . . . . . . . . 11 |- ( -. z e. D -> ( D i^i ( y u. { z } ) ) = ( D i^i y ) )
234	226, 233	syl 14	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( D i^i ( y u. { z } ) ) = ( D i^i y ) )
235	234	mpteq1d 4217	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) = ( k e. ( D i^i y ) |-> Y ) )
236	235	oveq2d 6104	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) = ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) )
237	223, 236	oveq12d 6106	. . . . . . 7 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
238	237	adantr 276	. . . . . 6 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
239	181, 238	eqtr4d 2274	. . . . 5 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) )
240	239	ex 115	. . . 4 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. C ) -> ( ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) ) )
241	180	adantlr 481	. . . . . 6 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
242	116, 118	sylib 122	. . . . . . . . . . . . . 14 |- ( ph -> ( D i^i C ) = (/) )
243	242	ad2antrr 492	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( D i^i C ) = (/) )
244		disjel 3579	. . . . . . . . . . . . 13 |- ( ( ( D i^i C ) = (/) /\ z e. D ) -> -. z e. C )
245	243, 244	sylan 283	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> -. z e. C )
246		disjsn 3771	. . . . . . . . . . . . . . . 16 |- ( ( C i^i { z } ) = (/) <-> -. z e. C )
247	246	biimpri 133	. . . . . . . . . . . . . . 15 |- ( -. z e. C -> ( C i^i { z } ) = (/) )
248	247	uneq2d 3383	. . . . . . . . . . . . . 14 |- ( -. z e. C -> ( ( C i^i y ) u. ( C i^i { z } ) ) = ( ( C i^i y ) u. (/) ) )
249		un0 3556	. . . . . . . . . . . . . 14 |- ( ( C i^i y ) u. (/) ) = ( C i^i y )
250	248, 249	eqtrdi 2287	. . . . . . . . . . . . 13 |- ( -. z e. C -> ( ( C i^i y ) u. ( C i^i { z } ) ) = ( C i^i y ) )
251	192, 250	eqtrid 2283	. . . . . . . . . . . 12 |- ( -. z e. C -> ( C i^i ( y u. { z } ) ) = ( C i^i y ) )
252	245, 251	syl 14	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( C i^i ( y u. { z } ) ) = ( C i^i y ) )
253	252	mpteq1d 4217	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) = ( k e. ( C i^i y ) |-> Y ) )
254	253	oveq2d 6104	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) = ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) )
255	66	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> G e. CMnd )
256		simp-4l 547	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ k e. ( D i^i ( y u. { z } ) ) ) -> ph )
257		ssun2 3393	. . . . . . . . . . . . . . . . 17 |- D C_ ( C u. D )
258	257, 120	sseqtrrid 3299	. . . . . . . . . . . . . . . 16 |- ( ph -> D C_ A )
259	258	ad4antr 498	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ k e. ( D i^i ( y u. { z } ) ) ) -> D C_ A )
260		elinel1 3415	. . . . . . . . . . . . . . . 16 |- ( k e. ( D i^i ( y u. { z } ) ) -> k e. D )
261	260	adantl 277	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ k e. ( D i^i ( y u. { z } ) ) ) -> k e. D )
262	259, 261	sseldd 3249	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ k e. ( D i^i ( y u. { z } ) ) ) -> k e. A )
263	256, 262, 82	syl2anc 415	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ k e. ( D i^i ( y u. { z } ) ) ) -> Y e. B )
264	263	fmpttd 5866	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) : ( D i^i ( y u. { z } ) ) --> B )
265		snssi 3859	. . . . . . . . . . . . . . . . 17 |- ( z e. D -> { z } C_ D )
266		dfss1 3435	. . . . . . . . . . . . . . . . 17 |- ( { z } C_ D <-> ( D i^i { z } ) = { z } )
267	265, 266	sylib 122	. . . . . . . . . . . . . . . 16 |- ( z e. D -> ( D i^i { z } ) = { z } )
268	267	uneq2d 3383	. . . . . . . . . . . . . . 15 |- ( z e. D -> ( ( D i^i y ) u. ( D i^i { z } ) ) = ( ( D i^i y ) u. { z } ) )
269	227, 268	eqtrid 2283	. . . . . . . . . . . . . 14 |- ( z e. D -> ( D i^i ( y u. { z } ) ) = ( ( D i^i y ) u. { z } ) )
270	269	feq2d 5524	. . . . . . . . . . . . 13 |- ( z e. D -> ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) : ( D i^i ( y u. { z } ) ) --> B <-> ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) : ( ( D i^i y ) u. { z } ) --> B ) )
271	270	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) : ( D i^i ( y u. { z } ) ) --> B <-> ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) : ( ( D i^i y ) u. { z } ) --> B ) )
272	264, 271	mpbid 147	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) : ( ( D i^i y ) u. { z } ) --> B )
273	170	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( D i^i y ) e. Fin )
274		simpr 110	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> z e. D )
275		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( z e. D /\ z e. y ) -> z e. y )
276	275	con3i 641	. . . . . . . . . . . . . 14 |- ( -. z e. y -> -. ( z e. D /\ z e. y ) )
277		elin 3412	. . . . . . . . . . . . . 14 |- ( z e. ( D i^i y ) <-> ( z e. D /\ z e. y ) )
278	276, 277	sylnibr 688	. . . . . . . . . . . . 13 |- ( -. z e. y -> -. z e. ( D i^i y ) )
279	86, 278	syl 14	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. ( D i^i y ) )
280	279	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> -. z e. ( D i^i y ) )
281	43, 46, 255, 272, 273, 274, 280	gsump1 14247	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) = ( ( G gsumg ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) |` ( D i^i y ) ) ) .+ ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ` z ) ) )
282		ssun1 3392	. . . . . . . . . . . . . . . 16 |- ( D i^i y ) C_ ( ( D i^i y ) u. ( D i^i { z } ) )
283	282, 227	sseqtrri 3283	. . . . . . . . . . . . . . 15 |- ( D i^i y ) C_ ( D i^i ( y u. { z } ) )
284	283	a1i 9	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( D i^i y ) C_ ( D i^i ( y u. { z } ) ) )
285	284	resmptd 5117	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) |` ( D i^i y ) ) = ( k e. ( D i^i y ) |-> Y ) )
286	285	oveq2d 6104	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( G gsumg ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) |` ( D i^i y ) ) ) = ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) )
287	286	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( G gsumg ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) |` ( D i^i y ) ) ) = ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) )
288		elin 3412	. . . . . . . . . . . . 13 |- ( z e. ( D i^i ( y u. { z } ) ) <-> ( z e. D /\ z e. ( y u. { z } ) ) )
289	274, 94, 288	sylanblrc 420	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> z e. ( D i^i ( y u. { z } ) ) )
290	102	adantr 276	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> [_ z / k ]_ Y e. B )
291		eqid 2238	. . . . . . . . . . . . 13 |- ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) = ( k e. ( D i^i ( y u. { z } ) ) |-> Y )
292	291	fvmpts 5786	. . . . . . . . . . . 12 |- ( ( z e. ( D i^i ( y u. { z } ) ) /\ [_ z / k ]_ Y e. B ) -> ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ` z ) = [_ z / k ]_ Y )
293	289, 290, 292	syl2anc 415	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ` z ) = [_ z / k ]_ Y )
294	287, 293	oveq12d 6106	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( G gsumg ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) |` ( D i^i y ) ) ) .+ ( ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ` z ) ) = ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) )
295	281, 294	eqtrd 2271	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) = ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) )
296	254, 295	oveq12d 6106	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) ) )
297	43, 46	cmncom 14195	. . . . . . . . . . . 12 |- ( ( G e. CMnd /\ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) e. B /\ [_ z / k ]_ Y e. B ) -> ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) = ( [_ z / k ]_ Y .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
298	66, 175, 102, 297	syl3anc 1278	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) = ( [_ z / k ]_ Y .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
299	298	oveq2d 6104	. . . . . . . . . 10 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( [_ z / k ]_ Y .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) )
300	42	ad2antrr 492	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> G e. Mnd )
301	43, 46	mndass 13796	. . . . . . . . . . 11 |- ( ( G e. Mnd /\ ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) e. B /\ [_ z / k ]_ Y e. B /\ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) e. B ) ) -> ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( [_ z / k ]_ Y .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) )
302	300, 150, 102, 175, 301	syl13anc 1280	. . . . . . . . . 10 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( [_ z / k ]_ Y .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) )
303	299, 302	eqtr4d 2274	. . . . . . . . 9 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
304	303	adantr 276	. . . . . . . 8 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
305	296, 304	eqtrd 2271	. . . . . . 7 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
306	305	adantr 276	. . . . . 6 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) = ( ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ [_ z / k ]_ Y ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) )
307	241, 306	eqtr4d 2274	. . . . 5 |- ( ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) /\ ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) )
308	307	ex 115	. . . 4 |- ( ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ z e. D ) -> ( ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) ) )
309	120	eleq2d 2308	. . . . . . 7 |- ( ph -> ( z e. A <-> z e. ( C u. D ) ) )
310	309	ad2antrr 492	. . . . . 6 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( z e. A <-> z e. ( C u. D ) ) )
311	73, 310	mpbid 147	. . . . 5 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. ( C u. D ) )
312		elun 3370	. . . . 5 |- ( z e. ( C u. D ) <-> ( z e. C \/ z e. D ) )
313	311, 312	sylib 122	. . . 4 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( z e. C \/ z e. D ) )
314	240, 308, 313	mpjaodan 810	. . 3 |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( G gsumg ( k e. y |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i y ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i y ) |-> Y ) ) ) -> ( G gsumg ( k e. ( y u. { z } ) |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i ( y u. { z } ) ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i ( y u. { z } ) ) |-> Y ) ) ) ) )
315	10, 20, 30, 40, 65, 314, 112	findcard2sd 7200	. 2 |- ( ph -> ( G gsumg ( k e. A |-> Y ) ) = ( ( G gsumg ( k e. ( C i^i A ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i A ) |-> Y ) ) ) )
316		df-ss 3233	. . . . . 6 |- ( C C_ A <-> ( C i^i A ) = C )
317	185, 316	sylib 122	. . . . 5 |- ( ph -> ( C i^i A ) = C )
318	317	mpteq1d 4217	. . . 4 |- ( ph -> ( k e. ( C i^i A ) |-> Y ) = ( k e. C |-> Y ) )
319	318	oveq2d 6104	. . 3 |- ( ph -> ( G gsumg ( k e. ( C i^i A ) |-> Y ) ) = ( G gsumg ( k e. C |-> Y ) ) )
320		df-ss 3233	. . . . . 6 |- ( D C_ A <-> ( D i^i A ) = D )
321	258, 320	sylib 122	. . . . 5 |- ( ph -> ( D i^i A ) = D )
322	321	mpteq1d 4217	. . . 4 |- ( ph -> ( k e. ( D i^i A ) |-> Y ) = ( k e. D |-> Y ) )
323	322	oveq2d 6104	. . 3 |- ( ph -> ( G gsumg ( k e. ( D i^i A ) |-> Y ) ) = ( G gsumg ( k e. D |-> Y ) ) )
324	319, 323	oveq12d 6106	. 2 |- ( ph -> ( ( G gsumg ( k e. ( C i^i A ) |-> Y ) ) .+ ( G gsumg ( k e. ( D i^i A ) |-> Y ) ) ) = ( ( G gsumg ( k e. C |-> Y ) ) .+ ( G gsumg ( k e. D |-> Y ) ) ) )
325	315, 324	eqtrd 2271	1 |- ( ph -> ( G gsumg ( k e. A |-> Y ) ) = ( ( G gsumg ( k e. C |-> Y ) ) .+ ( G gsumg ( k e. D |-> Y ) ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   A.wral 2528   [_csb 3147   \ cdif 3217   u. cun 3218   i^i cin 3219   C_ wss 3220   (/)c0 3520   {csn 3709   |-> cmpt 4193   |` cres 4778   -->wf 5376   ` cfv 5380  (class class class)co 6088   Fincfn 7026   Basecbs 13410   +g cplusg 13490   0gc0g 13669   Mndcmnd 13788  CMndccmn 14177   gsum_g cgsu 14240

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-mulrcl 8284  ax-addcom 8285  ax-mulcom 8286  ax-addass 8287  ax-mulass 8288  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-1rid 8292  ax-0id 8293  ax-rnegex 8294  ax-precex 8295  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-apti 8300  ax-pre-ltadd 8301  ax-pre-mulgt0 8302

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-1st 6378  df-2nd 6379  df-recs 6580  df-irdg 6645  df-frec 6666  df-1o 6691  df-oadd 6695  df-er 6811  df-en 7027  df-dom 7028  df-fin 7029  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-reap 8911  df-ap 8918  df-inn 9314  df-2 9372  df-n0 9575  df-z 9656  df-uz 9938  df-fz 10429  df-fzo 10567  df-seqfrec 10906  df-ihash 11237  df-ndx 13413  df-slot 13414  df-base 13416  df-plusg 13503  df-0g 13671  df-gzsum 13672  df-mgm 13735  df-sgrp 13776  df-mnd 13789  df-minusg 13868  df-mulg 13982  df-cmn 14179  df-gsumfi 14241

This theorem is used by:  gsummptfidmsplitres  14255  gsumunsnfd  14259