gsumvalx

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	gsumval.b	$⊢ B = {Base}_{G}$
	gsumval.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumval.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumval.o	$⊢ O = \{s \in B \| \forall t \in B (s \underset{˙}{+} t = t \land t \underset{˙}{+} s = t)\}$
	gsumval.w	$⊢ φ \to W = F^{-1} [V ∖ O]$
	gsumval.g	$⊢ φ \to G \in V$
	gsumvalx.f	$⊢ φ \to F \in X$
	gsumvalx.a	$⊢ φ \to dom F = A$
Assertion	gsumvalx	$⊢ φ \to \sum_{G} F = if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))))$

Proof

Step	Hyp	Ref	Expression
1		gsumval.b	$⊢ B = {Base}_{G}$
2		gsumval.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumval.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumval.o	$⊢ O = \{s \in B \| \forall t \in B (s \underset{˙}{+} t = t \land t \underset{˙}{+} s = t)\}$
5		gsumval.w	$⊢ φ \to W = F^{-1} [V ∖ O]$
6		gsumval.g	$⊢ φ \to G \in V$
7		gsumvalx.f	$⊢ φ \to F \in X$
8		gsumvalx.a	$⊢ φ \to dom F = A$
9		df-gsum	$⊢ Σ_{𝑔} = (w \in V, g \in V ⟼ ⦋ \{x \in {Base}_{w} \| \forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y)\} / o ⦌ if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))))))$
10	9	a1i	$⊢ φ \to Σ_{𝑔} = (w \in V, g \in V ⟼ ⦋ \{x \in {Base}_{w} \| \forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y)\} / o ⦌ if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))))))$
11		simprl	$⊢ (φ \land (w = G \land g = F)) \to w = G$
12	11	fveq2d	$⊢ (φ \land (w = G \land g = F)) \to {Base}_{w} = {Base}_{G}$
13	12 1	eqtr4di	$⊢ (φ \land (w = G \land g = F)) \to {Base}_{w} = B$
14	11	fveq2d	$⊢ (φ \land (w = G \land g = F)) \to +_{w} = +_{G}$
15	14 3	eqtr4di	$⊢ (φ \land (w = G \land g = F)) \to +_{w} = \underset{˙}{+}$
16	15	oveqd	$⊢ (φ \land (w = G \land g = F)) \to x +_{w} y = x \underset{˙}{+} y$
17	16	eqeq1d	$⊢ (φ \land (w = G \land g = F)) \to (x +_{w} y = y \leftrightarrow x \underset{˙}{+} y = y)$
18	15	oveqd	$⊢ (φ \land (w = G \land g = F)) \to y +_{w} x = y \underset{˙}{+} x$
19	18	eqeq1d	$⊢ (φ \land (w = G \land g = F)) \to (y +_{w} x = y \leftrightarrow y \underset{˙}{+} x = y)$
20	17 19	anbi12d	$⊢ (φ \land (w = G \land g = F)) \to ((x +_{w} y = y \land y +_{w} x = y) \leftrightarrow (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y))$
21	13 20	raleqbidv	$⊢ (φ \land (w = G \land g = F)) \to (\forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y) \leftrightarrow \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y))$
22	13 21	rabeqbidv	$⊢ (φ \land (w = G \land g = F)) \to \{x \in {Base}_{w} \| \forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y)\} = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
23		oveq2	$⊢ t = y \to s \underset{˙}{+} t = s \underset{˙}{+} y$
24		id	$⊢ t = y \to t = y$
25	23 24	eqeq12d	$⊢ t = y \to (s \underset{˙}{+} t = t \leftrightarrow s \underset{˙}{+} y = y)$
26		oveq1	$⊢ t = y \to t \underset{˙}{+} s = y \underset{˙}{+} s$
27	26 24	eqeq12d	$⊢ t = y \to (t \underset{˙}{+} s = t \leftrightarrow y \underset{˙}{+} s = y)$
28	25 27	anbi12d	$⊢ t = y \to ((s \underset{˙}{+} t = t \land t \underset{˙}{+} s = t) \leftrightarrow (s \underset{˙}{+} y = y \land y \underset{˙}{+} s = y))$
29	28	cbvralvw	$⊢ \forall t \in B (s \underset{˙}{+} t = t \land t \underset{˙}{+} s = t) \leftrightarrow \forall y \in B (s \underset{˙}{+} y = y \land y \underset{˙}{+} s = y)$
30		oveq1	$⊢ s = x \to s \underset{˙}{+} y = x \underset{˙}{+} y$
31	30	eqeq1d	$⊢ s = x \to (s \underset{˙}{+} y = y \leftrightarrow x \underset{˙}{+} y = y)$
32	31	ovanraleqv	$⊢ s = x \to (\forall y \in B (s \underset{˙}{+} y = y \land y \underset{˙}{+} s = y) \leftrightarrow \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y))$
33	29 32	syl5bb	$⊢ s = x \to (\forall t \in B (s \underset{˙}{+} t = t \land t \underset{˙}{+} s = t) \leftrightarrow \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y))$
34	33	cbvrabv	$⊢ \{s \in B \| \forall t \in B (s \underset{˙}{+} t = t \land t \underset{˙}{+} s = t)\} = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
35	4 34	eqtri	$⊢ O = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
36	22 35	eqtr4di	$⊢ (φ \land (w = G \land g = F)) \to \{x \in {Base}_{w} \| \forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y)\} = O$
37	36	csbeq1d	$⊢ (φ \land (w = G \land g = F)) \to ⦋ \{x \in {Base}_{w} \| \forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y)\} / o ⦌ if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))))) = ⦋ O / o ⦌ if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)))))$
38	1	fvexi	$⊢ B \in V$
39	4 38	rabex2	$⊢ O \in V$
40	39	a1i	$⊢ (φ \land (w = G \land g = F)) \to O \in V$
41		simplrr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to g = F$
42	41	rneqd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to ran g = ran F$
43		simpr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to o = O$
44	42 43	sseq12d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (ran g \subseteq o \leftrightarrow ran F \subseteq O)$
45	11	adantr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to w = G$
46	45	fveq2d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to 0_{w} = 0_{G}$
47	46 2	eqtr4di	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to 0_{w} = \underset{˙}{0}$
48	41	dmeqd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to dom g = dom F$
49	8	ad2antrr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to dom F = A$
50	48 49	eqtrd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to dom g = A$
51	50	eleq1d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (dom g \in ran \dots \leftrightarrow A \in ran \dots)$
52	50	eqeq1d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (dom g = (m \dots n) \leftrightarrow A = (m \dots n))$
53	15	adantr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to +_{w} = \underset{˙}{+}$
54	53	seqeq2d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq m (+_{w}, g) = seq m (\underset{˙}{+}, g)$
55	41	seqeq3d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq m (\underset{˙}{+}, g) = seq m (\underset{˙}{+}, F)$
56	54 55	eqtrd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq m (+_{w}, g) = seq m (\underset{˙}{+}, F)$
57	56	fveq1d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq m (+_{w}, g) (n) = seq m (\underset{˙}{+}, F) (n)$
58	57	eqeq2d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (x = seq m (+_{w}, g) (n) \leftrightarrow x = seq m (\underset{˙}{+}, F) (n))$
59	52 58	anbi12d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to ((dom g = (m \dots n) \land x = seq m (+_{w}, g) (n)) \leftrightarrow (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n)))$
60	59	rexbidv	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (\exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n)) \leftrightarrow \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n)))$
61	60	exbidv	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (\exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n)) \leftrightarrow \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n)))$
62	61	iotabidv	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))) = (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n)))$
63	43	difeq2d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to V ∖ o = V ∖ O$
64	63	imaeq2d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to F^{-1} [V ∖ o] = F^{-1} [V ∖ O]$
65	41	cnveqd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to g^{-1} = F^{-1}$
66	65	imaeq1d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to g^{-1} [V ∖ o] = F^{-1} [V ∖ o]$
67	5	ad2antrr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to W = F^{-1} [V ∖ O]$
68	64 66 67	3eqtr4d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to g^{-1} [V ∖ o] = W$
69	68	sbceq1d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (\underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)) \leftrightarrow \underset{˙}{[} W / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)))$
70		cnvexg	$⊢ F \in X \to F^{-1} \in V$
71		imaexg	$⊢ F^{-1} \in V \to F^{-1} [V ∖ O] \in V$
72	7 70 71	3syl	$⊢ φ \to F^{-1} [V ∖ O] \in V$
73	5 72	eqeltrd	$⊢ φ \to W \in V$
74	73	ad2antrr	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to W \in V$
75		fveq2	$⊢ y = W \to \|y\| = \|W\|$
76	75	adantl	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to \|y\| = \|W\|$
77	76	oveq2d	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to (1 \dots \|y\|) = (1 \dots \|W\|)$
78	77	f1oeq2d	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} y)$
79		f1oeq3	$⊢ y = W \to (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} y \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
80	79	adantl	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} y \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
81	78 80	bitrd	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
82	53	seqeq2d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq 1 (+_{w}, (g \circ f)) = seq 1 (\underset{˙}{+}, (g \circ f))$
83	41	coeq1d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to g \circ f = F \circ f$
84	83	seqeq3d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq 1 (\underset{˙}{+}, (g \circ f)) = seq 1 (\underset{˙}{+}, (F \circ f))$
85	82 84	eqtrd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to seq 1 (+_{w}, (g \circ f)) = seq 1 (\underset{˙}{+}, (F \circ f))$
86	85	adantr	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to seq 1 (+_{w}, (g \circ f)) = seq 1 (\underset{˙}{+}, (F \circ f))$
87	86 76	fveq12d	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to seq 1 (+_{w}, (g \circ f)) (\|y\|) = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)$
88	87	eqeq2d	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to (x = seq 1 (+_{w}, (g \circ f)) (\|y\|) \leftrightarrow x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))$
89	81 88	anbi12d	$⊢ (((φ \land (w = G \land g = F)) \land o = O) \land y = W) \to ((f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)) \leftrightarrow (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
90	74 89	sbcied	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (\underset{˙}{[} W / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)) \leftrightarrow (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
91	69 90	bitrd	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (\underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)) \leftrightarrow (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
92	91	exbidv	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (\exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)) \leftrightarrow \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
93	92	iotabidv	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))) = (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
94	51 62 93	ifbieq12d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|)))) = if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))))$
95	44 47 94	ifbieq12d	$⊢ ((φ \land (w = G \land g = F)) \land o = O) \to if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))))) = if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))))$
96	40 95	csbied	$⊢ (φ \land (w = G \land g = F)) \to ⦋ O / o ⦌ if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))))) = if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))))$
97	37 96	eqtrd	$⊢ (φ \land (w = G \land g = F)) \to ⦋ \{x \in {Base}_{w} \| \forall y \in {Base}_{w} (x +_{w} y = y \land y +_{w} x = y)\} / o ⦌ if (ran g \subseteq o, 0_{w}, if (dom g \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (dom g = (m \dots n) \land x = seq m (+_{w}, g) (n))), (ι x \| \exists f \underset{˙}{[} g^{-1} [V ∖ o] / y \underset{˙}{]} (f : (1 \dots \|y\|) \underset{1-1 onto}{⟶} y \land x = seq 1 (+_{w}, (g \circ f)) (\|y\|))))) = if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))))$
98	6	elexd	$⊢ φ \to G \in V$
99	7	elexd	$⊢ φ \to F \in V$
100	2	fvexi	$⊢ \underset{˙}{0} \in V$
101		iotaex	$⊢ (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))) \in V$
102		iotaex	$⊢ (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))) \in V$
103	101 102	ifex	$⊢ if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))) \in V$
104	100 103	ifex	$⊢ if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))))) \in V$
105	104	a1i	$⊢ φ \to if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))))) \in V$
106	10 97 98 99 105	ovmpod	$⊢ φ \to \sum_{G} F = if (ran F \subseteq O, \underset{˙}{0}, if (A \in ran \dots, (ι x \| \exists m \exists n \in ℤ_{\geq m} (A = (m \dots n) \land x = seq m (\underset{˙}{+}, F) (n))), (ι x \| \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))))$

Metamath Proof Explorer

Theorem gsumvalx

Proof