gsumpropd

Description: The group sum depends only on the base set and additive operation. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd etc. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	gsumpropd.f	$⊢ φ \to F \in V$
	gsumpropd.g	$⊢ φ \to G \in W$
	gsumpropd.h	$⊢ φ \to H \in X$
	gsumpropd.b	$⊢ φ \to {Base}_{G} = {Base}_{H}$
	gsumpropd.p	$⊢ φ \to +_{G} = +_{H}$
Assertion	gsumpropd	$⊢ φ \to \sum_{G} F = \sum_{H} F$

Proof

Step	Hyp	Ref	Expression
1		gsumpropd.f	$⊢ φ \to F \in V$
2		gsumpropd.g	$⊢ φ \to G \in W$
3		gsumpropd.h	$⊢ φ \to H \in X$
4		gsumpropd.b	$⊢ φ \to {Base}_{G} = {Base}_{H}$
5		gsumpropd.p	$⊢ φ \to +_{G} = +_{H}$
6	5	oveqd	$⊢ φ \to s +_{G} t = s +_{H} t$
7	6	eqeq1d	$⊢ φ \to (s +_{G} t = t \leftrightarrow s +_{H} t = t)$
8	5	oveqd	$⊢ φ \to t +_{G} s = t +_{H} s$
9	8	eqeq1d	$⊢ φ \to (t +_{G} s = t \leftrightarrow t +_{H} s = t)$
10	7 9	anbi12d	$⊢ φ \to ((s +_{G} t = t \land t +_{G} s = t) \leftrightarrow (s +_{H} t = t \land t +_{H} s = t))$
11	4 10	raleqbidv	$⊢ φ \to (\forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t) \leftrightarrow \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t))$
12	4 11	rabeqbidv	$⊢ φ \to \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\} = \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}$
13	12	sseq2d	$⊢ φ \to (ran F \subseteq \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\} \leftrightarrow ran F \subseteq \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\})$
14		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
15	5	oveqdr	$⊢ (φ \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b = a +_{H} b$
16	14 4 15	grpidpropd	$⊢ φ \to 0_{G} = 0_{H}$
17	5	seqeq2d	$⊢ φ \to seq m (+_{G}, F) = seq m (+_{H}, F)$
18	17	fveq1d	$⊢ φ \to seq m (+_{G}, F) (n) = seq m (+_{H}, F) (n)$
19	18	eqeq2d	$⊢ φ \to (x = seq m (+_{G}, F) (n) \leftrightarrow x = seq m (+_{H}, F) (n))$
20	19	anbi2d	$⊢ φ \to ((dom F = (m \dots n) \land x = seq m (+_{G}, F) (n)) \leftrightarrow (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n)))$
21	20	rexbidv	$⊢ φ \to (\exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{G}, F) (n)) \leftrightarrow \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n)))$
22	21	exbidv	$⊢ φ \to (\exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{G}, F) (n)) \leftrightarrow \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n)))$
23	22	iotabidv	$⊢ φ \to (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{G}, F) (n))) = (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n)))$
24	12	difeq2d	$⊢ φ \to V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\} = V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}$
25	24	imaeq2d	$⊢ φ \to F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] = F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]$
26	25	fveq2d	$⊢ φ \to \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\| = \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|$
27	26	oveq2d	$⊢ φ \to (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) = (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)$
28	27	f1oeq2d	$⊢ φ \to (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \leftrightarrow f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}])$
29	25	f1oeq3d	$⊢ φ \to (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \leftrightarrow f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}])$
30	28 29	bitrd	$⊢ φ \to (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \leftrightarrow f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}])$
31	5	seqeq2d	$⊢ φ \to seq 1 (+_{G}, (F \circ f)) = seq 1 (+_{H}, (F \circ f))$
32	31 26	fveq12d	$⊢ φ \to seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)$
33	32	eqeq2d	$⊢ φ \to (x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \leftrightarrow x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|))$
34	30 33	anbi12d	$⊢ φ \to ((f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \land x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|)) \leftrightarrow (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] \land x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)))$
35	34	exbidv	$⊢ φ \to (\exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \land x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|)) \leftrightarrow \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] \land x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)))$
36	35	iotabidv	$⊢ φ \to (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \land x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|))) = (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] \land x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)))$
37	23 36	ifeq12d	$⊢ φ \to if (dom F \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{G}, F) (n))), (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \land x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|)))) = if (dom F \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n))), (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] \land x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|))))$
38	13 16 37	ifbieq12d	$⊢ φ \to if (ran F \subseteq \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}, 0_{G}, if (dom F \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{G}, F) (n))), (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \land x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|))))) = if (ran F \subseteq \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}, 0_{H}, if (dom F \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n))), (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] \land x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)))))$
39		eqid	$⊢ {Base}_{G} = {Base}_{G}$
40		eqid	$⊢ 0_{G} = 0_{G}$
41		eqid	$⊢ +_{G} = +_{G}$
42		eqid	$⊢ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\} = \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}$
43		eqidd	$⊢ φ \to F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] = F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
44		eqidd	$⊢ φ \to dom F = dom F$
45	39 40 41 42 43 2 1 44	gsumvalx	$⊢ φ \to \sum_{G} F = if (ran F \subseteq \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}, 0_{G}, if (dom F \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{G}, F) (n))), (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \land x = seq 1 (+_{G}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]\|)))))$
46		eqid	$⊢ {Base}_{H} = {Base}_{H}$
47		eqid	$⊢ 0_{H} = 0_{H}$
48		eqid	$⊢ +_{H} = +_{H}$
49		eqid	$⊢ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\} = \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}$
50		eqidd	$⊢ φ \to F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] = F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]$
51	46 47 48 49 50 3 1 44	gsumvalx	$⊢ φ \to \sum_{H} F = if (ran F \subseteq \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}, 0_{H}, if (dom F \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom F = (m \dots n) \land x = seq m (+_{H}, F) (n))), (ι x \| \exists f (f : (1 \dots \|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|) \underset{1-1 onto}{⟶} F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}] \land x = seq 1 (+_{H}, (F \circ f)) (\|F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]\|)))))$
52	38 45 51	3eqtr4d	$⊢ φ \to \sum_{G} F = \sum_{H} F$

Metamath Proof Explorer

Theorem gsumpropd

Proof