Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadfval Structured version   Visualization version   GIF version

 Description: Define the addition of two bit sequences, using df-had 1595 and df-cad 1609 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.)
Hypotheses
Ref Expression
sadval.c 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
Assertion
Ref Expression
Distinct variable groups:   𝑘,𝑐,𝑚,𝑛   𝐴,𝑐,𝑘,𝑚   𝐵,𝑐,𝑘,𝑚   𝐶,𝑘   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sadval.a . . 3 (𝜑𝐴 ⊆ ℕ0)
2 nn0ex 11895 . . . 4 0 ∈ V
32elpw2 5215 . . 3 (𝐴 ∈ 𝒫 ℕ0𝐴 ⊆ ℕ0)
41, 3sylibr 237 . 2 (𝜑𝐴 ∈ 𝒫 ℕ0)
5 sadval.b . . 3 (𝜑𝐵 ⊆ ℕ0)
62elpw2 5215 . . 3 (𝐵 ∈ 𝒫 ℕ0𝐵 ⊆ ℕ0)
75, 6sylibr 237 . 2 (𝜑𝐵 ∈ 𝒫 ℕ0)
8 simpl 486 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝐴)
98eleq2d 2878 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑘𝑥𝑘𝐴))
10 simpr 488 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑦 = 𝐵)
1110eleq2d 2878 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑘𝑦𝑘𝐵))
12 simp1l 1194 . . . . . . . . . . . . 13 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → 𝑥 = 𝐴)
1312eleq2d 2878 . . . . . . . . . . . 12 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → (𝑚𝑥𝑚𝐴))
14 simp1r 1195 . . . . . . . . . . . . 13 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → 𝑦 = 𝐵)
1514eleq2d 2878 . . . . . . . . . . . 12 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → (𝑚𝑦𝑚𝐵))
16 biidd 265 . . . . . . . . . . . 12 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → (∅ ∈ 𝑐 ↔ ∅ ∈ 𝑐))
1713, 15, 16cadbi123d 1612 . . . . . . . . . . 11 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → (cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐) ↔ cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐)))
1817ifbid 4450 . . . . . . . . . 10 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2o𝑚 ∈ ℕ0) → if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅) = if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅))
1918mpoeq3dva 7214 . . . . . . . . 9 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)) = (𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)))
2019seqeq2d 13375 . . . . . . . 8 ((𝑥 = 𝐴𝑦 = 𝐵) → seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))))
21 sadval.c . . . . . . . 8 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
2220, 21eqtr4di 2854 . . . . . . 7 ((𝑥 = 𝐴𝑦 = 𝐵) → seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = 𝐶)
2322fveq1d 6651 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = (𝐶𝑘))
2423eleq2d 2878 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) ↔ ∅ ∈ (𝐶𝑘)))
259, 11, 24hadbi123d 1596 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)) ↔ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))))
2625rabbidv 3430 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))} = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})
27 df-sad 15794 . . 3 sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
282rabex 5202 . . 3 {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))} ∈ V
2926, 27, 28ovmpoa 7288 . 2 ((𝐴 ∈ 𝒫 ℕ0𝐵 ∈ 𝒫 ℕ0) → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})
304, 7, 29syl2anc 587 1 (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})