Theorem sadadd2lem2 16413

Description: The core of the proof of sadadd2 16423. 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 11130	. . . . . . . . 9 ⊢ 0 ∈ ℂ
2		ifcl 4513	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜓, 𝐴, 0) ∈ ℂ)
3	1, 2	mpan2 692	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ)
4	3	ad2antrr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
5		simpll 767	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ)
6	4, 5, 5	add12d 11367	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
7	5, 4, 5	addassd 11161	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
8	6, 7	eqtr4d 2775	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
9		pm5.501 366	. . . . . . . . 9 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
10	9	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓)))
11	10	bicomd 223	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑 ↔ 𝜓) ↔ 𝜓))
12	11	ifbid 4491	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ↔ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
13		animorrl 983	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑 ∨ 𝜓))
14		iftrue 4473	. . . . . . . 8 ⊢ ((𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
15	13, 14	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
16	5	2timesd 12414	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴))
17	15, 16	eqtrd 2772	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴))
18	12, 17	oveq12d 7379	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)))
19		iftrue 4473	. . . . . . . 8 ⊢ (𝜑 → if(𝜑, 𝐴, 0) = 𝐴)
20	19	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
21	20	oveq1d 7376	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
22	21	oveq1d 7376	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
23	8, 18, 22	3eqtr4d 2782	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
24		iffalse 4476	. . . . . . . . 9 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 0) = 0)
25	24	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
26	25	oveq1d 7376	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
27	3	ad2antrr 727	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
28	27	addlidd 11341	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
29	26, 28	eqtrd 2772	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
30	29	oveq1d 7376	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴))
31		2cnd 12253	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
32		id 22	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
33	31, 32	mulcld 11159	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
34	33	addlidd 11341	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (2 · 𝐴))
35		2times 12306	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
36	34, 35	eqtrd 2772	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
37	36	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
38		iftrue 4473	. . . . . . . . . 10 ⊢ (𝜓 → if(𝜓, 0, 𝐴) = 0)
39	38	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0)
40		iftrue 4473	. . . . . . . . . 10 ⊢ (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
41	40	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
42	39, 41	oveq12d 7379	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴)))
43		iftrue 4473	. . . . . . . . . 10 ⊢ (𝜓 → if(𝜓, 𝐴, 0) = 𝐴)
44	43	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴)
45	44	oveq1d 7376	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴))
46	37, 42, 45	3eqtr4d 2782	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
47		simpl 482	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 𝐴 ∈ ℂ)
48		0cnd 11131	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 0 ∈ ℂ)
49	47, 48	addcomd 11342	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (𝐴 + 0) = (0 + 𝐴))
50		iffalse 4476	. . . . . . . . . 10 ⊢ (¬ 𝜓 → if(𝜓, 0, 𝐴) = 𝐴)
51	50	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 0, 𝐴) = 𝐴)
52		iffalse 4476	. . . . . . . . . 10 ⊢ (¬ 𝜓 → if(𝜓, (2 · 𝐴), 0) = 0)
53	52	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = 0)
54	51, 53	oveq12d 7379	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0))
55		iffalse 4476	. . . . . . . . . 10 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 0) = 0)
56	55	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 𝐴, 0) = 0)
57	56	oveq1d 7376	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴))
58	49, 54, 57	3eqtr4d 2782	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
59	46, 58	pm2.61dan 813	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
60	59	ad2antrr 727	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
61		ifnot 4520	. . . . . . 7 ⊢ if(¬ 𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴)
62		nbn2 370	. . . . . . . . 9 ⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
63	62	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
64	63	ifbid 4491	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0))
65	61, 64	eqtr3id 2786	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ↔ 𝜓), 𝐴, 0))
66		biorf 937	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))
67	66	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑 ∨ 𝜓)))
68	67	ifbid 4491	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))
69	65, 68	oveq12d 7379	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)))
70	30, 60, 69	3eqtr2rd 2779	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
71	23, 70	pm2.61dan 813	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
72		hadrot 1603	. . . . . . 7 ⊢ (hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒))
73		had1 1605	. . . . . . 7 ⊢ (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ↔ 𝜓)))
74	72, 73	bitr3id 285	. . . . . 6 ⊢ (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓)))
75	74	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓)))
76	75	ifbid 4491	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0))
77		cad1 1619	. . . . . 6 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓)))
78	77	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓)))
79	78	ifbid 4491	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))
80	76, 79	oveq12d 7379	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)))
81		iftrue 4473	. . . . 5 ⊢ (𝜒 → if(𝜒, 𝐴, 0) = 𝐴)
82	81	adantl 481	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴)
83	82	oveq2d 7377	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
84	71, 80, 83	3eqtr4d 2782	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
85	19	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
86	85	oveq1d 7376	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
87	44	oveq2d 7377	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴))
88	37, 42, 87	3eqtr4d 2782	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
89	53, 56	eqtr4d 2775	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0))
90	51, 89	oveq12d 7379	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
91	88, 90	pm2.61dan 813	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
92	91	ad2antrr 727	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
93	9	adantl 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓)))
94	93	notbid 318	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑 ↔ 𝜓)))
95		df-xor 1514	. . . . . . . . 9 ⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
96	94, 95	bitr4di 289	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑 ⊻ 𝜓)))
97	96	ifbid 4491	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0))
98	61, 97	eqtr3id 2786	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ⊻ 𝜓), 𝐴, 0))
99		ibar 528	. . . . . . . 8 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
100	99	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ∧ 𝜓)))
101	100	ifbid 4491	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))
102	98, 101	oveq12d 7379	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)))
103	86, 92, 102	3eqtr2rd 2779	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
104		simplll 775	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ)
105		0cnd 11131	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ)
106	104, 105	ifclda 4503	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
107		0cnd 11131	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → 0 ∈ ℂ)
108	106, 107	addcomd 11342	. . . . 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 4491	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑 ⊻ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
113		simpr 484	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ 𝜑)
114	113	intnanrd 489	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ (𝜑 ∧ 𝜓))
115		iffalse 4476	. . . . . . 7 ⊢ (¬ (𝜑 ∧ 𝜓) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0)
116	114, 115	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0)
117	112, 116	oveq12d 7379	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0))
118	24	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
119	118	oveq1d 7376	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
120	108, 117, 119	3eqtr4d 2782	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
121	103, 120	pm2.61dan 813	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
122		had0 1606	. . . . . . 7 ⊢ (¬ 𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ⊻ 𝜓)))
123	72, 122	bitr3id 285	. . . . . 6 ⊢ (¬ 𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓)))
124	123	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓)))
125	124	ifbid 4491	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0))
126		cad0 1620	. . . . . 6 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓)))
127	126	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓)))
128	127	ifbid 4491	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))
129	125, 128	oveq12d 7379	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)))
130		iffalse 4476	. . . . 5 ⊢ (¬ 𝜒 → if(𝜒, 𝐴, 0) = 0)
131	130	oveq2d 7377	. . . 4 ⊢ (¬ 𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0))
132		ifcl 4513	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜑, 𝐴, 0) ∈ ℂ)
133	1, 132	mpan2 692	. . . . . 6 ⊢ (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ)
134	133, 3	addcld 11158	. . . . 5 ⊢ (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ)
135	134	addridd 11340	. . . 4 ⊢ (𝐴 ∈ ℂ → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
136	131, 135	sylan9eqr 2794	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
137	121, 129, 136	3eqtr4d 2782	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
138	84, 137	pm2.61dan 813	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 848   ⊻ wxo 1513   = wceq 1542  haddwhad 1595  caddwcad 1608   ∈ wcel 2114  ifcif 4467  (class class class)co 7361  ℂcc 11030  0cc0 11032   + caddc 11035   · cmul 11037  2c2 12230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1514  df-tru 1545  df-fal 1555  df-had 1596  df-cad 1609  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-2 12238

This theorem is referenced by:  sadadd2lem  16422