tsmsxplem1

	Ref	Expression
Hypotheses	tsmsxp.b	$⊢ B = {Base}_{G}$
	tsmsxp.g	$⊢ φ \to G \in CMnd$
	tsmsxp.2	$⊢ φ \to G \in TopGrp$
	tsmsxp.a	$⊢ φ \to A \in V$
	tsmsxp.c	$⊢ φ \to C \in W$
	tsmsxp.f	$⊢ φ \to F : A \times C ⟶ B$
	tsmsxp.h	$⊢ φ \to H : A ⟶ B$
	tsmsxp.1	$⊢ (φ \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
	tsmsxp.j	$⊢ J = TopOpen (G)$
	tsmsxp.z	$⊢ \underset{˙}{0} = 0_{G}$
	tsmsxp.p	$⊢ \underset{˙}{+} = +_{G}$
	tsmsxp.m	$⊢ \underset{˙}{-} = -_{G}$
	tsmsxp.l	$⊢ φ \to L \in J$
	tsmsxp.3	$⊢ φ \to \underset{˙}{0} \in L$
	tsmsxp.k	$⊢ φ \to K \in (𝒫 A \cap Fin)$
	tsmsxp.ks	$⊢ φ \to dom D \subseteq K$
	tsmsxp.d	$⊢ φ \to D \in (𝒫 (A \times C) \cap Fin)$
Assertion	tsmsxplem1	$⊢ φ \to \exists n \in (𝒫 C \cap Fin) (ran D \subseteq n \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L)$

Proof

Step	Hyp	Ref	Expression
1		tsmsxp.b	$⊢ B = {Base}_{G}$
2		tsmsxp.g	$⊢ φ \to G \in CMnd$
3		tsmsxp.2	$⊢ φ \to G \in TopGrp$
4		tsmsxp.a	$⊢ φ \to A \in V$
5		tsmsxp.c	$⊢ φ \to C \in W$
6		tsmsxp.f	$⊢ φ \to F : A \times C ⟶ B$
7		tsmsxp.h	$⊢ φ \to H : A ⟶ B$
8		tsmsxp.1	$⊢ (φ \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
9		tsmsxp.j	$⊢ J = TopOpen (G)$
10		tsmsxp.z	$⊢ \underset{˙}{0} = 0_{G}$
11		tsmsxp.p	$⊢ \underset{˙}{+} = +_{G}$
12		tsmsxp.m	$⊢ \underset{˙}{-} = -_{G}$
13		tsmsxp.l	$⊢ φ \to L \in J$
14		tsmsxp.3	$⊢ φ \to \underset{˙}{0} \in L$
15		tsmsxp.k	$⊢ φ \to K \in (𝒫 A \cap Fin)$
16		tsmsxp.ks	$⊢ φ \to dom D \subseteq K$
17		tsmsxp.d	$⊢ φ \to D \in (𝒫 (A \times C) \cap Fin)$
18	15	elin2d	$⊢ φ \to K \in Fin$
19		elfpw	$⊢ K \in (𝒫 A \cap Fin) \leftrightarrow (K \subseteq A \land K \in Fin)$
20	19	simplbi	$⊢ K \in (𝒫 A \cap Fin) \to K \subseteq A$
21	15 20	syl	$⊢ φ \to K \subseteq A$
22	21	sselda	$⊢ (φ \land j \in K) \to j \in A$
23		eqid	$⊢ 𝒫 C \cap Fin = 𝒫 C \cap Fin$
24	2	adantr	$⊢ (φ \land j \in A) \to G \in CMnd$
25		tgptps	$⊢ G \in TopGrp \to G \in TopSp$
26	3 25	syl	$⊢ φ \to G \in TopSp$
27	26	adantr	$⊢ (φ \land j \in A) \to G \in TopSp$
28	5	adantr	$⊢ (φ \land j \in A) \to C \in W$
29		fovrn	$⊢ (F : A \times C ⟶ B \land j \in A \land k \in C) \to j F k \in B$
30	6 29	syl3an1	$⊢ (φ \land j \in A \land k \in C) \to j F k \in B$
31	30	3expa	$⊢ ((φ \land j \in A) \land k \in C) \to j F k \in B$
32	31	fmpttd	$⊢ (φ \land j \in A) \to (k \in C ⟼ j F k) : C ⟶ B$
33		df-ima	$⊢ (g \in B ⟼ H (j) \underset{˙}{-} g) [L] = ran ({(g \in B ⟼ H (j) \underset{˙}{-} g) ↾}_{L})$
34	9 1	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (B)$
35	3 34	syl	$⊢ φ \to J \in TopOn (B)$
36		toponss	$⊢ (J \in TopOn (B) \land L \in J) \to L \subseteq B$
37	35 13 36	syl2anc	$⊢ φ \to L \subseteq B$
38	37	adantr	$⊢ (φ \land j \in A) \to L \subseteq B$
39	38	resmptd	$⊢ (φ \land j \in A) \to {(g \in B ⟼ H (j) \underset{˙}{-} g) ↾}_{L} = (g \in L ⟼ H (j) \underset{˙}{-} g)$
40	39	rneqd	$⊢ (φ \land j \in A) \to ran ({(g \in B ⟼ H (j) \underset{˙}{-} g) ↾}_{L}) = ran (g \in L ⟼ H (j) \underset{˙}{-} g)$
41	33 40	eqtrid	$⊢ (φ \land j \in A) \to (g \in B ⟼ H (j) \underset{˙}{-} g) [L] = ran (g \in L ⟼ H (j) \underset{˙}{-} g)$
42	7	ffvelrnda	$⊢ (φ \land j \in A) \to H (j) \in B$
43		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
44	1 11 43 12	grpsubval	$⊢ (H (j) \in B \land g \in B) \to H (j) \underset{˙}{-} g = H (j) \underset{˙}{+} {inv}_{g} (G) (g)$
45	42 44	sylan	$⊢ ((φ \land j \in A) \land g \in B) \to H (j) \underset{˙}{-} g = H (j) \underset{˙}{+} {inv}_{g} (G) (g)$
46	45	mpteq2dva	$⊢ (φ \land j \in A) \to (g \in B ⟼ H (j) \underset{˙}{-} g) = (g \in B ⟼ H (j) \underset{˙}{+} {inv}_{g} (G) (g))$
47		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
48	3 47	syl	$⊢ φ \to G \in Grp$
49	48	adantr	$⊢ (φ \land j \in A) \to G \in Grp$
50	1 43	grpinvcl	$⊢ (G \in Grp \land g \in B) \to {inv}_{g} (G) (g) \in B$
51	49 50	sylan	$⊢ ((φ \land j \in A) \land g \in B) \to {inv}_{g} (G) (g) \in B$
52	1 43	grpinvf	$⊢ G \in Grp \to {inv}_{g} (G) : B ⟶ B$
53	49 52	syl	$⊢ (φ \land j \in A) \to {inv}_{g} (G) : B ⟶ B$
54	53	feqmptd	$⊢ (φ \land j \in A) \to {inv}_{g} (G) = (g \in B ⟼ {inv}_{g} (G) (g))$
55		eqidd	$⊢ (φ \land j \in A) \to (y \in B ⟼ H (j) \underset{˙}{+} y) = (y \in B ⟼ H (j) \underset{˙}{+} y)$
56		oveq2	$⊢ y = {inv}_{g} (G) (g) \to H (j) \underset{˙}{+} y = H (j) \underset{˙}{+} {inv}_{g} (G) (g)$
57	51 54 55 56	fmptco	$⊢ (φ \land j \in A) \to (y \in B ⟼ H (j) \underset{˙}{+} y) \circ {inv}_{g} (G) = (g \in B ⟼ H (j) \underset{˙}{+} {inv}_{g} (G) (g))$
58	46 57	eqtr4d	$⊢ (φ \land j \in A) \to (g \in B ⟼ H (j) \underset{˙}{-} g) = (y \in B ⟼ H (j) \underset{˙}{+} y) \circ {inv}_{g} (G)$
59	3	adantr	$⊢ (φ \land j \in A) \to G \in TopGrp$
60	9 43	grpinvhmeo	$⊢ G \in TopGrp \to {inv}_{g} (G) \in (J Homeo J)$
61	59 60	syl	$⊢ (φ \land j \in A) \to {inv}_{g} (G) \in (J Homeo J)$
62		eqid	$⊢ (y \in B ⟼ H (j) \underset{˙}{+} y) = (y \in B ⟼ H (j) \underset{˙}{+} y)$
63	62 1 11 9	tgplacthmeo	$⊢ (G \in TopGrp \land H (j) \in B) \to (y \in B ⟼ H (j) \underset{˙}{+} y) \in (J Homeo J)$
64	59 42 63	syl2anc	$⊢ (φ \land j \in A) \to (y \in B ⟼ H (j) \underset{˙}{+} y) \in (J Homeo J)$
65		hmeoco	$⊢ ({inv}_{g} (G) \in (J Homeo J) \land (y \in B ⟼ H (j) \underset{˙}{+} y) \in (J Homeo J)) \to (y \in B ⟼ H (j) \underset{˙}{+} y) \circ {inv}_{g} (G) \in (J Homeo J)$
66	61 64 65	syl2anc	$⊢ (φ \land j \in A) \to (y \in B ⟼ H (j) \underset{˙}{+} y) \circ {inv}_{g} (G) \in (J Homeo J)$
67	58 66	eqeltrd	$⊢ (φ \land j \in A) \to (g \in B ⟼ H (j) \underset{˙}{-} g) \in (J Homeo J)$
68	13	adantr	$⊢ (φ \land j \in A) \to L \in J$
69		hmeoima	$⊢ ((g \in B ⟼ H (j) \underset{˙}{-} g) \in (J Homeo J) \land L \in J) \to (g \in B ⟼ H (j) \underset{˙}{-} g) [L] \in J$
70	67 68 69	syl2anc	$⊢ (φ \land j \in A) \to (g \in B ⟼ H (j) \underset{˙}{-} g) [L] \in J$
71	41 70	eqeltrrd	$⊢ (φ \land j \in A) \to ran (g \in L ⟼ H (j) \underset{˙}{-} g) \in J$
72	1 10 12	grpsubid1	$⊢ (G \in Grp \land H (j) \in B) \to H (j) \underset{˙}{-} \underset{˙}{0} = H (j)$
73	49 42 72	syl2anc	$⊢ (φ \land j \in A) \to H (j) \underset{˙}{-} \underset{˙}{0} = H (j)$
74	14	adantr	$⊢ (φ \land j \in A) \to \underset{˙}{0} \in L$
75		ovex	$⊢ H (j) \underset{˙}{-} \underset{˙}{0} \in V$
76		eqid	$⊢ (g \in L ⟼ H (j) \underset{˙}{-} g) = (g \in L ⟼ H (j) \underset{˙}{-} g)$
77		oveq2	$⊢ g = \underset{˙}{0} \to H (j) \underset{˙}{-} g = H (j) \underset{˙}{-} \underset{˙}{0}$
78	76 77	elrnmpt1s	$⊢ (\underset{˙}{0} \in L \land H (j) \underset{˙}{-} \underset{˙}{0} \in V) \to H (j) \underset{˙}{-} \underset{˙}{0} \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)$
79	74 75 78	sylancl	$⊢ (φ \land j \in A) \to H (j) \underset{˙}{-} \underset{˙}{0} \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)$
80	73 79	eqeltrrd	$⊢ (φ \land j \in A) \to H (j) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)$
81	1 9 23 24 27 28 32 8 71 80	tsmsi	$⊢ (φ \land j \in A) \to \exists y \in (𝒫 C \cap Fin) \forall z \in (𝒫 C \cap Fin) (y \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
82	22 81	syldan	$⊢ (φ \land j \in K) \to \exists y \in (𝒫 C \cap Fin) \forall z \in (𝒫 C \cap Fin) (y \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
83	82	ralrimiva	$⊢ φ \to \forall j \in K \exists y \in (𝒫 C \cap Fin) \forall z \in (𝒫 C \cap Fin) (y \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
84		sseq1	$⊢ y = f (j) \to (y \subseteq z \leftrightarrow f (j) \subseteq z)$
85	84	imbi1d	$⊢ y = f (j) \to ((y \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \leftrightarrow (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))$
86	85	ralbidv	$⊢ y = f (j) \to (\forall z \in (𝒫 C \cap Fin) (y \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \leftrightarrow \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))$
87	86	ac6sfi	$⊢ (K \in Fin \land \forall j \in K \exists y \in (𝒫 C \cap Fin) \forall z \in (𝒫 C \cap Fin) (y \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))) \to \exists f (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))$
88	18 83 87	syl2anc	$⊢ φ \to \exists f (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))$
89		frn	$⊢ f : K ⟶ 𝒫 C \cap Fin \to ran f \subseteq 𝒫 C \cap Fin$
90	89	adantl	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ran f \subseteq 𝒫 C \cap Fin$
91		inss1	$⊢ 𝒫 C \cap Fin \subseteq 𝒫 C$
92	90 91	sstrdi	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ran f \subseteq 𝒫 C$
93		sspwuni	$⊢ ran f \subseteq 𝒫 C \leftrightarrow ⋃ ran f \subseteq C$
94	92 93	sylib	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \subseteq C$
95		elfpw	$⊢ D \in (𝒫 (A \times C) \cap Fin) \leftrightarrow (D \subseteq A \times C \land D \in Fin)$
96	95	simplbi	$⊢ D \in (𝒫 (A \times C) \cap Fin) \to D \subseteq A \times C$
97		rnss	$⊢ D \subseteq A \times C \to ran D \subseteq ran (A \times C)$
98	17 96 97	3syl	$⊢ φ \to ran D \subseteq ran (A \times C)$
99		rnxpss	$⊢ ran (A \times C) \subseteq C$
100	98 99	sstrdi	$⊢ φ \to ran D \subseteq C$
101	100	adantr	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ran D \subseteq C$
102	94 101	unssd	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \cup ran D \subseteq C$
103	18	adantr	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to K \in Fin$
104		ffn	$⊢ f : K ⟶ 𝒫 C \cap Fin \to f Fn K$
105	104	adantl	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to f Fn K$
106		dffn4	$⊢ f Fn K \leftrightarrow f : K \underset{onto}{⟶} ran f$
107	105 106	sylib	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to f : K \underset{onto}{⟶} ran f$
108		fofi	$⊢ (K \in Fin \land f : K \underset{onto}{⟶} ran f) \to ran f \in Fin$
109	103 107 108	syl2anc	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ran f \in Fin$
110		inss2	$⊢ 𝒫 C \cap Fin \subseteq Fin$
111	90 110	sstrdi	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ran f \subseteq Fin$
112		unifi	$⊢ (ran f \in Fin \land ran f \subseteq Fin) \to ⋃ ran f \in Fin$
113	109 111 112	syl2anc	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \in Fin$
114		elinel2	$⊢ D \in (𝒫 (A \times C) \cap Fin) \to D \in Fin$
115		rnfi	$⊢ D \in Fin \to ran D \in Fin$
116	17 114 115	3syl	$⊢ φ \to ran D \in Fin$
117	116	adantr	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ran D \in Fin$
118		unfi	$⊢ (⋃ ran f \in Fin \land ran D \in Fin) \to ⋃ ran f \cup ran D \in Fin$
119	113 117 118	syl2anc	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \cup ran D \in Fin$
120		elfpw	$⊢ ⋃ ran f \cup ran D \in (𝒫 C \cap Fin) \leftrightarrow (⋃ ran f \cup ran D \subseteq C \land ⋃ ran f \cup ran D \in Fin)$
121	102 119 120	sylanbrc	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \cup ran D \in (𝒫 C \cap Fin)$
122	121	adantrr	$⊢ (φ \land (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))) \to ⋃ ran f \cup ran D \in (𝒫 C \cap Fin)$
123		ssun2	$⊢ ran D \subseteq ⋃ ran f \cup ran D$
124	123	a1i	$⊢ (φ \land (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))) \to ran D \subseteq ⋃ ran f \cup ran D$
125	121	adantlr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \cup ran D \in (𝒫 C \cap Fin)$
126		fvssunirn	$⊢ f (j) \subseteq ⋃ ran f$
127		ssun1	$⊢ ⋃ ran f \subseteq ⋃ ran f \cup ran D$
128	126 127	sstri	$⊢ f (j) \subseteq ⋃ ran f \cup ran D$
129		id	$⊢ z = ⋃ ran f \cup ran D \to z = ⋃ ran f \cup ran D$
130	128 129	sseqtrrid	$⊢ z = ⋃ ran f \cup ran D \to f (j) \subseteq z$
131		pm5.5	$⊢ f (j) \subseteq z \to ((f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \leftrightarrow \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
132	130 131	syl	$⊢ z = ⋃ ran f \cup ran D \to ((f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \leftrightarrow \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
133		reseq2	$⊢ z = ⋃ ran f \cup ran D \to {(k \in C ⟼ j F k) ↾}_{z} = {(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}$
134	133	oveq2d	$⊢ z = ⋃ ran f \cup ran D \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) = \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)})$
135	134	eleq1d	$⊢ z = ⋃ ran f \cup ran D \to (\sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g) \leftrightarrow \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
136	132 135	bitrd	$⊢ z = ⋃ ran f \cup ran D \to ((f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \leftrightarrow \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
137	136	rspcv	$⊢ ⋃ ran f \cup ran D \in (𝒫 C \cap Fin) \to (\forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
138	125 137	syl	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (\forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
139	2	ad2antrr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to G \in CMnd$
140		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
141	139 140	syl	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to G \in Mnd$
142		simplr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to j \in K$
143	119	adantlr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \cup ran D \in Fin$
144	102	adantlr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to ⋃ ran f \cup ran D \subseteq C$
145	144	sselda	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land k \in (⋃ ran f \cup ran D)) \to k \in C$
146	6	adantr	$⊢ (φ \land j \in K) \to F : A \times C ⟶ B$
147	146 22	jca	$⊢ (φ \land j \in K) \to (F : A \times C ⟶ B \land j \in A)$
148	29	3expa	$⊢ ((F : A \times C ⟶ B \land j \in A) \land k \in C) \to j F k \in B$
149	147 148	sylan	$⊢ ((φ \land j \in K) \land k \in C) \to j F k \in B$
150	149	adantlr	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land k \in C) \to j F k \in B$
151	145 150	syldan	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land k \in (⋃ ran f \cup ran D)) \to j F k \in B$
152	151	fmpttd	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (k \in (⋃ ran f \cup ran D) ⟼ j F k) : ⋃ ran f \cup ran D ⟶ B$
153		eqid	$⊢ (k \in (⋃ ran f \cup ran D) ⟼ j F k) = (k \in (⋃ ran f \cup ran D) ⟼ j F k)$
154		ovexd	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land k \in (⋃ ran f \cup ran D)) \to j F k \in V$
155	10	fvexi	$⊢ \underset{˙}{0} \in V$
156	155	a1i	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \underset{˙}{0} \in V$
157	153 143 154 156	fsuppmptdm	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to {finSupp}_{\underset{˙}{0}} ((k \in (⋃ ran f \cup ran D) ⟼ j F k))$
158	1 10 139 143 152 157	gsumcl	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (j F k) \in B$
159		velsn	$⊢ y \in \{j\} \leftrightarrow y = j$
160		ovres	$⊢ (y \in \{j\} \land k \in (⋃ ran f \cup ran D)) \to y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k = y F k$
161	159 160	sylanbr	$⊢ (y = j \land k \in (⋃ ran f \cup ran D)) \to y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k = y F k$
162		oveq1	$⊢ y = j \to y F k = j F k$
163	162	adantr	$⊢ (y = j \land k \in (⋃ ran f \cup ran D)) \to y F k = j F k$
164	161 163	eqtrd	$⊢ (y = j \land k \in (⋃ ran f \cup ran D)) \to y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k = j F k$
165	164	mpteq2dva	$⊢ y = j \to (k \in (⋃ ran f \cup ran D) ⟼ y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k) = (k \in (⋃ ran f \cup ran D) ⟼ j F k)$
166	165	oveq2d	$⊢ y = j \to \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k) = \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (j F k)$
167	1 166	gsumsn	$⊢ (G \in Mnd \land j \in K \land \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (j F k) \in B) \to \underset{y \in \{j\}}{\sum_{G}} (\underset{k \in ⋃ ran f \cup ran D}{\sum_{G}}, (y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k)) = \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (j F k)$
168	141 142 158 167	syl3anc	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \underset{y \in \{j\}}{\sum_{G}} (\underset{k \in ⋃ ran f \cup ran D}{\sum_{G}}, (y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k)) = \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (j F k)$
169		snfi	$⊢ \{j\} \in Fin$
170	169	a1i	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \{j\} \in Fin$
171	6	ad2antrr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to F : A \times C ⟶ B$
172	22	adantr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to j \in A$
173	172	snssd	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \{j\} \subseteq A$
174		xpss12	$⊢ (\{j\} \subseteq A \land ⋃ ran f \cup ran D \subseteq C) \to \{j\} \times (⋃ ran f \cup ran D) \subseteq A \times C$
175	173 144 174	syl2anc	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \{j\} \times (⋃ ran f \cup ran D) \subseteq A \times C$
176	171 175	fssresd	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) : \{j\} \times (⋃ ran f \cup ran D) ⟶ B$
177		xpfi	$⊢ (\{j\} \in Fin \land ⋃ ran f \cup ran D \in Fin) \to \{j\} \times (⋃ ran f \cup ran D) \in Fin$
178	169 143 177	sylancr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \{j\} \times (⋃ ran f \cup ran D) \in Fin$
179	176 178 156	fdmfifsupp	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}))$
180	1 10 139 170 143 176 179	gsumxp	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = \underset{y \in \{j\}}{\sum_{G}} (\underset{k \in ⋃ ran f \cup ran D}{\sum_{G}}, (y ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) k))$
181	144	resmptd	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to {(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)} = (k \in (⋃ ran f \cup ran D) ⟼ j F k)$
182	181	oveq2d	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) = \underset{k \in ⋃ ran f \cup ran D}{\sum_{G}} (j F k)$
183	168 180 182	3eqtr4rd	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) = \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})$
184	183	eleq1d	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (\sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g) \leftrightarrow \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g))$
185		ovex	$⊢ H (j) \underset{˙}{-} g \in V$
186	76 185	elrnmpti	$⊢ \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g) \leftrightarrow \exists g \in L \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = H (j) \underset{˙}{-} g$
187		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
188	48 2 187	sylanbrc	$⊢ φ \to G \in Abel$
189	188	ad3antrrr	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to G \in Abel$
190	22 42	syldan	$⊢ (φ \land j \in K) \to H (j) \in B$
191	190	ad2antrr	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to H (j) \in B$
192	37	ad2antrr	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to L \subseteq B$
193	192	sselda	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to g \in B$
194	1 12 189 191 193	ablnncan	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to H (j) \underset{˙}{-} (H (j) \underset{˙}{-} g) = g$
195		simpr	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to g \in L$
196	194 195	eqeltrd	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to H (j) \underset{˙}{-} (H (j) \underset{˙}{-} g) \in L$
197		oveq2	$⊢ \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = H (j) \underset{˙}{-} g \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) = H (j) \underset{˙}{-} (H (j) \underset{˙}{-} g)$
198	197	eleq1d	$⊢ \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = H (j) \underset{˙}{-} g \to (H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L \leftrightarrow H (j) \underset{˙}{-} (H (j) \underset{˙}{-} g) \in L)$
199	196 198	syl5ibrcom	$⊢ (((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \land g \in L) \to (\sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = H (j) \underset{˙}{-} g \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
200	199	rexlimdva	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (\exists g \in L \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = H (j) \underset{˙}{-} g \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
201	186 200	syl5bi	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (\sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g) \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
202	184 201	sylbid	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (\sum_{G} ({(k \in C ⟼ j F k) ↾}_{(⋃ ran f \cup ran D)}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g) \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
203	138 202	syld	$⊢ ((φ \land j \in K) \land f : K ⟶ 𝒫 C \cap Fin) \to (\forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
204	203	an32s	$⊢ ((φ \land f : K ⟶ 𝒫 C \cap Fin) \land j \in K) \to (\forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
205	204	ralimdva	$⊢ (φ \land f : K ⟶ 𝒫 C \cap Fin) \to (\forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)) \to \forall j \in K H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L)$
206	205	impr	$⊢ (φ \land (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))) \to \forall j \in K H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L$
207		fveq2	$⊢ j = x \to H (j) = H (x)$
208		sneq	$⊢ j = x \to \{j\} = \{x\}$
209	208	xpeq1d	$⊢ j = x \to \{j\} \times (⋃ ran f \cup ran D) = \{x\} \times (⋃ ran f \cup ran D)$
210	209	reseq2d	$⊢ j = x \to {F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))} = {F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))}$
211	210	oveq2d	$⊢ j = x \to \sum_{G} ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))}) = \sum_{G} ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})$
212	207 211	oveq12d	$⊢ j = x \to H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) = H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))}))$
213	212	eleq1d	$⊢ j = x \to (H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L \leftrightarrow H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L)$
214	213	cbvralvw	$⊢ \forall j \in K H (j) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{j\} \times (⋃ ran f \cup ran D))})) \in L \leftrightarrow \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L$
215	206 214	sylib	$⊢ (φ \land (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))) \to \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L$
216		sseq2	$⊢ n = ⋃ ran f \cup ran D \to (ran D \subseteq n \leftrightarrow ran D \subseteq ⋃ ran f \cup ran D)$
217		xpeq2	$⊢ n = ⋃ ran f \cup ran D \to \{x\} \times n = \{x\} \times (⋃ ran f \cup ran D)$
218	217	reseq2d	$⊢ n = ⋃ ran f \cup ran D \to {F ↾}_{(\{x\} \times n)} = {F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))}$
219	218	oveq2d	$⊢ n = ⋃ ran f \cup ran D \to \sum_{G} ({F ↾}_{(\{x\} \times n)}) = \sum_{G} ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})$
220	219	oveq2d	$⊢ n = ⋃ ran f \cup ran D \to H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) = H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))}))$
221	220	eleq1d	$⊢ n = ⋃ ran f \cup ran D \to (H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L \leftrightarrow H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L)$
222	221	ralbidv	$⊢ n = ⋃ ran f \cup ran D \to (\forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L \leftrightarrow \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L)$
223	216 222	anbi12d	$⊢ n = ⋃ ran f \cup ran D \to ((ran D \subseteq n \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L) \leftrightarrow (ran D \subseteq ⋃ ran f \cup ran D \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L))$
224	223	rspcev	$⊢ (⋃ ran f \cup ran D \in (𝒫 C \cap Fin) \land (ran D \subseteq ⋃ ran f \cup ran D \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times (⋃ ran f \cup ran D))})) \in L)) \to \exists n \in (𝒫 C \cap Fin) (ran D \subseteq n \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L)$
225	122 124 215 224	syl12anc	$⊢ (φ \land (f : K ⟶ 𝒫 C \cap Fin \land \forall j \in K \forall z \in (𝒫 C \cap Fin) (f (j) \subseteq z \to \sum_{G} ({(k \in C ⟼ j F k) ↾}_{z}) \in ran (g \in L ⟼ H (j) \underset{˙}{-} g)))) \to \exists n \in (𝒫 C \cap Fin) (ran D \subseteq n \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L)$
226	88 225	exlimddv	$⊢ φ \to \exists n \in (𝒫 C \cap Fin) (ran D \subseteq n \land \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in L)$

Metamath Proof Explorer

Theorem tsmsxplem1

Proof