Metamath Proof Explorer

Theorem smufval

Description: The multiplication of two bit sequences as repeated sequence addition. (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 smufval 
|- ( ph -> ( A smul B ) = { k e. NN0 | k e. ( P ` ( k + 1 ) ) } )

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 nn0ex 
 |-  NN0 e. _V
5 4 elpw2 
 |-  ( A e. ~P NN0 <-> A C_ NN0 )
6 1 5 sylibr 
 |-  ( ph -> A e. ~P NN0 )
7 4 elpw2 
 |-  ( B e. ~P NN0 <-> B C_ NN0 )
8 2 7 sylibr 
 |-  ( ph -> B e. ~P NN0 )
9 simp1l 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> x = A )
10 9 eleq2d 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> ( m e. x <-> m e. A ) )
11 simp1r 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> y = B )
12 11 eleq2d 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> ( ( n - m ) e. y <-> ( n - m ) e. B ) )
13 10 12 anbi12d 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> ( ( m e. x /\ ( n - m ) e. y ) <-> ( m e. A /\ ( n - m ) e. B ) ) )
14 13 rabbidv 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } = { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } )
15 14 oveq2d 
 |-  ( ( ( x = A /\ y = B ) /\ p e. ~P NN0 /\ m e. NN0 ) -> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) = ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) )
16 15 mpoeq3dva 
 |-  ( ( x = A /\ y = B ) -> ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) = ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) )
17 16 seqeq2d 
 |-  ( ( x = A /\ y = B ) -> seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = 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 ) ) ) ) )
18 17 3 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = P )
19 18 fveq1d 
 |-  ( ( x = A /\ y = B ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) )
20 19 eleq2d 
 |-  ( ( x = A /\ y = B ) -> ( k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) <-> k e. ( P ` ( k + 1 ) ) ) )
21 20 rabbidv 
 |-  ( ( x = A /\ y = B ) -> { k e. NN0 | k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) } = { k e. NN0 | k e. ( P ` ( k + 1 ) ) } )
22 df-smu 
 |-  smul = ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) } )
23 4 rabex 
 |-  { k e. NN0 | k e. ( P ` ( k + 1 ) ) } e. _V
24 21 22 23 ovmpoa 
 |-  ( ( A e. ~P NN0 /\ B e. ~P NN0 ) -> ( A smul B ) = { k e. NN0 | k e. ( P ` ( k + 1 ) ) } )
25 6 8 24 syl2anc 
 |-  ( ph -> ( A smul B ) = { k e. NN0 | k e. ( P ` ( k + 1 ) ) } )