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

 Description: The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.)
Assertion
Ref Expression

Dummy variables 𝑘 𝑐 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hadcoma 1529 . . . 4 (hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)) ↔ hadd(𝑘𝐵, 𝑘𝐴, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)))
21a1i 11 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)) ↔ hadd(𝑘𝐵, 𝑘𝐴, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))))
32rabbidv 3164 . 2 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))} = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐵, 𝑘𝐴, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
4 simpl 472 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → 𝐴 ⊆ ℕ0)
5 simpr 476 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → 𝐵 ⊆ ℕ0)
6 eqid 2610 . . 3 seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
74, 5, 6sadfval 15012 . 2 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
8 cadcoma 1542 . . . . . . 7 (cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐) ↔ cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐))
98a1i 11 . . . . . 6 ((𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → (cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐) ↔ cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐)))
109ifbid 4058 . . . . 5 ((𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅) = if(cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐), 1𝑜, ∅))
1110mpt2eq3ia 6618 . . . 4 (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)) = (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐), 1𝑜, ∅))
12 seqeq2 12667 . . . 4 ((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)) = (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐), 1𝑜, ∅)) → seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))))
1311, 12ax-mp 5 . . 3 seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐵, 𝑚𝐴, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
145, 4, 13sadfval 15012 . 2 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐵 sadd 𝐴) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐵, 𝑘𝐴, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
153, 7, 143eqtr4d 2654 1 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴))