Theorem esumpad2

Description: Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020)

	Ref	Expression
Hypotheses	esumpad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumpad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	esumpad.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
	esumpad.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 0 )
Assertion	esumpad2	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		esumpad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		esumpad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		esumpad.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
4		esumpad.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 0 )
5		nfv	⊢ Ⅎ 𝑘 𝜑
6		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
7	5 1 3 6	esummono	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 )
8		unexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V )
10		elun	⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
11		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
12	4 11	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
13	3 12	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
14	10 13	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
15		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
16	15	a1i	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) )
17	5 9 14 16	esummono	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 )
18		undif1	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
19		esumeq1	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) → Σ* 𝑘 ∈ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 )
20	18 19	ax-mp	⊢ Σ* 𝑘 ∈ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶
21		difexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ 𝐵 ) ∈ V )
22	1 21	syl	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ V )
23	6	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑘 ∈ 𝐴 )
24	23 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
25	22 2 24 4	esumpad	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 )
26	20 25	eqtr3id	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 )
27	17 26	breqtrd	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 )
28	7 27	jca	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) )
29		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
30	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
31		nfcv	⊢ Ⅎ 𝑘 ( 𝐴 ∖ 𝐵 )
32	31	esumcl	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∈ V ∧ ∀ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
33	22 30 32	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
34	29 33	sseldi	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ℝ* )
35	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
36		nfcv	⊢ Ⅎ 𝑘 𝐴
37	36	esumcl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
38	1 35 37	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
39	29 38	sseldi	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ℝ* )
40		xrletri3	⊢ ( ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ℝ* ) → ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 ↔ ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) ) )
41	34 39 40	syl2anc	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 ↔ ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) ) )
42	28 41	mpbird	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 )