Theorem sadadd2lem2 16375

Description: The core of the proof of sadadd2 16385. The intuitive justification for this is that cadd is true if at least two arguments are true, and hadd is true if an odd number of arguments are true, so altogether the result is 𝑛 · 𝐴 where 𝑛 is the number of true arguments, which is equivalently obtained by adding together one 𝐴 for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016.)

Assertion

Ref	Expression
sadadd2lem2	⊢ (𝐴 ∈ ℂ → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))

Proof of Theorem sadadd2lem2

Step	Hyp	Ref	Expression
1		0cn 11122	. . . . . . . . 9 ⊢ 0 ∈ ℂ
2		ifcl 4523	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜓, 𝐴, 0) ∈ ℂ)
3	1, 2	mpan2 691	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ)
4	3	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
5		simpll 766	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ)
6	4, 5, 5	add12d 11358	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
7	5, 4, 5	addassd 11152	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
8	6, 7	eqtr4d 2772	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
9		pm5.501 366	. . . . . . . . 9 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
10	9	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓)))
11	10	bicomd 223	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑 ↔ 𝜓) ↔ 𝜓))
12	11	ifbid 4501	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ↔ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
13		animorrl 982	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑 ∨ 𝜓))
14		iftrue 4483	. . . . . . . 8 ⊢ ((𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
15	13, 14	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
16	5	2timesd 12382	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴))
17	15, 16	eqtrd 2769	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴))
18	12, 17	oveq12d 7374	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)))
19		iftrue 4483	. . . . . . . 8 ⊢ (𝜑 → if(𝜑, 𝐴, 0) = 𝐴)
20	19	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
21	20	oveq1d 7371	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
22	21	oveq1d 7371	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
23	8, 18, 22	3eqtr4d 2779	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
24		iffalse 4486	. . . . . . . . 9 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 0) = 0)
25	24	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
26	25	oveq1d 7371	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
27	3	ad2antrr 726	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
28	27	addlidd 11332	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
29	26, 28	eqtrd 2769	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
30	29	oveq1d 7371	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴))
31		2cnd 12221	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
32		id 22	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
33	31, 32	mulcld 11150	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
34	33	addlidd 11332	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (2 · 𝐴))
35		2times 12274	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
36	34, 35	eqtrd 2769	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
37	36	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
38		iftrue 4483	. . . . . . . . . 10 ⊢ (𝜓 → if(𝜓, 0, 𝐴) = 0)
39	38	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0)
40		iftrue 4483	. . . . . . . . . 10 ⊢ (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
41	40	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
42	39, 41	oveq12d 7374	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴)))
43		iftrue 4483	. . . . . . . . . 10 ⊢ (𝜓 → if(𝜓, 𝐴, 0) = 𝐴)
44	43	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴)
45	44	oveq1d 7371	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴))
46	37, 42, 45	3eqtr4d 2779	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
47		simpl 482	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 𝐴 ∈ ℂ)
48		0cnd 11123	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 0 ∈ ℂ)
49	47, 48	addcomd 11333	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (𝐴 + 0) = (0 + 𝐴))
50		iffalse 4486	. . . . . . . . . 10 ⊢ (¬ 𝜓 → if(𝜓, 0, 𝐴) = 𝐴)
51	50	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 0, 𝐴) = 𝐴)
52		iffalse 4486	. . . . . . . . . 10 ⊢ (¬ 𝜓 → if(𝜓, (2 · 𝐴), 0) = 0)
53	52	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = 0)
54	51, 53	oveq12d 7374	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0))
55		iffalse 4486	. . . . . . . . . 10 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 0) = 0)
56	55	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 𝐴, 0) = 0)
57	56	oveq1d 7371	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴))
58	49, 54, 57	3eqtr4d 2779	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
59	46, 58	pm2.61dan 812	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
60	59	ad2antrr 726	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
61		ifnot 4530	. . . . . . 7 ⊢ if(¬ 𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴)
62		nbn2 370	. . . . . . . . 9 ⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
63	62	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
64	63	ifbid 4501	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0))
65	61, 64	eqtr3id 2783	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ↔ 𝜓), 𝐴, 0))
66		biorf 936	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))
67	66	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑 ∨ 𝜓)))
68	67	ifbid 4501	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))
69	65, 68	oveq12d 7374	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)))
70	30, 60, 69	3eqtr2rd 2776	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
71	23, 70	pm2.61dan 812	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
72		hadrot 1602	. . . . . . 7 ⊢ (hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒))
73		had1 1604	. . . . . . 7 ⊢ (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ↔ 𝜓)))
74	72, 73	bitr3id 285	. . . . . 6 ⊢ (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓)))
75	74	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓)))
76	75	ifbid 4501	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0))
77		cad1 1618	. . . . . 6 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓)))
78	77	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓)))
79	78	ifbid 4501	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))
80	76, 79	oveq12d 7374	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)))
81		iftrue 4483	. . . . 5 ⊢ (𝜒 → if(𝜒, 𝐴, 0) = 𝐴)
82	81	adantl 481	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴)
83	82	oveq2d 7372	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
84	71, 80, 83	3eqtr4d 2779	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
85	19	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
86	85	oveq1d 7371	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
87	44	oveq2d 7372	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴))
88	37, 42, 87	3eqtr4d 2779	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
89	53, 56	eqtr4d 2772	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0))
90	51, 89	oveq12d 7374	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
91	88, 90	pm2.61dan 812	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
92	91	ad2antrr 726	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
93	9	adantl 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓)))
94	93	notbid 318	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑 ↔ 𝜓)))
95		df-xor 1513	. . . . . . . . 9 ⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
96	94, 95	bitr4di 289	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑 ⊻ 𝜓)))
97	96	ifbid 4501	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0))
98	61, 97	eqtr3id 2783	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ⊻ 𝜓), 𝐴, 0))
99		ibar 528	. . . . . . . 8 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
100	99	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ∧ 𝜓)))
101	100	ifbid 4501	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))
102	98, 101	oveq12d 7374	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)))
103	86, 92, 102	3eqtr2rd 2776	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
104		simplll 774	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ)
105		0cnd 11123	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ)
106	104, 105	ifclda 4513	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
107		0cnd 11123	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → 0 ∈ ℂ)
108	106, 107	addcomd 11333	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 𝐴, 0) + 0) = (0 + if(𝜓, 𝐴, 0)))
109	62	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
110	109	con1bid 355	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ (𝜑 ↔ 𝜓) ↔ 𝜓))
111	95, 110	bitrid 283	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ((𝜑 ⊻ 𝜓) ↔ 𝜓))
112	111	ifbid 4501	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑 ⊻ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
113		simpr 484	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ 𝜑)
114	113	intnanrd 489	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ (𝜑 ∧ 𝜓))
115		iffalse 4486	. . . . . . 7 ⊢ (¬ (𝜑 ∧ 𝜓) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0)
116	114, 115	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0)
117	112, 116	oveq12d 7374	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0))
118	24	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
119	118	oveq1d 7371	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
120	108, 117, 119	3eqtr4d 2779	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
121	103, 120	pm2.61dan 812	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
122		had0 1605	. . . . . . 7 ⊢ (¬ 𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ⊻ 𝜓)))
123	72, 122	bitr3id 285	. . . . . 6 ⊢ (¬ 𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓)))
124	123	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓)))
125	124	ifbid 4501	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0))
126		cad0 1619	. . . . . 6 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓)))
127	126	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓)))
128	127	ifbid 4501	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))
129	125, 128	oveq12d 7374	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)))
130		iffalse 4486	. . . . 5 ⊢ (¬ 𝜒 → if(𝜒, 𝐴, 0) = 0)
131	130	oveq2d 7372	. . . 4 ⊢ (¬ 𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0))
132		ifcl 4523	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜑, 𝐴, 0) ∈ ℂ)
133	1, 132	mpan2 691	. . . . . 6 ⊢ (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ)
134	133, 3	addcld 11149	. . . . 5 ⊢ (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ)
135	134	addridd 11331	. . . 4 ⊢ (𝐴 ∈ ℂ → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
136	131, 135	sylan9eqr 2791	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
137	121, 129, 136	3eqtr4d 2779	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
138	84, 137	pm2.61dan 812	1 ⊢ (𝐴 ∈ ℂ → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ⊻ wxo 1512   = wceq 1541  haddwhad 1594  caddwcad 1607   ∈ wcel 2113  ifcif 4477  (class class class)co 7356  ℂcc 11022  0cc0 11024   + caddc 11027   · cmul 11029  2c2 12198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1513  df-tru 1544  df-fal 1554  df-had 1595  df-cad 1608  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-ltxr 11169  df-2 12206

This theorem is referenced by:  sadadd2lem  16384