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 ⊢φ→A⊆ℕ0
sadval.b ⊢φ→B⊆ℕ0
sadval.c ⊢C=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
Assertion sadfval ⊢φ→AsaddB=k∈ℕ0|haddk∈Ak∈B∅∈C⁡k

Proof

Step Hyp Ref Expression
1 sadval.a ⊢φ→A⊆ℕ0
2 sadval.b ⊢φ→B⊆ℕ0
3 sadval.c ⊢C=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
4 nn0ex ⊢ℕ0∈V
5 4 elpw2 ⊢A∈𝒫ℕ0↔A⊆ℕ0
6 1 5 sylibr ⊢φ→A∈𝒫ℕ0
7 4 elpw2 ⊢B∈𝒫ℕ0↔B⊆ℕ0
8 2 7 sylibr ⊢φ→B∈𝒫ℕ0
9 simpl ⊢x=A∧y=B→x=A
10 9 eleq2d ⊢x=A∧y=B→k∈x↔k∈A
11 simpr ⊢x=A∧y=B→y=B
12 11 eleq2d ⊢x=A∧y=B→k∈y↔k∈B
13 simp1l ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→x=A
14 13 eleq2d ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→m∈x↔m∈A
15 simp1r ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→y=B
16 15 eleq2d ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→m∈y↔m∈B
17 biidd ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→∅∈c↔∅∈c
18 14 16 17 cadbi123d ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→caddm∈xm∈y∅∈c↔caddm∈Am∈B∅∈c
19 18 ifbid ⊢x=A∧y=B∧c∈2𝑜∧m∈ℕ0→ifcaddm∈xm∈y∅∈c1𝑜∅=ifcaddm∈Am∈B∅∈c1𝑜∅
20 19 mpoeq3dva ⊢x=A∧y=B→c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅=c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅
21 20 seqeq2d ⊢x=A∧y=B→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
22 21 3 eqtr4di ⊢x=A∧y=B→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1=C
23 22 fveq1d ⊢x=A∧y=B→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k=C⁡k
24 23 eleq2d ⊢x=A∧y=B→∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k↔∅∈C⁡k
25 10 12 24 hadbi123d ⊢x=A∧y=B→haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k↔haddk∈Ak∈B∅∈C⁡k
26 25 rabbidv ⊢x=A∧y=B→k∈ℕ0|haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k=k∈ℕ0|haddk∈Ak∈B∅∈C⁡k
27 df-sad ⊢sadd=x∈𝒫ℕ0,y∈𝒫ℕ0⟼k∈ℕ0|haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
28 4 rabex ⊢k∈ℕ0|haddk∈Ak∈B∅∈C⁡k∈V
29 26 27 28 ovmpoa ⊢A∈𝒫ℕ0∧B∈𝒫ℕ0→AsaddB=k∈ℕ0|haddk∈Ak∈B∅∈C⁡k
30 6 8 29 syl2anc ⊢φ→AsaddB=k∈ℕ0|haddk∈Ak∈B∅∈C⁡k