Metamath Proof Explorer

Theorem smupf

Description: The sequence of partial sums of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses smuval.a 
|- ( ph -> A C_ NN0 )
smuval.b 
|- ( ph -> B C_ NN0 )
smuval.p 
|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
Assertion smupf 
|- ( ph -> P : NN0 --> ~P NN0 )

Proof

Step Hyp Ref Expression
1 smuval.a 
 |-  ( ph -> A C_ NN0 )
2 smuval.b 
 |-  ( ph -> B C_ NN0 )
3 smuval.p 
 |-  P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 0nn0 
 |-  0 e. NN0
5 iftrue 
 |-  ( n = 0 -> if ( n = 0 , (/) , ( n - 1 ) ) = (/) )
6 eqid 
 |-  ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) = ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
7 0ex 
 |-  (/) e. _V
8 5 6 7 fvmpt 
 |-  ( 0 e. NN0 -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/) )
9 4 8 mp1i 
 |-  ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/) )
10 0elpw 
 |-  (/) e. ~P NN0
11 9 10 eqeltrdi 
 |-  ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) e. ~P NN0 )
12 df-ov 
 |-  ( x ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) y ) = ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ` <. x , y >. )
13 elpwi 
 |-  ( p e. ~P NN0 -> p C_ NN0 )
14 13 adantr 
 |-  ( ( p e. ~P NN0 /\ m e. NN0 ) -> p C_ NN0 )
15 ssrab2 
 |-  { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } C_ NN0
16 sadcl 
 |-  ( ( p C_ NN0 /\ { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } C_ NN0 ) -> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) C_ NN0 )
17 14 15 16 sylancl 
 |-  ( ( p e. ~P NN0 /\ m e. NN0 ) -> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) C_ NN0 )
18 nn0ex 
 |-  NN0 e. _V
19 18 elpw2 
 |-  ( ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) e. ~P NN0 <-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) C_ NN0 )
20 17 19 sylibr 
 |-  ( ( p e. ~P NN0 /\ m e. NN0 ) -> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) e. ~P NN0 )
21 20 rgen2 
 |-  A. p e. ~P NN0 A. m e. NN0 ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) e. ~P NN0
22 eqid 
 |-  ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) = ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) )
23 22 fmpo 
 |-  ( A. p e. ~P NN0 A. m e. NN0 ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) e. ~P NN0 <-> ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) : ( ~P NN0 X. NN0 ) --> ~P NN0 )
24 21 23 mpbi 
 |-  ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) : ( ~P NN0 X. NN0 ) --> ~P NN0
25 24 10 f0cli 
 |-  ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ` <. x , y >. ) e. ~P NN0
26 12 25 eqeltri 
 |-  ( x ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) y ) e. ~P NN0
27 26 a1i 
 |-  ( ( ph /\ ( x e. ~P NN0 /\ y e. _V ) ) -> ( x ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) y ) e. ~P NN0 )
28 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
29 0zd 
 |-  ( ph -> 0 e. ZZ )
30 fvexd 
 |-  ( ( ph /\ x e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` x ) e. _V )
31 11 27 28 29 30 seqf2 
 |-  ( ph -> seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) : NN0 --> ~P NN0 )
32 3 feq1i 
 |-  ( P : NN0 --> ~P NN0 <-> seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) : NN0 --> ~P NN0 )
33 31 32 sylibr 
 |-  ( ph -> P : NN0 --> ~P NN0 )