gsumval3eu - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gsumval3eu		Structured version Unicode version

Theorem gsumval3eu 16374

Description: The group sum as defined in gsumval3a 16372 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.)

**Hypotheses**
Ref	Expression
gsumval3.b
gsumval3.0
gsumval3.p
gsumval3.z	Cntz
gsumval3.g
gsumval3.a
gsumval3.f
gsumval3.c
gsumval3a.t
gsumval3a.n
gsumval3a.s

**Assertion**
Ref	Expression
gsumval3eu	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem gsumval3eu Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumval3a.n	. . . . . 6
2	1	neneqd 2622	. . . . 5
3		gsumval3a.t	. . . . . . 7
4		fz1f1o 13183	. . . . . . 7 $\/$ $/\$
5	3, 4	syl 16	. . . . . 6 $\/$ $/\$
6	5	ord 377	. . . . 5 $/\$
7	2, 6	mpd 15	. . . 4 $/\$
8	7	simprd 460	. . 3
9		excom 1792	. . . 4 $/\$ $/\$
10		exancom 1643	. . . . . 6 $/\$ $/\$
11		fvex 5698	. . . . . . 7
12		biidd 237	. . . . . . 7
13	11, 12	ceqsexv 3006	. . . . . 6 $/\$
14	10, 13	bitri 249	. . . . 5 $/\$
15	14	exbii 1639	. . . 4 $/\$
16	9, 15	bitri 249	. . 3 $/\$
17	8, 16	sylibr 212	. 2 $/\$
18		eeanv 1936	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		an4 815	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		gsumval3.g	. . . . . . . . . . 11
21	20	adantr 462	. . . . . . . . . 10 $/\$ $/\$
22		gsumval3.b	. . . . . . . . . . . 12
23		gsumval3.p	. . . . . . . . . . . 12
24	22, 23	mndcl 15416	. . . . . . . . . . 11 $/\$ $/\$
25	24	3expb 1183	. . . . . . . . . 10 $/\$ $/\$
26	21, 25	sylan 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
27		gsumval3.c	. . . . . . . . . . . . 13
28	27	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
29	28	sselda 3353	. . . . . . . . . . 11 $/\$ $/\$ $/\$
30	29	adantrr 711	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
31		simprr 751	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
32		gsumval3.z	. . . . . . . . . . 11 Cntz
33	23, 32	cntzi 15840	. . . . . . . . . 10 $/\$
34	30, 31, 33	syl2anc 656	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	22, 23	mndass 15417	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	21, 35	sylan 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
37	7	simpld 456	. . . . . . . . . . 11
38	37	adantr 462	. . . . . . . . . 10 $/\$ $/\$
39		nnuz 10892	. . . . . . . . . 10
40	38, 39	syl6eleq 2531	. . . . . . . . 9 $/\$ $/\$
41		gsumval3.f	. . . . . . . . . . 11
42	41	adantr 462	. . . . . . . . . 10 $/\$ $/\$
43		frn 5562	. . . . . . . . . 10
44	42, 43	syl 16	. . . . . . . . 9 $/\$ $/\$
45		simprr 751	. . . . . . . . . . 11 $/\$ $/\$
46		f1ocnv 5650	. . . . . . . . . . 11
47	45, 46	syl 16	. . . . . . . . . 10 $/\$ $/\$
48		simprl 750	. . . . . . . . . 10 $/\$ $/\$
49		f1oco 5660	. . . . . . . . . 10 $/\$
50	47, 48, 49	syl2anc 656	. . . . . . . . 9 $/\$ $/\$
51		f1of 5638	. . . . . . . . . . . 12
52	45, 51	syl 16	. . . . . . . . . . 11 $/\$ $/\$
53		fvco3 5765	. . . . . . . . . . 11 $/\$
54	52, 53	sylan 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
55		ffn 5556	. . . . . . . . . . . . 13
56	42, 55	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
57	56	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
58		gsumval3a.s	. . . . . . . . . . . . . 14
59	58	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$
60		fss 5564	. . . . . . . . . . . . 13 $/\$
61	52, 59, 60	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$
62	61	ffvelrnda 5840	. . . . . . . . . . 11 $/\$ $/\$ $/\$
63		fnfvelrn 5837	. . . . . . . . . . 11 $/\$
64	57, 62, 63	syl2anc 656	. . . . . . . . . 10 $/\$ $/\$ $/\$
65	54, 64	eqeltrd 2515	. . . . . . . . 9 $/\$ $/\$ $/\$
66		f1of 5638	. . . . . . . . . . . . . . 15
67	48, 66	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
68		fvco3 5765	. . . . . . . . . . . . . 14 $/\$
69	67, 68	sylan 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
70	69	fveq2d 5692	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
71	45	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
72	67	ffvelrnda 5840	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73		f1ocnvfv2 5981	. . . . . . . . . . . . 13 $/\$
74	71, 72, 73	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75	70, 74	eqtr2d 2474	. . . . . . . . . . 11 $/\$ $/\$ $/\$
76	75	fveq2d 5692	. . . . . . . . . 10 $/\$ $/\$ $/\$
77		fvco3 5765	. . . . . . . . . . 11 $/\$
78	67, 77	sylan 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
79		f1of 5638	. . . . . . . . . . . . 13
80	50, 79	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
81	80	ffvelrnda 5840	. . . . . . . . . . 11 $/\$ $/\$ $/\$
82		fvco3 5765	. . . . . . . . . . . 12 $/\$
83	61, 82	sylan 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	81, 83	syldan 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	76, 78, 84	3eqtr4d 2483	. . . . . . . . 9 $/\$ $/\$ $/\$
86	26, 34, 36, 40, 44, 50, 65, 85	seqf1o 11843	. . . . . . . 8 $/\$ $/\$
87		eqeq12 2453	. . . . . . . 8 $/\$
88	86, 87	syl5ibrcom 222	. . . . . . 7 $/\$ $/\$ $/\$
89	88	expimpd 600	. . . . . 6 $/\$ $/\$ $/\$
90	19, 89	syl5bir 218	. . . . 5 $/\$ $/\$ $/\$
91	90	exlimdvv 1696	. . . 4 $/\$ $/\$ $/\$
92	18, 91	syl5bir 218	. . 3 $/\$ $/\$ $/\$
93	92	alrimivv 1691	. 2 $/\$ $/\$ $/\$
94		eqeq1 2447	. . . . . 6
95	94	anbi2d 698	. . . . 5 $/\$ $/\$
96	95	exbidv 1685	. . . 4 $/\$ $/\$
97		f1oeq1 5629	. . . . . 6
98		coeq2 4994	. . . . . . . . 9
99	98	seqeq3d 11810	. . . . . . . 8
100	99	fveq1d 5690	. . . . . . 7
101	100	eqeq2d 2452	. . . . . 6
102	97, 101	anbi12d 705	. . . . 5 $/\$ $/\$
103	102	cbvexv 1977	. . . 4 $/\$ $/\$
104	96, 103	syl6bb 261	. . 3 $/\$ $/\$
105	104	eu4 2323	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	17, 93, 105	sylanbrc 659	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 960

wal 1362

wceq 1364

wex 1591

wcel 1761

weu 2259

wne 2604

wss 3325

c0 3634

ccnv 4835

crn 4837

ccom 4840

wfn 5410

wf 5411

wf1o 5414

cfv 5415 (class class class)co 6090

cfn 7306

c1 9279

cn 10318

cuz 10857

cfz 11433

cseq 11802

chash 12099

cbs 14170

cplusg 14234

c0g 14374

cmnd 15405 Cntzccntz 15826

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-oadd 6920 df-er 7097 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-card 8105 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-nn 10319 df-n0 10576 df-z 10643 df-uz 10858 df-fz 11434 df-fzo 11545 df-seq 11803 df-hash 12100 df-mnd 15411 df-cntz 15828

This theorem is referenced by: gsumval3OLD 16375 gsumval3lem2 16377

W3C validator