Metamath Proof Explorer

Theorem sadfval

Description: Define the addition of two bit sequences, using df-had and df-cad bit operations. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Hypotheses sadval.a 
|- ( ph -> A C_ NN0 )
sadval.b 
|- ( ph -> B C_ NN0 )
sadval.c 
|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
Assertion sadfval 
|- ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )

Proof

Step Hyp Ref Expression
1 sadval.a 
 |-  ( ph -> A C_ NN0 )
2 sadval.b 
 |-  ( ph -> B C_ NN0 )
3 sadval.c 
 |-  C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( 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 simpl 
 |-  ( ( x = A /\ y = B ) -> x = A )
10 9 eleq2d 
 |-  ( ( x = A /\ y = B ) -> ( k e. x <-> k e. A ) )
11 simpr 
 |-  ( ( x = A /\ y = B ) -> y = B )
12 11 eleq2d 
 |-  ( ( x = A /\ y = B ) -> ( k e. y <-> k e. B ) )
13 simp1l 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> x = A )
14 13 eleq2d 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> ( m e. x <-> m e. A ) )
15 simp1r 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> y = B )
16 15 eleq2d 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> ( m e. y <-> m e. B ) )
17 biidd 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> ( (/) e. c <-> (/) e. c ) )
18 14 16 17 cadbi123d 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> ( cadd ( m e. x , m e. y , (/) e. c ) <-> cadd ( m e. A , m e. B , (/) e. c ) ) )
19 18 ifbid 
 |-  ( ( ( x = A /\ y = B ) /\ c e. 2o /\ m e. NN0 ) -> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) = if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) )
20 19 mpoeq3dva 
 |-  ( ( x = A /\ y = B ) -> ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) = ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) )
21 20 seqeq2d 
 |-  ( ( x = A /\ y = B ) -> seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) )
22 21 3 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = C )
23 22 fveq1d 
 |-  ( ( x = A /\ y = B ) -> ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = ( C ` k ) )
24 23 eleq2d 
 |-  ( ( x = A /\ y = B ) -> ( (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) <-> (/) e. ( C ` k ) ) )
25 10 12 24 hadbi123d 
 |-  ( ( x = A /\ y = B ) -> ( hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) <-> hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) ) )
26 25 rabbidv 
 |-  ( ( x = A /\ y = B ) -> { k e. NN0 | hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
27 df-sad 
 |-  sadd = ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )
28 4 rabex 
 |-  { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } e. _V
29 26 27 28 ovmpoa 
 |-  ( ( A e. ~P NN0 /\ B e. ~P NN0 ) -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
30 6 8 29 syl2anc 
 |-  ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )