sumtp - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > sumtp		GIF version

Theorem sumtp 12096

Description: A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.)

**Hypotheses**
Ref	Expression
sumtp.e	⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)
sumtp.f	⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)
sumtp.g	⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)
sumtp.c	⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ))
sumtp.v	⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋))
sumtp.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
sumtp.2	⊢ (𝜑 → 𝐴 ≠ 𝐶)
sumtp.3	⊢ (𝜑 → 𝐵 ≠ 𝐶)

**Assertion**
Ref	Expression
sumtp	⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 + 𝐹) + 𝐺))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝐶,𝑘 𝑘,𝐸 𝑘,𝐹 𝑘,𝐺 𝜑,𝑘 𝑘,𝑉 𝑘,𝑊 𝑘,𝑋 Allowed substitution hint: 𝐷(𝑘)

**Proof of Theorem sumtp**
Step	Hyp	Ref	Expression
1		sumtp.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
2	1	necomd 2498	. . . . 5 ⊢ (𝜑 → 𝐶 ≠ 𝐴)
3		sumtp.3	. . . . . 6 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
4	3	necomd 2498	. . . . 5 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
5	2, 4	nelprd 3714	. . . 4 ⊢ (𝜑 → ¬ 𝐶 ∈ {𝐴, 𝐵})
6		disjsn 3750	. . . 4 ⊢ (({𝐴, 𝐵} ∩ {𝐶}) = ∅ ↔ ¬ 𝐶 ∈ {𝐴, 𝐵})
7	5, 6	sylibr 134	. . 3 ⊢ (𝜑 → ({𝐴, 𝐵} ∩ {𝐶}) = ∅)
8		df-tp 3696	. . . 4 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
9	8	a1i 9	. . 3 ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}))
10		sumtp.v	. . . . 5 ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋))
11	10	simp1d 1036	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
12	10	simp2d 1037	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
13	10	simp3d 1038	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
14		sumtp.1	. . . 4 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
15	11, 12, 13, 14, 1, 3	tpfidisj 7188	. . 3 ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin)
16		sumtp.c	. . . . 5 ⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ))
17		sumtp.e	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)
18	17	eleq1d 2301	. . . . . . 7 ⊢ (𝑘 = 𝐴 → (𝐷 ∈ ℂ ↔ 𝐸 ∈ ℂ))
19		sumtp.f	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)
20	19	eleq1d 2301	. . . . . . 7 ⊢ (𝑘 = 𝐵 → (𝐷 ∈ ℂ ↔ 𝐹 ∈ ℂ))
21		sumtp.g	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)
22	21	eleq1d 2301	. . . . . . 7 ⊢ (𝑘 = 𝐶 → (𝐷 ∈ ℂ ↔ 𝐺 ∈ ℂ))
23	18, 20, 22	raltpg 3741	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 ∈ ℂ ↔ (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ)))
24	10, 23	syl 14	. . . . 5 ⊢ (𝜑 → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 ∈ ℂ ↔ (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ)))
25	16, 24	mpbird 167	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 ∈ ℂ)
26	25	r19.21bi 2630	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝐴, 𝐵, 𝐶}) → 𝐷 ∈ ℂ)
27	7, 9, 15, 26	fsumsplit 12089	. 2 ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = (Σ𝑘 ∈ {𝐴, 𝐵}𝐷 + Σ𝑘 ∈ {𝐶}𝐷))
28		3simpa 1021	. . . . 5 ⊢ ((𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ) → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ))
29	16, 28	syl 14	. . . 4 ⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ))
30		3simpa 1021	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊))
31	10, 30	syl 14	. . . 4 ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊))
32	17, 19, 29, 31, 14	sumpr 12095	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 + 𝐹))
33	16	simp3d 1038	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ℂ)
34	21	sumsn 12093	. . . 4 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐺 ∈ ℂ) → Σ𝑘 ∈ {𝐶}𝐷 = 𝐺)
35	13, 33, 34	syl2anc 411	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝐶}𝐷 = 𝐺)
36	32, 35	oveq12d 6067	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ {𝐴, 𝐵}𝐷 + Σ𝑘 ∈ {𝐶}𝐷) = ((𝐸 + 𝐹) + 𝐺))
37	27, 36	eqtrd 2265	1 ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 + 𝐹) + 𝐺))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1005 = wceq 1398 ∈ wcel 2203 ≠ wne 2412 ∀wral 2520 ∪ cun 3208 ∩ cin 3209 ∅c0 3507 {csn 3688 {cpr 3689 {ctp 3690 (class class class)co 6049 ℂcc 8124 + caddc 8129 Σcsu 12034

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4224 ax-sep 4227 ax-nul 4235 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-iinf 4709 ax-cnex 8217 ax-resscn 8218 ax-1cn 8219 ax-1re 8220 ax-icn 8221 ax-addcl 8222 ax-addrcl 8223 ax-mulcl 8224 ax-mulrcl 8225 ax-addcom 8226 ax-mulcom 8227 ax-addass 8228 ax-mulass 8229 ax-distr 8230 ax-i2m1 8231 ax-0lt1 8232 ax-1rid 8233 ax-0id 8234 ax-rnegex 8235 ax-precex 8236 ax-cnre 8237 ax-pre-ltirr 8238 ax-pre-ltwlin 8239 ax-pre-lttrn 8240 ax-pre-apti 8241 ax-pre-ltadd 8242 ax-pre-mulgt0 8243 ax-pre-mulext 8244 ax-arch 8245 ax-caucvg 8246

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2814 df-sbc 3042 df-csb 3138 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-nul 3508 df-if 3620 df-pw 3670 df-sn 3694 df-pr 3695 df-tp 3696 df-op 3697 df-uni 3914 df-int 3949 df-iun 3992 df-br 4109 df-opab 4171 df-mpt 4172 df-tr 4208 df-id 4413 df-po 4416 df-iso 4417 df-iord 4486 df-on 4488 df-ilim 4489 df-suc 4491 df-iom 4712 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-rn 4759 df-res 4760 df-ima 4761 df-iota 5311 df-fun 5353 df-fn 5354 df-f 5355 df-f1 5356 df-fo 5357 df-f1o 5358 df-fv 5359 df-isom 5360 df-riota 6002 df-ov 6052 df-oprab 6053 df-mpo 6054 df-1st 6333 df-2nd 6334 df-recs 6535 df-irdg 6600 df-frec 6621 df-1o 6646 df-oadd 6650 df-er 6766 df-en 6975 df-dom 6976 df-fin 6977 df-pnf 8309 df-mnf 8310 df-xr 8311 df-ltxr 8312 df-le 8313 df-sub 8445 df-neg 8446 df-reap 8848 df-ap 8855 df-div 8946 df-inn 9237 df-2 9295 df-3 9296 df-4 9297 df-n0 9496 df-z 9577 df-uz 9853 df-q 9951 df-rp 9986 df-fz 10342 df-fzo 10476 df-seqfrec 10809 df-exp 10900 df-ihash 11137 df-cj 11523 df-re 11524 df-im 11525 df-rsqrt 11679 df-abs 11680 df-clim 11960 df-sumdc 12035

This theorem is referenced by: (None)

W3C validator