gsumval2a

Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumval2.b	$⊢ B = {Base}_{G}$
	gsumval2.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumval2.g	$⊢ φ \to G \in V$
	gsumval2.n	$⊢ φ \to N \in ℤ_{\geq M}$
	gsumval2.f	$⊢ φ \to F : (M \dots N) ⟶ B$
	gsumval2a.o	$⊢ O = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
	gsumval2a.f	$⊢ φ \to \neg ran F \subseteq O$
Assertion	gsumval2a	$⊢ φ \to \sum_{G} F = seq M (\underset{˙}{+}, F) (N)$

Proof

Step	Hyp	Ref	Expression
1		gsumval2.b	$⊢ B = {Base}_{G}$
2		gsumval2.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsumval2.g	$⊢ φ \to G \in V$
4		gsumval2.n	$⊢ φ \to N \in ℤ_{\geq M}$
5		gsumval2.f	$⊢ φ \to F : (M \dots N) ⟶ B$
6		gsumval2a.o	$⊢ O = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
7		gsumval2a.f	$⊢ φ \to \neg ran F \subseteq O$
8		eqid	$⊢ 0_{G} = 0_{G}$
9		eqidd	$⊢ φ \to F^{-1} [V ∖ O] = F^{-1} [V ∖ O]$
10		ovexd	$⊢ φ \to (M \dots N) \in V$
11	1 8 2 6 9 3 10 5	gsumval	$⊢ φ \to \sum_{G} F = if (ran F \subseteq O, 0_{G}, if ((M \dots N) \in ran \dots, (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))), (ι z \| \exists f (f : (1 \dots \|F^{-1} [V ∖ O]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ O] \land z = seq 1 (\underset{˙}{+}, (F \circ f)) (\|F^{-1} [V ∖ O]\|)))))$
12	7	iffalsed	$⊢ φ \to if (ran F \subseteq O, 0_{G}, if ((M \dots N) \in ran \dots, (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))), (ι z \| \exists f (f : (1 \dots \|F^{-1} [V ∖ O]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ O] \land z = seq 1 (\underset{˙}{+}, (F \circ f)) (\|F^{-1} [V ∖ O]\|))))) = if ((M \dots N) \in ran \dots, (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))), (ι z \| \exists f (f : (1 \dots \|F^{-1} [V ∖ O]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ O] \land z = seq 1 (\underset{˙}{+}, (F \circ f)) (\|F^{-1} [V ∖ O]\|))))$
13		fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
14		ffn	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ \to \dots Fn (ℤ \times ℤ)$
15	13 14	ax-mp	$⊢ \dots Fn (ℤ \times ℤ)$
16		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
17	4 16	syl	$⊢ φ \to M \in ℤ$
18		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
19	4 18	syl	$⊢ φ \to N \in ℤ$
20		fnovrn	$⊢ (\dots Fn (ℤ \times ℤ) \land M \in ℤ \land N \in ℤ) \to (M \dots N) \in ran \dots$
21	15 17 19 20	mp3an2i	$⊢ φ \to (M \dots N) \in ran \dots$
22	21	iftrued	$⊢ φ \to if ((M \dots N) \in ran \dots, (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))), (ι z \| \exists f (f : (1 \dots \|F^{-1} [V ∖ O]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ O] \land z = seq 1 (\underset{˙}{+}, (F \circ f)) (\|F^{-1} [V ∖ O]\|)))) = (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)))$
23	12 22	eqtrd	$⊢ φ \to if (ran F \subseteq O, 0_{G}, if ((M \dots N) \in ran \dots, (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))), (ι z \| \exists f (f : (1 \dots \|F^{-1} [V ∖ O]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ O] \land z = seq 1 (\underset{˙}{+}, (F \circ f)) (\|F^{-1} [V ∖ O]\|))))) = (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)))$
24	11 23	eqtrd	$⊢ φ \to \sum_{G} F = (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)))$
25		fvex	$⊢ seq M (\underset{˙}{+}, F) (N) \in V$
26		fzopth	$⊢ N \in ℤ_{\geq M} \to ((M \dots N) = (m \dots n) \leftrightarrow (M = m \land N = n))$
27	4 26	syl	$⊢ φ \to ((M \dots N) = (m \dots n) \leftrightarrow (M = m \land N = n))$
28		simpl	$⊢ (M = m \land N = n) \to M = m$
29	28	seqeq1d	$⊢ (M = m \land N = n) \to seq M (\underset{˙}{+}, F) = seq m (\underset{˙}{+}, F)$
30		simpr	$⊢ (M = m \land N = n) \to N = n$
31	29 30	fveq12d	$⊢ (M = m \land N = n) \to seq M (\underset{˙}{+}, F) (N) = seq m (\underset{˙}{+}, F) (n)$
32	31	eqcomd	$⊢ (M = m \land N = n) \to seq m (\underset{˙}{+}, F) (n) = seq M (\underset{˙}{+}, F) (N)$
33		eqeq1	$⊢ z = seq m (\underset{˙}{+}, F) (n) \to (z = seq M (\underset{˙}{+}, F) (N) \leftrightarrow seq m (\underset{˙}{+}, F) (n) = seq M (\underset{˙}{+}, F) (N))$
34	32 33	syl5ibrcom	$⊢ (M = m \land N = n) \to (z = seq m (\underset{˙}{+}, F) (n) \to z = seq M (\underset{˙}{+}, F) (N))$
35	27 34	biimtrdi	$⊢ φ \to ((M \dots N) = (m \dots n) \to (z = seq m (\underset{˙}{+}, F) (n) \to z = seq M (\underset{˙}{+}, F) (N)))$
36	35	impd	$⊢ φ \to (((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \to z = seq M (\underset{˙}{+}, F) (N))$
37	36	rexlimdvw	$⊢ φ \to (\exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \to z = seq M (\underset{˙}{+}, F) (N))$
38	37	exlimdv	$⊢ φ \to (\exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \to z = seq M (\underset{˙}{+}, F) (N))$
39	17	adantr	$⊢ (φ \land z = seq M (\underset{˙}{+}, F) (N)) \to M \in ℤ$
40		oveq2	$⊢ n = N \to (M \dots n) = (M \dots N)$
41	40	eqcomd	$⊢ n = N \to (M \dots N) = (M \dots n)$
42	41	biantrurd	$⊢ n = N \to (z = seq M (\underset{˙}{+}, F) (n) \leftrightarrow ((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n)))$
43		fveq2	$⊢ n = N \to seq M (\underset{˙}{+}, F) (n) = seq M (\underset{˙}{+}, F) (N)$
44	43	eqeq2d	$⊢ n = N \to (z = seq M (\underset{˙}{+}, F) (n) \leftrightarrow z = seq M (\underset{˙}{+}, F) (N))$
45	42 44	bitr3d	$⊢ n = N \to (((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n)) \leftrightarrow z = seq M (\underset{˙}{+}, F) (N))$
46	45	rspcev	$⊢ (N \in ℤ_{\geq M} \land z = seq M (\underset{˙}{+}, F) (N)) \to \exists n \in ℤ_{\geq M} ((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n))$
47	4 46	sylan	$⊢ (φ \land z = seq M (\underset{˙}{+}, F) (N)) \to \exists n \in ℤ_{\geq M} ((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n))$
48		fveq2	$⊢ m = M \to ℤ_{\geq m} = ℤ_{\geq M}$
49		oveq1	$⊢ m = M \to (m \dots n) = (M \dots n)$
50	49	eqeq2d	$⊢ m = M \to ((M \dots N) = (m \dots n) \leftrightarrow (M \dots N) = (M \dots n))$
51		seqeq1	$⊢ m = M \to seq m (\underset{˙}{+}, F) = seq M (\underset{˙}{+}, F)$
52	51	fveq1d	$⊢ m = M \to seq m (\underset{˙}{+}, F) (n) = seq M (\underset{˙}{+}, F) (n)$
53	52	eqeq2d	$⊢ m = M \to (z = seq m (\underset{˙}{+}, F) (n) \leftrightarrow z = seq M (\underset{˙}{+}, F) (n))$
54	50 53	anbi12d	$⊢ m = M \to (((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \leftrightarrow ((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n)))$
55	48 54	rexeqbidv	$⊢ m = M \to (\exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \leftrightarrow \exists n \in ℤ_{\geq M} ((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n)))$
56	55	spcegv	$⊢ M \in ℤ \to (\exists n \in ℤ_{\geq M} ((M \dots N) = (M \dots n) \land z = seq M (\underset{˙}{+}, F) (n)) \to \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)))$
57	39 47 56	sylc	$⊢ (φ \land z = seq M (\underset{˙}{+}, F) (N)) \to \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))$
58	57	ex	$⊢ φ \to (z = seq M (\underset{˙}{+}, F) (N) \to \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)))$
59	38 58	impbid	$⊢ φ \to (\exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \leftrightarrow z = seq M (\underset{˙}{+}, F) (N))$
60	59	adantr	$⊢ (φ \land seq M (\underset{˙}{+}, F) (N) \in V) \to (\exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n)) \leftrightarrow z = seq M (\underset{˙}{+}, F) (N))$
61	60	iota5	$⊢ (φ \land seq M (\underset{˙}{+}, F) (N) \in V) \to (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))) = seq M (\underset{˙}{+}, F) (N)$
62	25 61	mpan2	$⊢ φ \to (ι z \| \exists m \exists n \in ℤ_{\geq m} ((M \dots N) = (m \dots n) \land z = seq m (\underset{˙}{+}, F) (n))) = seq M (\underset{˙}{+}, F) (N)$
63	24 62	eqtrd	$⊢ φ \to \sum_{G} F = seq M (\underset{˙}{+}, F) (N)$

Metamath Proof Explorer

Theorem gsumval2a

Proof