gsumval3lem1

	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)$
	gsumval3.m	$⊢ φ \to M \in ℕ$
	gsumval3.h	$⊢ φ \to H : (1 \dots M) \underset{1-1}{⟶} A$
	gsumval3.n	$⊢ φ \to F supp \underset{˙}{0} \subseteq ran H$
	gsumval3.w	$⊢ W = (F \circ H) supp \underset{˙}{0}$
Assertion	gsumval3lem1	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$

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		gsumval3.m	$⊢ φ \to M \in ℕ$
10		gsumval3.h	$⊢ φ \to H : (1 \dots M) \underset{1-1}{⟶} A$
11		gsumval3.n	$⊢ φ \to F supp \underset{˙}{0} \subseteq ran H$
12		gsumval3.w	$⊢ W = (F \circ H) supp \underset{˙}{0}$
13	10	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H : (1 \dots M) \underset{1-1}{⟶} A$
14		suppssdm	$⊢ (F \circ H) supp \underset{˙}{0} \subseteq dom (F \circ H)$
15	12 14	eqsstri	$⊢ W \subseteq dom (F \circ H)$
16		f1f	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H : (1 \dots M) ⟶ A$
17	10 16	syl	$⊢ φ \to H : (1 \dots M) ⟶ A$
18		fco	$⊢ (F : A ⟶ B \land H : (1 \dots M) ⟶ A) \to (F \circ H) : (1 \dots M) ⟶ B$
19	7 17 18	syl2anc	$⊢ φ \to (F \circ H) : (1 \dots M) ⟶ B$
20	15 19	fssdm	$⊢ φ \to W \subseteq (1 \dots M)$
21	20	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \subseteq (1 \dots M)$
22		f1ores	$⊢ (H : (1 \dots M) \underset{1-1}{⟶} A \land W \subseteq (1 \dots M)) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W]$
23	13 21 22	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W]$
24	12	imaeq2i	$⊢ H [W] = H [(F \circ H) supp \underset{˙}{0}]$
25		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
26	7 6 25	syl2anc	$⊢ φ \to F \in V$
27		ovex	$⊢ (1 \dots M) \in V$
28		fex	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in V) \to H \in V$
29	16 27 28	sylancl	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H \in V$
30	10 29	syl	$⊢ φ \to H \in V$
31		f1fun	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to Fun H$
32	10 31	syl	$⊢ φ \to Fun H$
33	32 11	jca	$⊢ φ \to (Fun H \land F supp \underset{˙}{0} \subseteq ran H)$
34	26 30 33	jca31	$⊢ φ \to ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H))$
35	34	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H))$
36		imacosupp	$⊢ (F \in V \land H \in V) \to ((Fun H \land F supp \underset{˙}{0} \subseteq ran H) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0})$
37	36	imp	$⊢ ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H)) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
38	35 37	syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
39	24 38	syl5eq	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H [W] = F supp \underset{˙}{0}$
40	39	f1oeq3d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W] \leftrightarrow ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
41	23 40	mpbid	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
42		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|W\|), W) \to f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
43	42	ad2antll	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
44		f1oco	$⊢ (({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W) \to (({H ↾}_{W}) \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
45	41 43 44	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (({H ↾}_{W}) \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
46		f1of	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) ⟶ W$
47		frn	$⊢ f : (1 \dots \|W\|) ⟶ W \to ran f \subseteq W$
48	43 46 47	3syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ran f \subseteq W$
49		cores	$⊢ ran f \subseteq W \to ({H ↾}_{W}) \circ f = H \circ f$
50		f1oeq1	$⊢ ({H ↾}_{W}) \circ f = H \circ f \to ((({H ↾}_{W}) \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \leftrightarrow (H \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
51	48 49 50	3syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ((({H ↾}_{W}) \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \leftrightarrow (H \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
52	45 51	mpbid	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (H \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
53		fzfi	$⊢ (1 \dots M) \in Fin$
54		ssfi	$⊢ ((1 \dots M) \in Fin \land W \subseteq (1 \dots M)) \to W \in Fin$
55	53 20 54	sylancr	$⊢ φ \to W \in Fin$
56	55	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \in Fin$
57	12	a1i	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W = (F \circ H) supp \underset{˙}{0}$
58	57	imaeq2d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H [W] = H [(F \circ H) supp \underset{˙}{0}]$
59	53	a1i	$⊢ φ \to (1 \dots M) \in Fin$
60		fex2	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in Fin \land A \in V) \to H \in V$
61	17 59 6 60	syl3anc	$⊢ φ \to H \in V$
62	26 61 33	jca31	$⊢ φ \to ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H))$
63	62	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H))$
64	63 37	syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
65	58 64	eqtrd	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H [W] = F supp \underset{˙}{0}$
66	65	f1oeq3d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W] \leftrightarrow ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
67	23 66	mpbid	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
68	56 67	hasheqf1od	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \|W\| = \|F supp \underset{˙}{0}\|$
69	68	oveq2d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (1 \dots \|W\|) = (1 \dots \|F supp \underset{˙}{0}\|)$
70	69	f1oeq2d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ((H \circ f) : (1 \dots \|W\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \leftrightarrow (H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
71	52 70	mpbid	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$

Metamath Proof Explorer

Theorem gsumval3lem1

Proof