gsumval3eu

Description: The group sum as defined in gsumval3a is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014)

	Ref	Expression
Hypotheses	gsumval3.b	$⊢ B = {Base}_{G}$
	gsumval3.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsumval3.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumval3.z	$⊢ Z = Cntz (G)$
	gsumval3.g	$⊢ φ \to G \in Mnd$
	gsumval3.a	$⊢ φ \to A \in V$
	gsumval3.f	$⊢ φ \to F : A ⟶ B$
	gsumval3.c	$⊢ φ \to ran F \subseteq Z (ran F)$
	gsumval3a.t	$⊢ φ \to W \in Fin$
	gsumval3a.n	$⊢ φ \to W \neq \emptyset$
	gsumval3a.s	$⊢ φ \to W \subseteq A$
Assertion	gsumval3eu	$⊢ φ \to \exists! 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		gsumval3.b	$⊢ B = {Base}_{G}$
2		gsumval3.0	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumval3.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumval3.z	$⊢ Z = Cntz (G)$
5		gsumval3.g	$⊢ φ \to G \in Mnd$
6		gsumval3.a	$⊢ φ \to A \in V$
7		gsumval3.f	$⊢ φ \to F : A ⟶ B$
8		gsumval3.c	$⊢ φ \to ran F \subseteq Z (ran F)$
9		gsumval3a.t	$⊢ φ \to W \in Fin$
10		gsumval3a.n	$⊢ φ \to W \neq \emptyset$
11		gsumval3a.s	$⊢ φ \to W \subseteq A$
12	10	neneqd	$⊢ φ \to \neg W = \emptyset$
13		fz1f1o	$⊢ W \in Fin \to (W = \emptyset \lor (\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W))$
14	9 13	syl	$⊢ φ \to (W = \emptyset \lor (\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W))$
15	14	ord	$⊢ φ \to (\neg W = \emptyset \to (\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W))$
16	12 15	mpd	$⊢ φ \to (\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
17	16	simprd	$⊢ φ \to \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
18		excom	$⊢ \exists x \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists f \exists x (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))$
19		exancom	$⊢ \exists x (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists x (x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
20		fvex	$⊢ seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \in V$
21		biidd	$⊢ x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \to (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
22	20 21	ceqsexv	$⊢ \exists x (x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W) \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
23	19 22	bitri	$⊢ \exists x (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
24	23	exbii	$⊢ \exists f \exists x (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
25	18 24	bitri	$⊢ \exists x \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
26	17 25	sylibr	$⊢ φ \to \exists x \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))$
27		exdistrv	$⊢ \exists f \exists g ((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \leftrightarrow (\exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land \exists g (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)))$
28		an4	$⊢ ((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W) \land (x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \leftrightarrow ((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)))$
29	5	adantr	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to G \in Mnd$
30	1 3	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
31	30	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
32	29 31	sylan	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
33	8	adantr	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ran F \subseteq Z (ran F)$
34	33	sselda	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in ran F) \to x \in Z (ran F)$
35	34	adantrr	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (x \in ran F \land y \in ran F)) \to x \in Z (ran F)$
36		simprr	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (x \in ran F \land y \in ran F)) \to y \in ran F$
37	3 4	cntzi	$⊢ (x \in Z (ran F) \land y \in ran F) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
38	35 36 37	syl2anc	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (x \in ran F \land y \in ran F)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
39	1 3	mndass	$⊢ (G \in Mnd \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
40	29 39	sylan	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
41	16	simpld	$⊢ φ \to \|W\| \in ℕ$
42	41	adantr	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \|W\| \in ℕ$
43		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
44	42 43	eleqtrdi	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \|W\| \in ℤ_{\geq 1}$
45	7	adantr	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to F : A ⟶ B$
46	45	frnd	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ran F \subseteq B$
47		simprr	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
48		f1ocnv	$⊢ g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to g^{-1} : W \underset{1-1 onto}{⟶} (1 \dots \|W\|)$
49	47 48	syl	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to g^{-1} : W \underset{1-1 onto}{⟶} (1 \dots \|W\|)$
50		simprl	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
51		f1oco	$⊢ (g^{-1} : W \underset{1-1 onto}{⟶} (1 \dots \|W\|) \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W) \to (g^{-1} \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} (1 \dots \|W\|)$
52	49 50 51	syl2anc	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (g^{-1} \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} (1 \dots \|W\|)$
53		f1of	$⊢ g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to g : (1 \dots \|W\|) ⟶ W$
54	47 53	syl	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to g : (1 \dots \|W\|) ⟶ W$
55		fvco3	$⊢ (g : (1 \dots \|W\|) ⟶ W \land x \in (1 \dots \|W\|)) \to (F \circ g) (x) = F (g (x))$
56	54 55	sylan	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (1 \dots \|W\|)) \to (F \circ g) (x) = F (g (x))$
57	45	ffnd	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to F Fn A$
58	11	adantr	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to W \subseteq A$
59	54 58	fssd	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to g : (1 \dots \|W\|) ⟶ A$
60	59	ffvelrnda	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (1 \dots \|W\|)) \to g (x) \in A$
61		fnfvelrn	$⊢ (F Fn A \land g (x) \in A) \to F (g (x)) \in ran F$
62	57 60 61	syl2an2r	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (1 \dots \|W\|)) \to F (g (x)) \in ran F$
63	56 62	eqeltrd	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (1 \dots \|W\|)) \to (F \circ g) (x) \in ran F$
64		f1of	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) ⟶ W$
65	50 64	syl	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to f : (1 \dots \|W\|) ⟶ W$
66		fvco3	$⊢ (f : (1 \dots \|W\|) ⟶ W \land k \in (1 \dots \|W\|)) \to (g^{-1} \circ f) (k) = g^{-1} (f (k))$
67	65 66	sylan	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (g^{-1} \circ f) (k) = g^{-1} (f (k))$
68	67	fveq2d	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to g ((g^{-1} \circ f) (k)) = g (g^{-1} (f (k)))$
69	65	ffvelrnda	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to f (k) \in W$
70		f1ocnvfv2	$⊢ (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land f (k) \in W) \to g (g^{-1} (f (k))) = f (k)$
71	47 69 70	syl2an2r	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to g (g^{-1} (f (k))) = f (k)$
72	68 71	eqtr2d	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to f (k) = g ((g^{-1} \circ f) (k))$
73	72	fveq2d	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to F (f (k)) = F (g ((g^{-1} \circ f) (k)))$
74		fvco3	$⊢ (f : (1 \dots \|W\|) ⟶ W \land k \in (1 \dots \|W\|)) \to (F \circ f) (k) = F (f (k))$
75	65 74	sylan	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (F \circ f) (k) = F (f (k))$
76		f1of	$⊢ (g^{-1} \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} (1 \dots \|W\|) \to (g^{-1} \circ f) : (1 \dots \|W\|) ⟶ (1 \dots \|W\|)$
77	52 76	syl	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (g^{-1} \circ f) : (1 \dots \|W\|) ⟶ (1 \dots \|W\|)$
78	77	ffvelrnda	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (g^{-1} \circ f) (k) \in (1 \dots \|W\|)$
79		fvco3	$⊢ (g : (1 \dots \|W\|) ⟶ A \land (g^{-1} \circ f) (k) \in (1 \dots \|W\|)) \to (F \circ g) ((g^{-1} \circ f) (k)) = F (g ((g^{-1} \circ f) (k)))$
80	59 78 79	syl2an2r	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (F \circ g) ((g^{-1} \circ f) (k)) = F (g ((g^{-1} \circ f) (k)))$
81	73 75 80	3eqtr4d	$⊢ ((φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (F \circ f) (k) = (F \circ g) ((g^{-1} \circ f) (k))$
82	32 38 40 44 46 52 63 81	seqf1o	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)$
83		eqeq12	$⊢ (x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)) \to (x = y \leftrightarrow seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))$
84	82 83	syl5ibrcom	$⊢ (φ \land (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ((x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)) \to x = y)$
85	84	expimpd	$⊢ φ \to (((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W) \land (x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \to x = y)$
86	28 85	syl5bir	$⊢ φ \to (((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \to x = y)$
87	86	exlimdvv	$⊢ φ \to (\exists f \exists g ((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \to x = y)$
88	27 87	syl5bir	$⊢ φ \to ((\exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land \exists g (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \to x = y)$
89	88	alrimivv	$⊢ φ \to \forall x \forall y ((\exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land \exists g (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \to x = y)$
90		eqeq1	$⊢ x = y \to (x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \leftrightarrow y = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|))$
91	90	anbi2d	$⊢ x = y \to ((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
92	91	exbidv	$⊢ x = y \to (\exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)))$
93		f1oeq1	$⊢ f = g \to (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \leftrightarrow g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)$
94		coeq2	$⊢ f = g \to F \circ f = F \circ g$
95	94	seqeq3d	$⊢ f = g \to seq 1 (\underset{˙}{+}, (F \circ f)) = seq 1 (\underset{˙}{+}, (F \circ g))$
96	95	fveq1d	$⊢ f = g \to seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)$
97	96	eqeq2d	$⊢ f = g \to (y = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \leftrightarrow y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))$
98	93 97	anbi12d	$⊢ f = g \to ((f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)))$
99	98	cbvexvw	$⊢ \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists g (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))$
100	92 99	bitrdi	$⊢ x = y \to (\exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow \exists g (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|)))$
101	100	eu4	$⊢ \exists! x \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \leftrightarrow (\exists x \exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land \forall x \forall y ((\exists f (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land x = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)) \land \exists g (g : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \land y = seq 1 (\underset{˙}{+}, (F \circ g)) (\|W\|))) \to x = y))$
102	26 89 101	sylanbrc	$⊢ φ \to \exists! 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 gsumval3eu

Proof