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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	sadval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	sadval.c	⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
Assertion	sadfval	⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		sadval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		sadval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		sadval.c	⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		nn0ex	⊢ ℕ0 ∈ V
5	4	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℕ0 ↔ 𝐴 ⊆ ℕ0 )
6	1 5	sylibr	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ℕ0 )
7	4	elpw2	⊢ ( 𝐵 ∈ 𝒫 ℕ0 ↔ 𝐵 ⊆ ℕ0 )
8	2 7	sylibr	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ℕ0 )
9		simpl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 = 𝐴 )
10	9	eleq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑘 ∈ 𝑥 ↔ 𝑘 ∈ 𝐴 ) )
11		simpr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
12	11	eleq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑘 ∈ 𝑦 ↔ 𝑘 ∈ 𝐵 ) )
13		simp1l	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → 𝑥 = 𝐴 )
14	13	eleq2d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 ∈ 𝑥 ↔ 𝑚 ∈ 𝐴 ) )
15		simp1r	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → 𝑦 = 𝐵 )
16	15	eleq2d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 ∈ 𝑦 ↔ 𝑚 ∈ 𝐵 ) )
17		biidd	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → ( ∅ ∈ 𝑐 ↔ ∅ ∈ 𝑐 ) )
18	14 16 17	cadbi123d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) ↔ cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) ) )
19	18	ifbid	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) = if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) )
20	19	mpoeq3dva	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) = ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) )
21	20	seqeq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) )
22	21 3	syl6eqr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = 𝐶 )
23	22	fveq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) )
24	23	eleq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ↔ ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) )
25	10 12 24	hadbi123d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) ↔ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) ) )
26	25	rabbidv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )
27		df-sad	⊢ sadd = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )
28	4	rabex	⊢ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } ∈ V
29	26 27 28	ovmpoa	⊢ ( ( 𝐴 ∈ 𝒫 ℕ0 ∧ 𝐵 ∈ 𝒫 ℕ0 ) → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )
30	6 8 29	syl2anc	⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )