Theorem dpjidcl 15571

Description: The key property of projections: the sum of all the projections of A is A. (Contributed by Mario Carneiro, 26-Apr-2016.)

Hypotheses

Ref	Expression
dpjfval.1	|- ( ph -> G dom DProd S )
dpjfval.2	|- ( ph -> dom S = I )
dpjfval.p	|- P = ( GdProj S )
dpjidcl.3	|- ( ph -> A e. ( G DProd S ) )
dpjidcl.0	|- .0. = ( 0g ` G )
dpjidcl.w	|- W = { h e. X_ i e. I ( S ` i ) | ( `' h " ( _V \ { .0. } ) ) e. Fin }

Assertion

Ref	Expression
dpjidcl	|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )

Distinct variable groups:   x, h, .0.   h, i, G, x   P, h, x   ph, i, x   h, I, i, x   x, W   A, h, x   S, h, i, x

Allowed substitution hints:   ph( h)   A( i)   P( i)   W( h, i)   .0. ( i)

Proof of Theorem dpjidcl

Dummy variables k f are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dpjidcl.3	. . . 4 |- ( ph -> A e. ( G DProd S ) )
2		dpjfval.2	. . . . 5 |- ( ph -> dom S = I )
3		dpjidcl.0	. . . . . 6 |- .0. = ( 0g ` G )
4		dpjidcl.w	. . . . . 6 |- W = { h e. X_ i e. I ( S ` i ) | ( `' h " ( _V \ { .0. } ) ) e. Fin }
5	3, 4	eldprd 15517	. . . . 5 |- ( dom S = I -> ( A e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsumg f ) ) ) )
6	2, 5	syl 16	. . . 4 |- ( ph -> ( A e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsumg f ) ) ) )
7	1, 6	mpbid 202	. . 3 |- ( ph -> ( G dom DProd S /\ E. f e. W A = ( G gsumg f ) ) )
8	7	simprd 450	. 2 |- ( ph -> E. f e. W A = ( G gsumg f ) )
9		dpjfval.1	. . . . 5 |- ( ph -> G dom DProd S )
10	9	adantr 452	. . . 4 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> G dom DProd S )
11	2	adantr 452	. . . 4 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> dom S = I )
12	9	ad2antrr 707	. . . . . 6 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> G dom DProd S )
13	2	ad2antrr 707	. . . . . 6 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> dom S = I )
14		dpjfval.p	. . . . . 6 |- P = ( GdProj S )
15		simpr 448	. . . . . 6 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> x e. I )
16	12, 13, 14, 15	dpjf 15570	. . . . 5 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( P ` x ) : ( G DProd S ) --> ( S ` x ) )
17	1	ad2antrr 707	. . . . 5 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> A e. ( G DProd S ) )
18	16, 17	ffvelrnd 5830	. . . 4 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( P ` x ) ` A ) e. ( S ` x ) )
19		simprl 733	. . . . . 6 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> f e. W )
20	4, 10, 11, 19	dprdffi 15527	. . . . 5 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( `' f " ( _V \ { .0. } ) ) e. Fin )
21		eldifi 3429	. . . . . . . 8 |- ( x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) -> x e. I )
22		eqid 2404	. . . . . . . . . 10 |- ( proj 1 ` G ) = ( proj 1 ` G )
23	12, 13, 14, 22, 15	dpjval 15569	. . . . . . . . 9 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( P ` x ) = ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) )
24	23	fveq1d 5689	. . . . . . . 8 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( P ` x ) ` A ) = ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) )
25	21, 24	sylan2 461	. . . . . . 7 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( ( P ` x ) ` A ) = ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) )
26		simplrr 738	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> A = ( G gsumg f ) )
27		eqid 2404	. . . . . . . . . . 11 |- ( Base ` G ) = ( Base ` G )
28		eqid 2404	. . . . . . . . . . 11 |- (Cntz ` G ) = (Cntz ` G )
29		dprdgrp 15518	. . . . . . . . . . . . 13 |- ( G dom DProd S -> G e. Grp )
30		grpmnd 14772	. . . . . . . . . . . . 13 |- ( G e. Grp -> G e. Mnd )
31	10, 29, 30	3syl 19	. . . . . . . . . . . 12 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> G e. Mnd )
32	31	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> G e. Mnd )
33		reldmdprd 15513	. . . . . . . . . . . . . . 15 |- Rel dom DProd
34	33	brrelex2i 4878	. . . . . . . . . . . . . 14 |- ( G dom DProd S -> S e. _V )
35		dmexg 5089	. . . . . . . . . . . . . 14 |- ( S e. _V -> dom S e. _V )
36	10, 34, 35	3syl 19	. . . . . . . . . . . . 13 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> dom S e. _V )
37	11, 36	eqeltrrd 2479	. . . . . . . . . . . 12 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> I e. _V )
38	37	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> I e. _V )
39	4, 10, 11, 19, 27	dprdff 15525	. . . . . . . . . . . 12 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> f : I --> ( Base ` G ) )
40	39	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> f : I --> ( Base ` G ) )
41	19	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> f e. W )
42	4, 12, 13, 41, 28	dprdfcntz 15528	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ran f C_ ( (Cntz ` G ) ` ran f ) )
43	21, 42	sylan2 461	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ran f C_ ( (Cntz ` G ) ` ran f ) )
44		snssi 3902	. . . . . . . . . . . . 13 |- ( x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) -> { x } C_ ( I \ ( `' f " ( _V \ { .0. } ) ) ) )
45	44	adantl 453	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> { x } C_ ( I \ ( `' f " ( _V \ { .0. } ) ) ) )
46	45	difss2d 3437	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> { x } C_ I )
47		cnvimass 5183	. . . . . . . . . . . . . . 15 |- ( `' f " ( _V \ { .0. } ) ) C_ dom f
48		fdm 5554	. . . . . . . . . . . . . . . 16 |- ( f : I --> ( Base ` G ) -> dom f = I )
49	39, 48	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> dom f = I )
50	47, 49	syl5sseq 3356	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( `' f " ( _V \ { .0. } ) ) C_ I )
51	50	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( `' f " ( _V \ { .0. } ) ) C_ I )
52		ssconb 3440	. . . . . . . . . . . . 13 |- ( ( { x } C_ I /\ ( `' f " ( _V \ { .0. } ) ) C_ I ) -> ( { x } C_ ( I \ ( `' f " ( _V \ { .0. } ) ) ) <-> ( `' f " ( _V \ { .0. } ) ) C_ ( I \ { x } ) ) )
53	46, 51, 52	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( { x } C_ ( I \ ( `' f " ( _V \ { .0. } ) ) ) <-> ( `' f " ( _V \ { .0. } ) ) C_ ( I \ { x } ) ) )
54	45, 53	mpbid 202	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( `' f " ( _V \ { .0. } ) ) C_ ( I \ { x } ) )
55	20	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( `' f " ( _V \ { .0. } ) ) e. Fin )
56	27, 3, 28, 32, 38, 40, 43, 54, 55	gsumzres 15472	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( G gsumg ( f |` ( I \ { x } ) ) ) = ( G gsumg f ) )
57	26, 56	eqtr4d 2439	. . . . . . . . 9 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> A = ( G gsumg ( f |` ( I \ { x } ) ) ) )
58		eqid 2404	. . . . . . . . . . 11 |- { h e. X_ i e. ( I \ { x } ) ( ( S |` ( I \ { x } ) ) ` i ) | ( `' h " ( _V \ { .0. } ) ) e. Fin } = { h e. X_ i e. ( I \ { x } ) ( ( S |` ( I \ { x } ) ) ` i ) | ( `' h " ( _V \ { .0. } ) ) e. Fin }
59		difss 3434	. . . . . . . . . . . . . 14 |- ( I \ { x } ) C_ I
60	59	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( I \ { x } ) C_ I )
61	12, 13, 60	dprdres 15541	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G dom DProd ( S |` ( I \ { x } ) ) /\ ( G DProd ( S |` ( I \ { x } ) ) ) C_ ( G DProd S ) ) )
62	61	simpld 446	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> G dom DProd ( S |` ( I \ { x } ) ) )
63	12, 13	dprdf2 15520	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> S : I --> (SubGrp ` G ) )
64		fssres 5569	. . . . . . . . . . . . 13 |- ( ( S : I --> (SubGrp ` G ) /\ ( I \ { x } ) C_ I ) -> ( S |` ( I \ { x } ) ) : ( I \ { x } ) --> (SubGrp ` G ) )
65	63, 59, 64	sylancl 644	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( S |` ( I \ { x } ) ) : ( I \ { x } ) --> (SubGrp ` G ) )
66		fdm 5554	. . . . . . . . . . . 12 |- ( ( S |` ( I \ { x } ) ) : ( I \ { x } ) --> (SubGrp ` G ) -> dom ( S |` ( I \ { x } ) ) = ( I \ { x } ) )
67	65, 66	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> dom ( S |` ( I \ { x } ) ) = ( I \ { x } ) )
68	39	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> f : I --> ( Base ` G ) )
69	68	feqmptd 5738	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> f = ( k e. I |-> ( f ` k ) ) )
70	69	reseq1d 5104	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( f |` ( I \ { x } ) ) = ( ( k e. I |-> ( f ` k ) ) |` ( I \ { x } ) ) )
71		resmpt 5150	. . . . . . . . . . . . . 14 |- ( ( I \ { x } ) C_ I -> ( ( k e. I |-> ( f ` k ) ) |` ( I \ { x } ) ) = ( k e. ( I \ { x } ) |-> ( f ` k ) ) )
72	59, 71	ax-mp 8	. . . . . . . . . . . . 13 |- ( ( k e. I |-> ( f ` k ) ) |` ( I \ { x } ) ) = ( k e. ( I \ { x } ) |-> ( f ` k ) )
73	70, 72	syl6eq 2452	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( f |` ( I \ { x } ) ) = ( k e. ( I \ { x } ) |-> ( f ` k ) ) )
74		eldifi 3429	. . . . . . . . . . . . . . 15 |- ( k e. ( I \ { x } ) -> k e. I )
75	4, 12, 13, 41	dprdfcl 15526	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ k e. I ) -> ( f ` k ) e. ( S ` k ) )
76	74, 75	sylan2 461	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ k e. ( I \ { x } ) ) -> ( f ` k ) e. ( S ` k ) )
77		fvres 5704	. . . . . . . . . . . . . . 15 |- ( k e. ( I \ { x } ) -> ( ( S |` ( I \ { x } ) ) ` k ) = ( S ` k ) )
78	77	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ k e. ( I \ { x } ) ) -> ( ( S |` ( I \ { x } ) ) ` k ) = ( S ` k ) )
79	76, 78	eleqtrrd 2481	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ k e. ( I \ { x } ) ) -> ( f ` k ) e. ( ( S |` ( I \ { x } ) ) ` k ) )
80	20	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( `' f " ( _V \ { .0. } ) ) e. Fin )
81		ssdif 3442	. . . . . . . . . . . . . . . . . 18 |- ( ( I \ { x } ) C_ I -> ( ( I \ { x } ) \ ( `' f " ( _V \ { .0. } ) ) ) C_ ( I \ ( `' f " ( _V \ { .0. } ) ) ) )
82	59, 81	ax-mp 8	. . . . . . . . . . . . . . . . 17 |- ( ( I \ { x } ) \ ( `' f " ( _V \ { .0. } ) ) ) C_ ( I \ ( `' f " ( _V \ { .0. } ) ) )
83	82	sseli 3304	. . . . . . . . . . . . . . . 16 |- ( k e. ( ( I \ { x } ) \ ( `' f " ( _V \ { .0. } ) ) ) -> k e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) )
84		ssid 3327	. . . . . . . . . . . . . . . . . 18 |- ( `' f " ( _V \ { .0. } ) ) C_ ( `' f " ( _V \ { .0. } ) )
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( `' f " ( _V \ { .0. } ) ) C_ ( `' f " ( _V \ { .0. } ) ) )
86	68, 85	suppssr 5823	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ k e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( f ` k ) = .0. )
87	83, 86	sylan2 461	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ k e. ( ( I \ { x } ) \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( f ` k ) = .0. )
88	87	suppss2 6259	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( `' ( k e. ( I \ { x } ) |-> ( f ` k ) ) " ( _V \ { .0. } ) ) C_ ( `' f " ( _V \ { .0. } ) ) )
89		ssfi 7288	. . . . . . . . . . . . . 14 |- ( ( ( `' f " ( _V \ { .0. } ) ) e. Fin /\ ( `' ( k e. ( I \ { x } ) |-> ( f ` k ) ) " ( _V \ { .0. } ) ) C_ ( `' f " ( _V \ { .0. } ) ) ) -> ( `' ( k e. ( I \ { x } ) |-> ( f ` k ) ) " ( _V \ { .0. } ) ) e. Fin )
90	80, 88, 89	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( `' ( k e. ( I \ { x } ) |-> ( f ` k ) ) " ( _V \ { .0. } ) ) e. Fin )
91	58, 62, 67, 79, 90	dprdwd 15524	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( k e. ( I \ { x } ) |-> ( f ` k ) ) e. { h e. X_ i e. ( I \ { x } ) ( ( S |` ( I \ { x } ) ) ` i ) | ( `' h " ( _V \ { .0. } ) ) e. Fin } )
92	73, 91	eqeltrd 2478	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( f |` ( I \ { x } ) ) e. { h e. X_ i e. ( I \ { x } ) ( ( S |` ( I \ { x } ) ) ` i ) | ( `' h " ( _V \ { .0. } ) ) e. Fin } )
93	3, 58, 62, 67, 92	eldprdi 15531	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G gsumg ( f |` ( I \ { x } ) ) ) e. ( G DProd ( S |` ( I \ { x } ) ) ) )
94	21, 93	sylan2 461	. . . . . . . . 9 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( G gsumg ( f |` ( I \ { x } ) ) ) e. ( G DProd ( S |` ( I \ { x } ) ) ) )
95	57, 94	eqeltrd 2478	. . . . . . . 8 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> A e. ( G DProd ( S |` ( I \ { x } ) ) ) )
96		eqid 2404	. . . . . . . . . 10 |- ( +g ` G ) = ( +g ` G )
97		eqid 2404	. . . . . . . . . 10 |- ( LSSum ` G ) = ( LSSum ` G )
98	63, 15	ffvelrnd 5830	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( S ` x ) e. (SubGrp ` G ) )
99		dprdsubg 15537	. . . . . . . . . . 11 |- ( G dom DProd ( S |` ( I \ { x } ) ) -> ( G DProd ( S |` ( I \ { x } ) ) ) e. (SubGrp ` G ) )
100	62, 99	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G DProd ( S |` ( I \ { x } ) ) ) e. (SubGrp ` G ) )
101	12, 13, 15, 3	dpjdisj 15566	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( S ` x ) i^i ( G DProd ( S |` ( I \ { x } ) ) ) ) = { .0. } )
102	12, 13, 15, 28	dpjcntz 15565	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( S ` x ) C_ ( (Cntz ` G ) ` ( G DProd ( S |` ( I \ { x } ) ) ) ) )
103	96, 97, 3, 28, 98, 100, 101, 102, 22	pj1rid 15289	. . . . . . . . 9 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) /\ A e. ( G DProd ( S |` ( I \ { x } ) ) ) ) -> ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = .0. )
104	21, 103	sylanl2 633	. . . . . . . 8 |- ( ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) /\ A e. ( G DProd ( S |` ( I \ { x } ) ) ) ) -> ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = .0. )
105	95, 104	mpdan 650	. . . . . . 7 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = .0. )
106	25, 105	eqtrd 2436	. . . . . 6 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. ( I \ ( `' f " ( _V \ { .0. } ) ) ) ) -> ( ( P ` x ) ` A ) = .0. )
107	106	suppss2 6259	. . . . 5 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( `' ( x e. I |-> ( ( P ` x ) ` A ) ) " ( _V \ { .0. } ) ) C_ ( `' f " ( _V \ { .0. } ) ) )
108		ssfi 7288	. . . . 5 |- ( ( ( `' f " ( _V \ { .0. } ) ) e. Fin /\ ( `' ( x e. I |-> ( ( P ` x ) ` A ) ) " ( _V \ { .0. } ) ) C_ ( `' f " ( _V \ { .0. } ) ) ) -> ( `' ( x e. I |-> ( ( P ` x ) ` A ) ) " ( _V \ { .0. } ) ) e. Fin )
109	20, 107, 108	syl2anc 643	. . . 4 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( `' ( x e. I |-> ( ( P ` x ) ` A ) ) " ( _V \ { .0. } ) ) e. Fin )
110	4, 10, 11, 18, 109	dprdwd 15524	. . 3 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( x e. I |-> ( ( P ` x ) ` A ) ) e. W )
111		simprr 734	. . . 4 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> A = ( G gsumg f ) )
112	39	feqmptd 5738	. . . . . 6 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> f = ( x e. I |-> ( f ` x ) ) )
113		simplrr 738	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> A = ( G gsumg f ) )
114	12, 29, 30	3syl 19	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> G e. Mnd )
115	12, 34, 35	3syl 19	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> dom S e. _V )
116	13, 115	eqeltrrd 2479	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> I e. _V )
117	4, 12, 13, 41	dprdffi 15527	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( `' f " ( _V \ { .0. } ) ) e. Fin )
118		disjdif 3660	. . . . . . . . . . . . 13 |- ( { x } i^i ( I \ { x } ) ) = (/)
119	118	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( { x } i^i ( I \ { x } ) ) = (/) )
120		undif2 3664	. . . . . . . . . . . . 13 |- ( { x } u. ( I \ { x } ) ) = ( { x } u. I )
121	15	snssd 3903	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> { x } C_ I )
122		ssequn1 3477	. . . . . . . . . . . . . 14 |- ( { x } C_ I <-> ( { x } u. I ) = I )
123	121, 122	sylib 189	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( { x } u. I ) = I )
124	120, 123	syl5req 2449	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> I = ( { x } u. ( I \ { x } ) ) )
125	27, 3, 96, 28, 114, 116, 68, 42, 117, 119, 124	gsumzsplit 15484	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G gsumg f ) = ( ( G gsumg ( f |` { x } ) ) ( +g ` G ) ( G gsumg ( f |` ( I \ { x } ) ) ) ) )
126	68, 121	feqresmpt 5739	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( f |` { x } ) = ( k e. { x } |-> ( f ` k ) ) )
127	126	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G gsumg ( f |` { x } ) ) = ( G gsumg ( k e. { x } |-> ( f ` k ) ) ) )
128	68, 15	ffvelrnd 5830	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( f ` x ) e. ( Base ` G ) )
129		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( k = x -> ( f ` k ) = ( f ` x ) )
130	27, 129	gsumsn 15498	. . . . . . . . . . . . . 14 |- ( ( G e. Mnd /\ x e. I /\ ( f ` x ) e. ( Base ` G ) ) -> ( G gsumg ( k e. { x } |-> ( f ` k ) ) ) = ( f ` x ) )
131	114, 15, 128, 130	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G gsumg ( k e. { x } |-> ( f ` k ) ) ) = ( f ` x ) )
132	127, 131	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G gsumg ( f |` { x } ) ) = ( f ` x ) )
133	132	oveq1d 6055	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( G gsumg ( f |` { x } ) ) ( +g ` G ) ( G gsumg ( f |` ( I \ { x } ) ) ) ) = ( ( f ` x ) ( +g ` G ) ( G gsumg ( f |` ( I \ { x } ) ) ) ) )
134	113, 125, 133	3eqtrd 2440	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> A = ( ( f ` x ) ( +g ` G ) ( G gsumg ( f |` ( I \ { x } ) ) ) ) )
135	12, 13, 15, 97	dpjlsm 15567	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( G DProd S ) = ( ( S ` x ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) )
136	17, 135	eleqtrd 2480	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> A e. ( ( S ` x ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) )
137	4, 10, 11, 19	dprdfcl 15526	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( f ` x ) e. ( S ` x ) )
138	96, 97, 3, 28, 98, 100, 101, 102, 22, 136, 137, 93	pj1eq 15287	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( A = ( ( f ` x ) ( +g ` G ) ( G gsumg ( f |` ( I \ { x } ) ) ) ) <-> ( ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = ( f ` x ) /\ ( ( ( G DProd ( S |` ( I \ { x } ) ) ) ( proj 1 ` G ) ( S ` x ) ) ` A ) = ( G gsumg ( f |` ( I \ { x } ) ) ) ) ) )
139	134, 138	mpbid 202	. . . . . . . . 9 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = ( f ` x ) /\ ( ( ( G DProd ( S |` ( I \ { x } ) ) ) ( proj 1 ` G ) ( S ` x ) ) ` A ) = ( G gsumg ( f |` ( I \ { x } ) ) ) ) )
140	139	simpld 446	. . . . . . . 8 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( ( S ` x ) ( proj 1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = ( f ` x ) )
141	24, 140	eqtrd 2436	. . . . . . 7 |- ( ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) /\ x e. I ) -> ( ( P ` x ) ` A ) = ( f ` x ) )
142	141	mpteq2dva 4255	. . . . . 6 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> ( f ` x ) ) )
143	112, 142	eqtr4d 2439	. . . . 5 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> f = ( x e. I |-> ( ( P ` x ) ` A ) ) )
144	143	oveq2d 6056	. . . 4 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( G gsumg f ) = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) )
145	111, 144	eqtrd 2436	. . 3 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> A = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) )
146	110, 145	jca 519	. 2 |- ( ( ph /\ ( f e. W /\ A = ( G gsumg f ) ) ) -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )
147	8, 146	rexlimddv 2794	1 |- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   E.wrex 2667   {crab 2670   _Vcvv 2916   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   (/)c0 3588   {csn 3774   class class class wbr 4172   e. cmpt 4226   `'ccnv 4836   dom cdm 4837   ran crn 4838   |` cres 4839   "cima 4840   -->wf 5409   ` cfv 5413  (class class class)co 6040   X_cixp 7022   Fincfn 7068   Basecbs 13424   +g cplusg 13484   0gc0g 13678   gsum_g cgsu 13679   Mndcmnd 14639   Grpcgrp 14640  SubGrpcsubg 14893  Cntzccntz 15069   LSSumclsm 15223   proj 1cpj1 15224   DProd cdprd 15509  dProjcdpj 15510

This theorem is referenced by:  dpjeq  15572  dpjid  15573

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-tpos 6438  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-n0 10178  df-z 10239  df-uz 10445  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-0g 13682  df-gsum 13683  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-mhm 14693  df-submnd 14694  df-grp 14767  df-minusg 14768  df-sbg 14769  df-mulg 14770  df-subg 14896  df-ghm 14959  df-gim 15001  df-cntz 15071  df-oppg 15097  df-lsm 15225  df-pj1 15226  df-cmn 15369  df-dprd 15511  df-dpj 15512