gsum2d2lem

Description: Lemma for gsum2d2 : show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Hypotheses	gsum2d2.b	$⊢ B = {Base}_{G}$
	gsum2d2.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsum2d2.g	$⊢ φ \to G \in CMnd$
	gsum2d2.a	$⊢ φ \to A \in V$
	gsum2d2.r	$⊢ (φ \land j \in A) \to C \in W$
	gsum2d2.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
	gsum2d2.u	$⊢ φ \to U \in Fin$
	gsum2d2.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
Assertion	gsum2d2lem	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((j \in A, k \in C ⟼ X))$

Proof

Step	Hyp	Ref	Expression
1		gsum2d2.b	$⊢ B = {Base}_{G}$
2		gsum2d2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsum2d2.g	$⊢ φ \to G \in CMnd$
4		gsum2d2.a	$⊢ φ \to A \in V$
5		gsum2d2.r	$⊢ (φ \land j \in A) \to C \in W$
6		gsum2d2.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
7		gsum2d2.u	$⊢ φ \to U \in Fin$
8		gsum2d2.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
9		eqid	$⊢ (j \in A, k \in C ⟼ X) = (j \in A, k \in C ⟼ X)$
10	9	mpofun	$⊢ Fun (j \in A, k \in C ⟼ X)$
11	10	a1i	$⊢ φ \to Fun (j \in A, k \in C ⟼ X)$
12	6	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in C X \in B$
13	9	fmpox	$⊢ \forall j \in A \forall k \in C X \in B \leftrightarrow (j \in A, k \in C ⟼ X) : ⋃_{j \in A} (\{j\} \times C) ⟶ B$
14	12 13	sylib	$⊢ φ \to (j \in A, k \in C ⟼ X) : ⋃_{j \in A} (\{j\} \times C) ⟶ B$
15		nfv	$⊢ Ⅎ j φ$
16		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times C)$
17		nfcv	$⊢ \underline{Ⅎ} j U$
18	16 17	nfdif	$⊢ \underline{Ⅎ} j (⋃_{j \in A} (\{j\} \times C) ∖ U)$
19	18	nfcri	$⊢ Ⅎ j z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)$
20	15 19	nfan	$⊢ Ⅎ j (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U))$
21		nfmpo1	$⊢ \underline{Ⅎ} j (j \in A, k \in C ⟼ X)$
22		nfcv	$⊢ \underline{Ⅎ} j z$
23	21 22	nffv	$⊢ \underline{Ⅎ} j (j \in A, k \in C ⟼ X) (z)$
24	23	nfeq1	$⊢ Ⅎ j (j \in A, k \in C ⟼ X) (z) = \underset{˙}{0}$
25		relxp	$⊢ Rel (\{j\} \times C)$
26	25	rgenw	$⊢ \forall j \in A Rel (\{j\} \times C)$
27		reliun	$⊢ Rel ⋃_{j \in A} (\{j\} \times C) \leftrightarrow \forall j \in A Rel (\{j\} \times C)$
28	26 27	mpbir	$⊢ Rel ⋃_{j \in A} (\{j\} \times C)$
29		eldifi	$⊢ z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \to z \in ⋃_{j \in A} (\{j\} \times C)$
30	29	adantl	$⊢ (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)) \to z \in ⋃_{j \in A} (\{j\} \times C)$
31		elrel	$⊢ (Rel ⋃_{j \in A} (\{j\} \times C) \land z \in ⋃_{j \in A} (\{j\} \times C)) \to \exists j \exists k z = ⟨j, k⟩$
32	28 30 31	sylancr	$⊢ (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)) \to \exists j \exists k z = ⟨j, k⟩$
33		nfv	$⊢ Ⅎ k (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U))$
34		nfmpo2	$⊢ \underline{Ⅎ} k (j \in A, k \in C ⟼ X)$
35		nfcv	$⊢ \underline{Ⅎ} k z$
36	34 35	nffv	$⊢ \underline{Ⅎ} k (j \in A, k \in C ⟼ X) (z)$
37	36	nfeq1	$⊢ Ⅎ k (j \in A, k \in C ⟼ X) (z) = \underset{˙}{0}$
38		simprr	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to z = ⟨j, k⟩$
39	38	fveq2d	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to (j \in A, k \in C ⟼ X) (z) = (j \in A, k \in C ⟼ X) (⟨j, k⟩)$
40		df-ov	$⊢ j (j \in A, k \in C ⟼ X) k = (j \in A, k \in C ⟼ X) (⟨j, k⟩)$
41		simprl	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)$
42	38 41	eqeltrrd	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to ⟨j, k⟩ \in (⋃_{j \in A} (\{j\} \times C) ∖ U)$
43	42	eldifad	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to ⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C)$
44		opeliunxp	$⊢ ⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow (j \in A \land k \in C)$
45	43 44	sylib	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to (j \in A \land k \in C)$
46	45	simpld	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to j \in A$
47	45	simprd	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to k \in C$
48	45 6	syldan	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to X \in B$
49	9	ovmpt4g	$⊢ (j \in A \land k \in C \land X \in B) \to j (j \in A, k \in C ⟼ X) k = X$
50	46 47 48 49	syl3anc	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to j (j \in A, k \in C ⟼ X) k = X$
51	40 50	syl5eqr	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to (j \in A, k \in C ⟼ X) (⟨j, k⟩) = X$
52		eldifn	$⊢ z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \to \neg z \in U$
53	52	ad2antrl	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to \neg z \in U$
54	38	eleq1d	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to (z \in U \leftrightarrow ⟨j, k⟩ \in U)$
55		df-br	$⊢ j U k \leftrightarrow ⟨j, k⟩ \in U$
56	54 55	bitr4di	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to (z \in U \leftrightarrow j U k)$
57	53 56	mtbid	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to \neg j U k$
58	45 57	jca	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to ((j \in A \land k \in C) \land \neg j U k)$
59	58 8	syldan	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to X = \underset{˙}{0}$
60	39 51 59	3eqtrd	$⊢ (φ \land (z \in (⋃_{j \in A} (\{j\} \times C) ∖ U) \land z = ⟨j, k⟩)) \to (j \in A, k \in C ⟼ X) (z) = \underset{˙}{0}$
61	60	expr	$⊢ (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)) \to (z = ⟨j, k⟩ \to (j \in A, k \in C ⟼ X) (z) = \underset{˙}{0})$
62	33 37 61	exlimd	$⊢ (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)) \to (\exists k z = ⟨j, k⟩ \to (j \in A, k \in C ⟼ X) (z) = \underset{˙}{0})$
63	20 24 32 62	exlimimdd	$⊢ (φ \land z \in (⋃_{j \in A} (\{j\} \times C) ∖ U)) \to (j \in A, k \in C ⟼ X) (z) = \underset{˙}{0}$
64	14 63	suppss	$⊢ φ \to (j \in A, k \in C ⟼ X) supp \underset{˙}{0} \subseteq U$
65	7 64	ssfid	$⊢ φ \to (j \in A, k \in C ⟼ X) supp \underset{˙}{0} \in Fin$
66	5	ralrimiva	$⊢ φ \to \forall j \in A C \in W$
67	9	mpoexxg	$⊢ (A \in V \land \forall j \in A C \in W) \to (j \in A, k \in C ⟼ X) \in V$
68	4 66 67	syl2anc	$⊢ φ \to (j \in A, k \in C ⟼ X) \in V$
69	2	fvexi	$⊢ \underset{˙}{0} \in V$
70	69	a1i	$⊢ φ \to \underset{˙}{0} \in V$
71		isfsupp	$⊢ ((j \in A, k \in C ⟼ X) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((j \in A, k \in C ⟼ X)) \leftrightarrow (Fun (j \in A, k \in C ⟼ X) \land (j \in A, k \in C ⟼ X) supp \underset{˙}{0} \in Fin))$
72	68 70 71	syl2anc	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} ((j \in A, k \in C ⟼ X)) \leftrightarrow (Fun (j \in A, k \in C ⟼ X) \land (j \in A, k \in C ⟼ X) supp \underset{˙}{0} \in Fin))$
73	11 65 72	mpbir2and	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((j \in A, k \in C ⟼ X))$

Metamath Proof Explorer

Theorem gsum2d2lem

Proof