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

Theorem seqf1o 12148
Description: Rearrange a sum via an arbitrary bijection on . (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
Hypotheses
Ref Expression
seqf1o.1
seqf1o.2
seqf1o.3
seqf1o.4
seqf1o.5
seqf1o.6
seqf1o.7
seqf1o.8
Assertion
Ref Expression
seqf1o
Distinct variable groups:   , , , ,   , , , ,   ,M, , ,   , , , ,   ,N, , ,   , , , ,   S, , , ,   , , , ,   ,

Proof of Theorem seqf1o
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqf1o.6 . . 3
2 seqf1o.7 . . . 4
3 eqid 2457 . . . 4
42, 3fmptd 6055 . . 3
5 seqf1o.4 . . . . 5
6 oveq2 6304 . . . . . . . . . . 11
7 f1oeq23 5815 . . . . . . . . . . 11
86, 6, 7syl2anc 661 . . . . . . . . . 10
96feq2d 5723 . . . . . . . . . 10
108, 9anbi12d 710 . . . . . . . . 9
11 fveq2 5871 . . . . . . . . . 10
12 fveq2 5871 . . . . . . . . . 10
1311, 12eqeq12d 2479 . . . . . . . . 9
1410, 13imbi12d 320 . . . . . . . 8
15142albidv 1715 . . . . . . 7
1615imbi2d 316 . . . . . 6
17 oveq2 6304 . . . . . . . . . . 11
18 f1oeq23 5815 . . . . . . . . . . 11
1917, 17, 18syl2anc 661 . . . . . . . . . 10
2017feq2d 5723 . . . . . . . . . 10
2119, 20anbi12d 710 . . . . . . . . 9
22 fveq2 5871 . . . . . . . . . 10
23 fveq2 5871 . . . . . . . . . 10
2422, 23eqeq12d 2479 . . . . . . . . 9
2521, 24imbi12d 320 . . . . . . . 8
26252albidv 1715 . . . . . . 7
2726imbi2d 316 . . . . . 6
28 oveq2 6304 . . . . . . . . . . 11
29 f1oeq23 5815 . . . . . . . . . . 11
3028, 28, 29syl2anc 661 . . . . . . . . . 10
3128feq2d 5723 . . . . . . . . . 10
3230, 31anbi12d 710 . . . . . . . . 9
33 fveq2 5871 . . . . . . . . . 10
34 fveq2 5871 . . . . . . . . . 10
3533, 34eqeq12d 2479 . . . . . . . . 9
3632, 35imbi12d 320 . . . . . . . 8
37362albidv 1715 . . . . . . 7
3837imbi2d 316 . . . . . 6
39 oveq2 6304 . . . . . . . . . . 11
40 f1oeq23 5815 . . . . . . . . . . 11
4139, 39, 40syl2anc 661 . . . . . . . . . 10
4239feq2d 5723 . . . . . . . . . 10
4341, 42anbi12d 710 . . . . . . . . 9
44 fveq2 5871 . . . . . . . . . 10
45 fveq2 5871 . . . . . . . . . 10
4644, 45eqeq12d 2479 . . . . . . . . 9
4743, 46imbi12d 320 . . . . . . . 8
48472albidv 1715 . . . . . . 7
4948imbi2d 316 . . . . . 6
50 f1of 5821 . . . . . . . . . . . . 13
5150adantr 465 . . . . . . . . . . . 12
52 elfz3 11725 . . . . . . . . . . . 12
53 fvco3 5950 . . . . . . . . . . . 12
5451, 52, 53syl2anr 478 . . . . . . . . . . 11
55 ffvelrn 6029 . . . . . . . . . . . . . . 15
5650, 52, 55syl2anr 478 . . . . . . . . . . . . . 14
57 fzsn 11754 . . . . . . . . . . . . . . . . 17
5857eleq2d 2527 . . . . . . . . . . . . . . . 16
59 elsni 4054 . . . . . . . . . . . . . . . 16
6058, 59syl6bi 228 . . . . . . . . . . . . . . 15
6160imp 429 . . . . . . . . . . . . . 14
6256, 61syldan 470 . . . . . . . . . . . . 13
6362adantrr 716 . . . . . . . . . . . 12
6463fveq2d 5875 . . . . . . . . . . 11
6554, 64eqtrd 2498 . . . . . . . . . 10
66 seq1 12120 . . . . . . . . . . 11
6766adantr 465 . . . . . . . . . 10
68 seq1 12120 . . . . . . . . . . 11
6968adantr 465 . . . . . . . . . 10
7065, 67, 693eqtr4d 2508 . . . . . . . . 9
7170ex 434 . . . . . . . 8
7271alrimivv 1720 . . . . . . 7
7372a1d 25 . . . . . 6
74 f1oeq1 5812 . . . . . . . . . . . 12
75 feq1 5718 . . . . . . . . . . . 12
7674, 75bi2anan9r 874 . . . . . . . . . . 11
77 coeq1 5165 . . . . . . . . . . . . . . 15
78 coeq2 5166 . . . . . . . . . . . . . . 15
7977, 78sylan9eq 2518 . . . . . . . . . . . . . 14
8079seqeq3d 12115 . . . . . . . . . . . . 13
8180fveq1d 5873 . . . . . . . . . . . 12
82 simpl 457 . . . . . . . . . . . . . 14
8382seqeq3d 12115 . . . . . . . . . . . . 13
8483fveq1d 5873 . . . . . . . . . . . 12
8581, 84eqeq12d 2479 . . . . . . . . . . 11
8676, 85imbi12d 320 . . . . . . . . . 10
8786cbval2v 2030 . . . . . . . . 9
88 simplll 759 . . . . . . . . . . . . . . 15
89 seqf1o.1 . . . . . . . . . . . . . . 15
9088, 89sylan 471 . . . . . . . . . . . . . 14
91 seqf1o.2 . . . . . . . . . . . . . . 15
9288, 91sylan 471 . . . . . . . . . . . . . 14
93 seqf1o.3 . . . . . . . . . . . . . . 15
9488, 93sylan 471 . . . . . . . . . . . . . 14
95 simpllr 760 . . . . . . . . . . . . . 14
96 seqf1o.5 . . . . . . . . . . . . . . 15
9788, 96syl 16 . . . . . . . . . . . . . 14
98 simprl 756 . . . . . . . . . . . . . 14
99 simprr 757 . . . . . . . . . . . . . 14
100 eqid 2457 . . . . . . . . . . . . . 14
101 eqid 2457 . . . . . . . . . . . . . 14
102 simplr 755 . . . . . . . . . . . . . . 15
103102, 87sylib 196 . . . . . . . . . . . . . 14
10490, 92, 94, 95, 97, 98, 99, 100, 101, 103seqf1olem2 12147 . . . . . . . . . . . . 13
105104exp31 604 . . . . . . . . . . . 12
10687, 105syl5bir 218 . . . . . . . . . . 11
107106alrimdv 1721 . . . . . . . . . 10
108107alrimdv 1721 . . . . . . . . 9
10987, 108syl5bi 217