Theorem gsumvsca2 26203

Description: Scalar product of a finite group sum for a left module over a semiring (Contributed by Thierry Arnoux, 16-Mar-2018.)

Hypotheses

Ref	Expression
gsumvsca.b	|- B = ( Base ` W )
gsumvsca.g	|- G = (Scalar ` W )
gsumvsca.z	|- .0. = ( 0g ` W )
gsumvsca.t	|- .x. = ( .s ` W )
gsumvsca.p	|- .+ = ( +g ` W )
gsumvsca.k	|- ( ph -> K C_ ( Base ` G ) )
gsumvsca.a	|- ( ph -> A e. Fin )
gsumvsca.w	|- ( ph -> W e. SLMod )
gsumvsca2.n	|- ( ph -> Q e. B )
gsumvsca2.c	|- ( ( ph /\ k e. A ) -> P e. K )

Assertion

Ref	Expression
gsumvsca2	|- ( ph -> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) )

Distinct variable groups:   .x. , k   A, k   k, W   ph, k   B, k   k, G   Q, k

Allowed substitution hints:   P( k)   .+ ( k)   K( k)   .0. ( k)

Proof of Theorem gsumvsca2

Dummy variables e a z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumvsca.a	. 2 |- ( ph -> A e. Fin )
2		ssid 3370	. . 3 |- A C_ A
3		sseq1 3372	. . . . . . 7 |- ( a = (/) -> ( a C_ A <-> (/) C_ A ) )
4	3	anbi2d 703	. . . . . 6 |- ( a = (/) -> ( ( ph /\ a C_ A ) <-> ( ph /\ (/) C_ A ) ) )
5		mpteq1 4367	. . . . . . . 8 |- ( a = (/) -> ( k e. a |-> ( P .x. Q ) ) = ( k e. (/) |-> ( P .x. Q ) ) )
6	5	oveq2d 6102	. . . . . . 7 |- ( a = (/) -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) )
7		mpteq1 4367	. . . . . . . . 9 |- ( a = (/) -> ( k e. a |-> P ) = ( k e. (/) |-> P ) )
8	7	oveq2d 6102	. . . . . . . 8 |- ( a = (/) -> ( G gsumg ( k e. a |-> P ) ) = ( G gsumg ( k e. (/) |-> P ) ) )
9	8	oveq1d 6101	. . . . . . 7 |- ( a = (/) -> ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) = ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) )
10	6, 9	eqeq12d 2452	. . . . . 6 |- ( a = (/) -> ( ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) <-> ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) ) )
11	4, 10	imbi12d 320	. . . . 5 |- ( a = (/) -> ( ( ( ph /\ a C_ A ) -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ (/) C_ A ) -> ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) ) ) )
12		sseq1 3372	. . . . . . 7 |- ( a = e -> ( a C_ A <-> e C_ A ) )
13	12	anbi2d 703	. . . . . 6 |- ( a = e -> ( ( ph /\ a C_ A ) <-> ( ph /\ e C_ A ) ) )
14		mpteq1 4367	. . . . . . . 8 |- ( a = e -> ( k e. a |-> ( P .x. Q ) ) = ( k e. e |-> ( P .x. Q ) ) )
15	14	oveq2d 6102	. . . . . . 7 |- ( a = e -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) )
16		mpteq1 4367	. . . . . . . . 9 |- ( a = e -> ( k e. a |-> P ) = ( k e. e |-> P ) )
17	16	oveq2d 6102	. . . . . . . 8 |- ( a = e -> ( G gsumg ( k e. a |-> P ) ) = ( G gsumg ( k e. e |-> P ) ) )
18	17	oveq1d 6101	. . . . . . 7 |- ( a = e -> ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) )
19	15, 18	eqeq12d 2452	. . . . . 6 |- ( a = e -> ( ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) <-> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) )
20	13, 19	imbi12d 320	. . . . 5 |- ( a = e -> ( ( ( ph /\ a C_ A ) -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ e C_ A ) -> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) ) )
21		sseq1 3372	. . . . . . 7 |- ( a = ( e u. { z } ) -> ( a C_ A <-> ( e u. { z } ) C_ A ) )
22	21	anbi2d 703	. . . . . 6 |- ( a = ( e u. { z } ) -> ( ( ph /\ a C_ A ) <-> ( ph /\ ( e u. { z } ) C_ A ) ) )
23		mpteq1 4367	. . . . . . . 8 |- ( a = ( e u. { z } ) -> ( k e. a |-> ( P .x. Q ) ) = ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) )
24	23	oveq2d 6102	. . . . . . 7 |- ( a = ( e u. { z } ) -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) )
25		mpteq1 4367	. . . . . . . . 9 |- ( a = ( e u. { z } ) -> ( k e. a |-> P ) = ( k e. ( e u. { z } ) |-> P ) )
26	25	oveq2d 6102	. . . . . . . 8 |- ( a = ( e u. { z } ) -> ( G gsumg ( k e. a |-> P ) ) = ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) )
27	26	oveq1d 6101	. . . . . . 7 |- ( a = ( e u. { z } ) -> ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) )
28	24, 27	eqeq12d 2452	. . . . . 6 |- ( a = ( e u. { z } ) -> ( ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) <-> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) )
29	22, 28	imbi12d 320	. . . . 5 |- ( a = ( e u. { z } ) -> ( ( ( ph /\ a C_ A ) -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
30		sseq1 3372	. . . . . . 7 |- ( a = A -> ( a C_ A <-> A C_ A ) )
31	30	anbi2d 703	. . . . . 6 |- ( a = A -> ( ( ph /\ a C_ A ) <-> ( ph /\ A C_ A ) ) )
32		mpteq1 4367	. . . . . . . 8 |- ( a = A -> ( k e. a |-> ( P .x. Q ) ) = ( k e. A |-> ( P .x. Q ) ) )
33	32	oveq2d 6102	. . . . . . 7 |- ( a = A -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) )
34		mpteq1 4367	. . . . . . . . 9 |- ( a = A -> ( k e. a |-> P ) = ( k e. A |-> P ) )
35	34	oveq2d 6102	. . . . . . . 8 |- ( a = A -> ( G gsumg ( k e. a |-> P ) ) = ( G gsumg ( k e. A |-> P ) ) )
36	35	oveq1d 6101	. . . . . . 7 |- ( a = A -> ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) )
37	33, 36	eqeq12d 2452	. . . . . 6 |- ( a = A -> ( ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) <-> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) ) )
38	31, 37	imbi12d 320	. . . . 5 |- ( a = A -> ( ( ( ph /\ a C_ A ) -> ( W gsumg ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ A C_ A ) -> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) ) ) )
39		gsumvsca.w	. . . . . . . . 9 |- ( ph -> W e. SLMod )
40		gsumvsca2.n	. . . . . . . . 9 |- ( ph -> Q e. B )
41		gsumvsca.b	. . . . . . . . . 10 |- B = ( Base ` W )
42		gsumvsca.g	. . . . . . . . . 10 |- G = (Scalar ` W )
43		gsumvsca.t	. . . . . . . . . 10 |- .x. = ( .s ` W )
44		eqid 2438	. . . . . . . . . 10 |- ( 0g ` G ) = ( 0g ` G )
45		gsumvsca.z	. . . . . . . . . 10 |- .0. = ( 0g ` W )
46	41, 42, 43, 44, 45	slmd0vs 26191	. . . . . . . . 9 |- ( ( W e. SLMod /\ Q e. B ) -> ( ( 0g ` G ) .x. Q ) = .0. )
47	39, 40, 46	syl2anc 661	. . . . . . . 8 |- ( ph -> ( ( 0g ` G ) .x. Q ) = .0. )
48		eqcom 2440	. . . . . . . 8 |- ( .0. = ( ( 0g ` G ) .x. Q ) <-> ( ( 0g ` G ) .x. Q ) = .0. )
49	47, 48	sylibr 212	. . . . . . 7 |- ( ph -> .0. = ( ( 0g ` G ) .x. Q ) )
50		mpt0 5533	. . . . . . . . . 10 |- ( k e. (/) |-> ( P .x. Q ) ) = (/)
51	50	oveq2i 6097	. . . . . . . . 9 |- ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = ( W gsumg (/) )
52	45	gsum0 15501	. . . . . . . . 9 |- ( W gsumg (/) ) = .0.
53	51, 52	eqtri 2458	. . . . . . . 8 |- ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = .0.
54		mpt0 5533	. . . . . . . . . . 11 |- ( k e. (/) |-> P ) = (/)
55	54	oveq2i 6097	. . . . . . . . . 10 |- ( G gsumg ( k e. (/) |-> P ) ) = ( G gsumg (/) )
56	44	gsum0 15501	. . . . . . . . . 10 |- ( G gsumg (/) ) = ( 0g ` G )
57	55, 56	eqtri 2458	. . . . . . . . 9 |- ( G gsumg ( k e. (/) |-> P ) ) = ( 0g ` G )
58	57	oveq1i 6096	. . . . . . . 8 |- ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) = ( ( 0g ` G ) .x. Q )
59	53, 58	eqeq12i 2451	. . . . . . 7 |- ( ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) <-> .0. = ( ( 0g ` G ) .x. Q ) )
60	49, 59	sylibr 212	. . . . . 6 |- ( ph -> ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) )
61	60	adantr 465	. . . . 5 |- ( ( ph /\ (/) C_ A ) -> ( W gsumg ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. (/) |-> P ) ) .x. Q ) )
62		ssun1 3514	. . . . . . . . 9 |- e C_ ( e u. { z } )
63		sstr2 3358	. . . . . . . . 9 |- ( e C_ ( e u. { z } ) -> ( ( e u. { z } ) C_ A -> e C_ A ) )
64	62, 63	ax-mp 5	. . . . . . . 8 |- ( ( e u. { z } ) C_ A -> e C_ A )
65	64	anim2i 569	. . . . . . 7 |- ( ( ph /\ ( e u. { z } ) C_ A ) -> ( ph /\ e C_ A ) )
66	65	imim1i 58	. . . . . 6 |- ( ( ( ph /\ e C_ A ) -> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) )
67	39	ad2antrl 727	. . . . . . . . . . . 12 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> W e. SLMod )
68		eqid 2438	. . . . . . . . . . . . 13 |- ( Base ` G ) = ( Base ` G )
69	42	slmdsrg 26174	. . . . . . . . . . . . . 14 |- ( W e. SLMod -> G e. SRing )
70		srgcmn 16598	. . . . . . . . . . . . . 14 |- ( G e. SRing -> G e. CMnd )
71	67, 69, 70	3syl 20	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> G e. CMnd )
72		vex 2970	. . . . . . . . . . . . . 14 |- e e. _V
73	72	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e e. _V )
74		simplrl 759	. . . . . . . . . . . . . . 15 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> ph )
75		simprr 756	. . . . . . . . . . . . . . . . 17 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( e u. { z } ) C_ A )
76	62, 75	syl5ss 3362	. . . . . . . . . . . . . . . 16 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e C_ A )
77	76	sselda 3351	. . . . . . . . . . . . . . 15 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> k e. A )
78		gsumvsca.k	. . . . . . . . . . . . . . . . 17 |- ( ph -> K C_ ( Base ` G ) )
79	78	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> K C_ ( Base ` G ) )
80		gsumvsca2.c	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> P e. K )
81	79, 80	sseldd 3352	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. A ) -> P e. ( Base ` G ) )
82	74, 77, 81	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> P e. ( Base ` G ) )
83		eqid 2438	. . . . . . . . . . . . . 14 |- ( k e. e |-> P ) = ( k e. e |-> P )
84	82, 83	fmptd 5862	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( k e. e |-> P ) : e --> ( Base ` G ) )
85		simpll 753	. . . . . . . . . . . . . 14 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e e. Fin )
86	85, 84	fisuppfi 7620	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( `' ( k e. e |-> P ) " ( _V \ { ( 0g ` G ) } ) ) e. Fin )
87	68, 44, 71, 73, 84, 86	gsumclOLD 16391	. . . . . . . . . . . 12 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( G gsumg ( k e. e |-> P ) ) e. ( Base ` G ) )
88		ssun2 3515	. . . . . . . . . . . . . . 15 |- { z } C_ ( e u. { z } )
89	88, 75	syl5ss 3362	. . . . . . . . . . . . . 14 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> { z } C_ A )
90		vex 2970	. . . . . . . . . . . . . . 15 |- z e. _V
91	90	snss 3994	. . . . . . . . . . . . . 14 |- ( z e. A <-> { z } C_ A )
92	89, 91	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> z e. A )
93	81	ralrimiva 2794	. . . . . . . . . . . . . 14 |- ( ph -> A. k e. A P e. ( Base ` G ) )
94	93	ad2antrl 727	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> A. k e. A P e. ( Base ` G ) )
95		rspcsbela 3700	. . . . . . . . . . . . 13 |- ( ( z e. A /\ A. k e. A P e. ( Base ` G ) ) -> [_ z / k ]_ P e. ( Base ` G ) )
96	92, 94, 95	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> [_ z / k ]_ P e. ( Base ` G ) )
97	40	ad2antrl 727	. . . . . . . . . . . 12 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> Q e. B )
98		gsumvsca.p	. . . . . . . . . . . . 13 |- .+ = ( +g ` W )
99		eqid 2438	. . . . . . . . . . . . 13 |- ( +g ` G ) = ( +g ` G )
100	41, 98, 42, 43, 68, 99	slmdvsdir 26183	. . . . . . . . . . . 12 |- ( ( W e. SLMod /\ ( ( G gsumg ( k e. e |-> P ) ) e. ( Base ` G ) /\ [_ z / k ]_ P e. ( Base ` G ) /\ Q e. B ) ) -> ( ( ( G gsumg ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) = ( ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
101	67, 87, 96, 97, 100	syl13anc 1220	. . . . . . . . . . 11 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( ( ( G gsumg ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) = ( ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
102	101	adantr 465	. . . . . . . . . 10 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ( G gsumg ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) = ( ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
103		nfcsb1v 3299	. . . . . . . . . . . . 13 |- F/_ k [_ z / k ]_ P
104	90	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> z e. _V )
105		simplr 754	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> -. z e. e )
106		csbeq1a 3292	. . . . . . . . . . . . 13 |- ( k = z -> P = [_ z / k ]_ P )
107	103, 68, 99, 71, 85, 82, 104, 105, 96, 106	gsumunsnf 26196	. . . . . . . . . . . 12 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) = ( ( G gsumg ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) )
108	107	oveq1d 6101	. . . . . . . . . . 11 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) = ( ( ( G gsumg ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) )
109	108	adantr 465	. . . . . . . . . 10 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) = ( ( ( G gsumg ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) )
110		nfcv 2574	. . . . . . . . . . . . . 14 |- F/_ k .x.
111		nfcv 2574	. . . . . . . . . . . . . 14 |- F/_ k Q
112	103, 110, 111	nfov 6109	. . . . . . . . . . . . 13 |- F/_ k ( [_ z / k ]_ P .x. Q )
113		slmdcmn 26172	. . . . . . . . . . . . . 14 |- ( W e. SLMod -> W e. CMnd )
114	67, 113	syl 16	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> W e. CMnd )
115	74, 39	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> W e. SLMod )
116	74, 40	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> Q e. B )
117	41, 42, 43, 68	slmdvscl 26181	. . . . . . . . . . . . . 14 |- ( ( W e. SLMod /\ P e. ( Base ` G ) /\ Q e. B ) -> ( P .x. Q ) e. B )
118	115, 82, 116, 117	syl3anc 1218	. . . . . . . . . . . . 13 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> ( P .x. Q ) e. B )
119	41, 42, 43, 68	slmdvscl 26181	. . . . . . . . . . . . . 14 |- ( ( W e. SLMod /\ [_ z / k ]_ P e. ( Base ` G ) /\ Q e. B ) -> ( [_ z / k ]_ P .x. Q ) e. B )
120	67, 96, 97, 119	syl3anc 1218	. . . . . . . . . . . . 13 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( [_ z / k ]_ P .x. Q ) e. B )
121	106	oveq1d 6101	. . . . . . . . . . . . 13 |- ( k = z -> ( P .x. Q ) = ( [_ z / k ]_ P .x. Q ) )
122	112, 41, 98, 114, 85, 118, 104, 105, 120, 121	gsumunsnf 26196	. . . . . . . . . . . 12 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) .+ ( [_ z / k ]_ P .x. Q ) ) )
123	122	adantr 465	. . . . . . . . . . 11 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) .+ ( [_ z / k ]_ P .x. Q ) ) )
124		simpr 461	. . . . . . . . . . . 12 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) )
125	124	oveq1d 6101	. . . . . . . . . . 11 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) .+ ( [_ z / k ]_ P .x. Q ) ) = ( ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
126	123, 125	eqtrd 2470	. . . . . . . . . 10 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
127	102, 109, 126	3eqtr4rd 2481	. . . . . . . . 9 |- ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) )
128	127	ex 434	. . . . . . . 8 |- ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) )
129	128	ex 434	. . . . . . 7 |- ( ( e e. Fin /\ -. z e. e ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
130	129	a2d 26	. . . . . 6 |- ( ( e e. Fin /\ -. z e. e ) -> ( ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
131	66, 130	syl5 32	. . . . 5 |- ( ( e e. Fin /\ -. z e. e ) -> ( ( ( ph /\ e C_ A ) -> ( W gsumg ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsumg ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
132	11, 20, 29, 38, 61, 131	findcard2s 7545	. . . 4 |- ( A e. Fin -> ( ( ph /\ A C_ A ) -> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) ) )
133	132	imp 429	. . 3 |- ( ( A e. Fin /\ ( ph /\ A C_ A ) ) -> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) )
134	2, 133	mpanr2 684	. 2 |- ( ( A e. Fin /\ ph ) -> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) )
135	1, 134	mpancom 669	1 |- ( ph -> ( W gsumg ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsumg ( k e. A |-> P ) ) .x. Q ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2710   _Vcvv 2967   [_csb 3283   \ cdif 3320   u. cun 3321   C_ wss 3323   (/)c0 3632   {csn 3872   e. cmpt 4345   ` cfv 5413  (class class class)co 6086   Fincfn 7302   Basecbs 14166   +g cplusg 14230  Scalarcsca 14233   .scvsca 14234   0gc0g 14370   gsum_g cgsu 14371  CMndccmn 16268  SRingcsrg 16595  SLModcslmd 26167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-iin 4169  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  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-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-n0 10572  df-z 10639  df-uz 10854  df-fz 11430  df-fzo 11541  df-seq 11799  df-hash 12096  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-0g 14372  df-gsum 14373  df-mre 14516  df-mrc 14517  df-acs 14519  df-mnd 15407  df-submnd 15457  df-mulg 15539  df-cntz 15826  df-cmn 16270  df-srg 16596  df-slmd 26168

This theorem is referenced by: (None)