gsumpropd2lem

	Ref	Expression
Hypotheses	gsumpropd2.f	$⊢ φ \to F \in V$
	gsumpropd2.g	$⊢ φ \to G \in W$
	gsumpropd2.h	$⊢ φ \to H \in X$
	gsumpropd2.b	$⊢ φ \to {Base}_{G} = {Base}_{H}$
	gsumpropd2.c	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to s +_{G} t \in {Base}_{G}$
	gsumpropd2.e	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to s +_{G} t = s +_{H} t$
	gsumpropd2.n	$⊢ φ \to Fun F$
	gsumpropd2.r	$⊢ φ \to ran F \subseteq {Base}_{G}$
	gsumprop2dlem.1	$⊢ A = F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
	gsumprop2dlem.2	$⊢ B = F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]$
Assertion	gsumpropd2lem	$⊢ φ \to \sum_{G} F = \sum_{H} F$

Proof

Step	Hyp	Ref	Expression
1		gsumpropd2.f	$⊢ φ \to F \in V$
2		gsumpropd2.g	$⊢ φ \to G \in W$
3		gsumpropd2.h	$⊢ φ \to H \in X$
4		gsumpropd2.b	$⊢ φ \to {Base}_{G} = {Base}_{H}$
5		gsumpropd2.c	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to s +_{G} t \in {Base}_{G}$
6		gsumpropd2.e	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to s +_{G} t = s +_{H} t$
7		gsumpropd2.n	$⊢ φ \to Fun F$
8		gsumpropd2.r	$⊢ φ \to ran F \subseteq {Base}_{G}$
9		gsumprop2dlem.1	$⊢ A = F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
10		gsumprop2dlem.2	$⊢ B = F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]$
11	4	adantr	$⊢ (φ \land s \in {Base}_{G}) \to {Base}_{G} = {Base}_{H}$
12	6	eqeq1d	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to (s +_{G} t = t \leftrightarrow s +_{H} t = t)$
13	6	oveqrspc2v	$⊢ (φ \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b = a +_{H} b$
14	13	oveqrspc2v	$⊢ (φ \land (t \in {Base}_{G} \land s \in {Base}_{G})) \to t +_{G} s = t +_{H} s$
15	14	ancom2s	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to t +_{G} s = t +_{H} s$
16	15	eqeq1d	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to (t +_{G} s = t \leftrightarrow t +_{H} s = t)$
17	12 16	anbi12d	$⊢ (φ \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to ((s +_{G} t = t \land t +_{G} s = t) \leftrightarrow (s +_{H} t = t \land t +_{H} s = t))$
18	17	anassrs	$⊢ ((φ \land s \in {Base}_{G}) \land t \in {Base}_{G}) \to ((s +_{G} t = t \land t +_{G} s = t) \leftrightarrow (s +_{H} t = t \land t +_{H} s = t))$
19	11 18	raleqbidva	$⊢ (φ \land s \in {Base}_{G}) \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))$
20	4 19	rabeqbidva	$⊢ φ \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)\}$
21	20	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)\})$
22		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
23	22 4 6	grpidpropd	$⊢ φ \to 0_{G} = 0_{H}$
24		simprl	$⊢ (φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \to n \in ℤ_{\geq m}$
25	8	ad2antrr	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to ran F \subseteq {Base}_{G}$
26	7	ad2antrr	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to Fun F$
27		simpr	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to s \in (m \dots n)$
28		simplrr	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to dom F = (m \dots n)$
29	27 28	eleqtrrd	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to s \in dom F$
30		fvelrn	$⊢ (Fun F \land s \in dom F) \to F (s) \in ran F$
31	26 29 30	syl2anc	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to F (s) \in ran F$
32	25 31	sseldd	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land s \in (m \dots n)) \to F (s) \in {Base}_{G}$
33	5	adantlr	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to s +_{G} t \in {Base}_{G}$
34	6	adantlr	$⊢ ((φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \land (s \in {Base}_{G} \land t \in {Base}_{G})) \to s +_{G} t = s +_{H} t$
35	24 32 33 34	seqfeq4	$⊢ (φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \to seq m (+_{G}, F) (n) = seq m (+_{H}, F) (n)$
36	35	eqeq2d	$⊢ (φ \land (n \in ℤ_{\geq m} \land dom F = (m \dots n))) \to (x = seq m (+_{G}, F) (n) \leftrightarrow x = seq m (+_{H}, F) (n))$
37	36	anassrs	$⊢ ((φ \land n \in ℤ_{\geq m}) \land dom F = (m \dots n)) \to (x = seq m (+_{G}, F) (n) \leftrightarrow x = seq m (+_{H}, F) (n))$
38	37	pm5.32da	$⊢ (φ \land n \in ℤ_{\geq m}) \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)))$
39	38	rexbidva	$⊢ φ \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)))$
40	39	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)))$
41	40	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)))$
42	20	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)\}$
43	42	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)\}]$
44	43 9 10	3eqtr4g	$⊢ φ \to A = B$
45	44	fveq2d	$⊢ φ \to \|A\| = \|B\|$
46	45	fveq2d	$⊢ φ \to seq 1 (+_{G}, (F \circ f)) (\|A\|) = seq 1 (+_{G}, (F \circ f)) (\|B\|)$
47	46	adantr	$⊢ (φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to seq 1 (+_{G}, (F \circ f)) (\|A\|) = seq 1 (+_{G}, (F \circ f)) (\|B\|)$
48		simpr	$⊢ ((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \to \|B\| \in ℤ_{\geq 1}$
49	8	ad3antrrr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to ran F \subseteq {Base}_{G}$
50		f1ofun	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to Fun f$
51	50	ad3antlr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to Fun f$
52		simpr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to a \in (1 \dots \|B\|)$
53		f1odm	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to dom f = (1 \dots \|A\|)$
54	53	ad3antlr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to dom f = (1 \dots \|A\|)$
55	45	oveq2d	$⊢ φ \to (1 \dots \|A\|) = (1 \dots \|B\|)$
56	55	ad3antrrr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to (1 \dots \|A\|) = (1 \dots \|B\|)$
57	54 56	eqtrd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to dom f = (1 \dots \|B\|)$
58	52 57	eleqtrrd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to a \in dom f$
59		fvco	$⊢ (Fun f \land a \in dom f) \to (F \circ f) (a) = F (f (a))$
60	51 58 59	syl2anc	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to (F \circ f) (a) = F (f (a))$
61	7	ad3antrrr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to Fun F$
62		difpreima	$⊢ Fun F \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] ∖ F^{-1} [\{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
63	7 62	syl	$⊢ φ \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] ∖ F^{-1} [\{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
64	9 63	eqtrid	$⊢ φ \to A = F^{-1} [V] ∖ F^{-1} [\{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
65		difss	$⊢ F^{-1} [V] ∖ F^{-1} [\{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}] \subseteq F^{-1} [V]$
66	64 65	eqsstrdi	$⊢ φ \to A \subseteq F^{-1} [V]$
67		dfdm4	$⊢ dom F = ran F^{-1}$
68		dfrn4	$⊢ ran F^{-1} = F^{-1} [V]$
69	67 68	eqtri	$⊢ dom F = F^{-1} [V]$
70	66 69	sseqtrrdi	$⊢ φ \to A \subseteq dom F$
71	70	ad3antrrr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to A \subseteq dom F$
72		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
73	72	ad3antlr	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to f : (1 \dots \|A\|) ⟶ A$
74	52 56	eleqtrrd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to a \in (1 \dots \|A\|)$
75	73 74	ffvelrnd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to f (a) \in A$
76	71 75	sseldd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to f (a) \in dom F$
77		fvelrn	$⊢ (Fun F \land f (a) \in dom F) \to F (f (a)) \in ran F$
78	61 76 77	syl2anc	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to F (f (a)) \in ran F$
79	60 78	eqeltrd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to (F \circ f) (a) \in ran F$
80	49 79	sseldd	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land a \in (1 \dots \|B\|)) \to (F \circ f) (a) \in {Base}_{G}$
81	5	caovclg	$⊢ (φ \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b \in {Base}_{G}$
82	81	ad4ant14	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b \in {Base}_{G}$
83	13	ad4ant14	$⊢ (((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b = a +_{H} b$
84	48 80 82 83	seqfeq4	$⊢ ((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \|B\| \in ℤ_{\geq 1}) \to seq 1 (+_{G}, (F \circ f)) (\|B\|) = seq 1 (+_{H}, (F \circ f)) (\|B\|)$
85		simpr	$⊢ (φ \land \neg \|B\| \in ℤ_{\geq 1}) \to \neg \|B\| \in ℤ_{\geq 1}$
86		1z	$⊢ 1 \in ℤ$
87		seqfn	$⊢ 1 \in ℤ \to seq 1 (+_{G}, (F \circ f)) Fn ℤ_{\geq 1}$
88		fndm	$⊢ seq 1 (+_{G}, (F \circ f)) Fn ℤ_{\geq 1} \to dom seq 1 (+_{G}, (F \circ f)) = ℤ_{\geq 1}$
89	86 87 88	mp2b	$⊢ dom seq 1 (+_{G}, (F \circ f)) = ℤ_{\geq 1}$
90	89	eleq2i	$⊢ \|B\| \in dom seq 1 (+_{G}, (F \circ f)) \leftrightarrow \|B\| \in ℤ_{\geq 1}$
91	85 90	sylnibr	$⊢ (φ \land \neg \|B\| \in ℤ_{\geq 1}) \to \neg \|B\| \in dom seq 1 (+_{G}, (F \circ f))$
92		ndmfv	$⊢ \neg \|B\| \in dom seq 1 (+_{G}, (F \circ f)) \to seq 1 (+_{G}, (F \circ f)) (\|B\|) = \emptyset$
93	91 92	syl	$⊢ (φ \land \neg \|B\| \in ℤ_{\geq 1}) \to seq 1 (+_{G}, (F \circ f)) (\|B\|) = \emptyset$
94		seqfn	$⊢ 1 \in ℤ \to seq 1 (+_{H}, (F \circ f)) Fn ℤ_{\geq 1}$
95		fndm	$⊢ seq 1 (+_{H}, (F \circ f)) Fn ℤ_{\geq 1} \to dom seq 1 (+_{H}, (F \circ f)) = ℤ_{\geq 1}$
96	86 94 95	mp2b	$⊢ dom seq 1 (+_{H}, (F \circ f)) = ℤ_{\geq 1}$
97	96	eleq2i	$⊢ \|B\| \in dom seq 1 (+_{H}, (F \circ f)) \leftrightarrow \|B\| \in ℤ_{\geq 1}$
98	85 97	sylnibr	$⊢ (φ \land \neg \|B\| \in ℤ_{\geq 1}) \to \neg \|B\| \in dom seq 1 (+_{H}, (F \circ f))$
99		ndmfv	$⊢ \neg \|B\| \in dom seq 1 (+_{H}, (F \circ f)) \to seq 1 (+_{H}, (F \circ f)) (\|B\|) = \emptyset$
100	98 99	syl	$⊢ (φ \land \neg \|B\| \in ℤ_{\geq 1}) \to seq 1 (+_{H}, (F \circ f)) (\|B\|) = \emptyset$
101	93 100	eqtr4d	$⊢ (φ \land \neg \|B\| \in ℤ_{\geq 1}) \to seq 1 (+_{G}, (F \circ f)) (\|B\|) = seq 1 (+_{H}, (F \circ f)) (\|B\|)$
102	101	adantlr	$⊢ ((φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land \neg \|B\| \in ℤ_{\geq 1}) \to seq 1 (+_{G}, (F \circ f)) (\|B\|) = seq 1 (+_{H}, (F \circ f)) (\|B\|)$
103	84 102	pm2.61dan	$⊢ (φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to seq 1 (+_{G}, (F \circ f)) (\|B\|) = seq 1 (+_{H}, (F \circ f)) (\|B\|)$
104	47 103	eqtrd	$⊢ (φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to seq 1 (+_{G}, (F \circ f)) (\|A\|) = seq 1 (+_{H}, (F \circ f)) (\|B\|)$
105	104	eqeq2d	$⊢ (φ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to (x = seq 1 (+_{G}, (F \circ f)) (\|A\|) \leftrightarrow x = seq 1 (+_{H}, (F \circ f)) (\|B\|))$
106	105	pm5.32da	$⊢ φ \to ((f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|)) \leftrightarrow (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))$
107	55	f1oeq2d	$⊢ φ \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} A)$
108	44	f1oeq3d	$⊢ φ \to (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)$
109	107 108	bitrd	$⊢ φ \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)$
110	109	anbi1d	$⊢ φ \to ((f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)) \leftrightarrow (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))$
111	106 110	bitrd	$⊢ φ \to ((f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|)) \leftrightarrow (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))$
112	111	exbidv	$⊢ φ \to (\exists f (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|)) \leftrightarrow \exists f (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))$
113	112	iotabidv	$⊢ φ \to (ι x \| \exists f (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|))) = (ι x \| \exists f (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))$
114	41 113	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 \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|)))) = 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 \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|))))$
115	21 23 114	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 \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|))))) = 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 \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))))$
116		eqid	$⊢ {Base}_{G} = {Base}_{G}$
117		eqid	$⊢ 0_{G} = 0_{G}$
118		eqid	$⊢ +_{G} = +_{G}$
119		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)\}$
120	9	a1i	$⊢ φ \to A = F^{-1} [V ∖ \{s \in {Base}_{G} \| \forall t \in {Base}_{G} (s +_{G} t = t \land t +_{G} s = t)\}]$
121		eqidd	$⊢ φ \to dom F = dom F$
122	116 117 118 119 120 2 1 121	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 \|A\|) \underset{1-1 onto}{⟶} A \land x = seq 1 (+_{G}, (F \circ f)) (\|A\|)))))$
123		eqid	$⊢ {Base}_{H} = {Base}_{H}$
124		eqid	$⊢ 0_{H} = 0_{H}$
125		eqid	$⊢ +_{H} = +_{H}$
126		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)\}$
127	10	a1i	$⊢ φ \to B = F^{-1} [V ∖ \{s \in {Base}_{H} \| \forall t \in {Base}_{H} (s +_{H} t = t \land t +_{H} s = t)\}]$
128	123 124 125 126 127 3 1 121	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 \|B\|) \underset{1-1 onto}{⟶} B \land x = seq 1 (+_{H}, (F \circ f)) (\|B\|)))))$
129	115 122 128	3eqtr4d	$⊢ φ \to \sum_{G} F = \sum_{H} F$

Metamath Proof Explorer

Theorem gsumpropd2lem

Proof