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	7 6	fexd	$⊢ φ \to F \in V$
26		ovex	$⊢ (1 \dots M) \in V$
27		fex	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in V) \to H \in V$
28	16 26 27	sylancl	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H \in V$
29	10 28	syl	$⊢ φ \to H \in V$
30		f1fun	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to Fun H$
31	10 30	syl	$⊢ φ \to Fun H$
32	31 11	jca	$⊢ φ \to (Fun H \land F supp \underset{˙}{0} \subseteq ran H)$
33	25 29 32	jca31	$⊢ φ \to ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H))$
34	33	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))$
35		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})$
36	35	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}$
37	34 36	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}$
38	24 37	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}$
39	38	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})$
40	23 39	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}$
41		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|W\|), W) \to f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
42	41	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$
43		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}$
44	40 42 43	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}$
45		f1of	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) ⟶ W$
46		frn	$⊢ f : (1 \dots \|W\|) ⟶ W \to ran f \subseteq W$
47	42 45 46	3syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ran f \subseteq W$
48		cores	$⊢ ran f \subseteq W \to ({H ↾}_{W}) \circ f = H \circ f$
49		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})$
50	47 48 49	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})$
51	44 50	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}$
52		fzfi	$⊢ (1 \dots M) \in Fin$
53		ssfi	$⊢ ((1 \dots M) \in Fin \land W \subseteq (1 \dots M)) \to W \in Fin$
54	52 20 53	sylancr	$⊢ φ \to W \in Fin$
55	54	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \in Fin$
56	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}$
57	56	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}]$
58	52	a1i	$⊢ φ \to (1 \dots M) \in Fin$
59	17 58	fexd	$⊢ φ \to H \in V$
60	25 59 32	jca31	$⊢ φ \to ((F \in V \land H \in V) \land (Fun H \land F supp \underset{˙}{0} \subseteq ran H))$
61	60	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))$
62	61 36	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}$
63	57 62	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}$
64	63	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})$
65	23 64	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}$
66	55 65	hasheqf1od	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \|W\| = \|F supp \underset{˙}{0}\|$
67	66	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}\|)$
68	67	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})$
69	51 68	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