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 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
Assertion sadfval ⊢ φ → A sadd B = k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ φ → A ⊆ ℕ 0
2 sadval.b ⊢ φ → B ⊆ ℕ 0
3 sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 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 → cadd m ∈ x m ∈ y ∅ ∈ c ↔ cadd m ∈ A m ∈ B ∅ ∈ c
19 18 ifbid ⊢ x = A ∧ y = B ∧ c ∈ 2 𝑜 ∧ m ∈ ℕ 0 → if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ = if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅
20 19 mpoeq3dva ⊢ x = A ∧ y = B → c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ = c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅
21 20 seqeq2d ⊢ x = A ∧ y = B → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
22 21 3 eqtr4di ⊢ x = A ∧ y = B → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = C
23 22 fveq1d ⊢ x = A ∧ y = B → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k = C ⁡ k
24 23 eleq2d ⊢ x = A ∧ y = B → ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k ↔ ∅ ∈ C ⁡ k
25 10 12 24 hadbi123d ⊢ x = A ∧ y = B → hadd k ∈ x k ∈ y ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k ↔ hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k
26 25 rabbidv ⊢ x = A ∧ y = B → k ∈ ℕ 0 | hadd k ∈ x k ∈ y ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k = k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k
27 df-sad ⊢ sadd = x ∈ 𝒫 ℕ 0 , y ∈ 𝒫 ℕ 0 ⟼ k ∈ ℕ 0 | hadd k ∈ x k ∈ y ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ x m ∈ y ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
28 4 rabex ⊢ k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k ∈ V
29 26 27 28 ovmpoa ⊢ A ∈ 𝒫 ℕ 0 ∧ B ∈ 𝒫 ℕ 0 → A sadd B = k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k
30 6 8 29 syl2anc ⊢ φ → A sadd B = k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k