mptiffisupp

Description: Conditions for a mapping function defined with a conditional to have finite support. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	mptiffisupp.f	$⊢ F = (x \in A ⟼ if (x \in B, C, Z))$
	mptiffisupp.a	$⊢ φ \to A \in U$
	mptiffisupp.b	$⊢ φ \to B \in Fin$
	mptiffisupp.c	$⊢ (φ \land x \in B) \to C \in V$
	mptiffisupp.z	$⊢ φ \to Z \in W$
Assertion	mptiffisupp	$⊢ φ \to {finSupp}_{Z} (F)$

Proof

Step	Hyp	Ref	Expression
1		mptiffisupp.f	$⊢ F = (x \in A ⟼ if (x \in B, C, Z))$
2		mptiffisupp.a	$⊢ φ \to A \in U$
3		mptiffisupp.b	$⊢ φ \to B \in Fin$
4		mptiffisupp.c	$⊢ (φ \land x \in B) \to C \in V$
5		mptiffisupp.z	$⊢ φ \to Z \in W$
6	2	mptexd	$⊢ φ \to (x \in A ⟼ if (x \in B, C, Z)) \in V$
7	1 6	eqeltrid	$⊢ φ \to F \in V$
8	1	funmpt2	$⊢ Fun F$
9	8	a1i	$⊢ φ \to Fun F$
10		partfun	$⊢ (x \in A ⟼ if (x \in B, C, Z)) = (x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ Z)$
11	1 10	eqtri	$⊢ F = (x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ Z)$
12	11	oveq1i	$⊢ F supp Z = ((x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ Z)) supp Z$
13		inss2	$⊢ A \cap B \subseteq B$
14	13	a1i	$⊢ φ \to A \cap B \subseteq B$
15	14	sselda	$⊢ (φ \land x \in (A \cap B)) \to x \in B$
16	15 4	syldan	$⊢ (φ \land x \in (A \cap B)) \to C \in V$
17	16	fmpttd	$⊢ φ \to (x \in (A \cap B) ⟼ C) : A \cap B ⟶ V$
18		incom	$⊢ B \cap A = A \cap B$
19		infi	$⊢ B \in Fin \to B \cap A \in Fin$
20	3 19	syl	$⊢ φ \to B \cap A \in Fin$
21	18 20	eqeltrrid	$⊢ φ \to A \cap B \in Fin$
22	17 21 5	fidmfisupp	$⊢ φ \to {finSupp}_{Z} ((x \in (A \cap B) ⟼ C))$
23		difexg	$⊢ A \in U \to A ∖ B \in V$
24		mptexg	$⊢ A ∖ B \in V \to (x \in (A ∖ B) ⟼ Z) \in V$
25	2 23 24	3syl	$⊢ φ \to (x \in (A ∖ B) ⟼ Z) \in V$
26		funmpt	$⊢ Fun (x \in (A ∖ B) ⟼ Z)$
27	26	a1i	$⊢ φ \to Fun (x \in (A ∖ B) ⟼ Z)$
28		supppreima	$⊢ (Fun (x \in (A ∖ B) ⟼ Z) \land (x \in (A ∖ B) ⟼ Z) \in V \land Z \in W) \to (x \in (A ∖ B) ⟼ Z) supp Z = {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}]$
29	26 25 5 28	mp3an2i	$⊢ φ \to (x \in (A ∖ B) ⟼ Z) supp Z = {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}]$
30		simpr	$⊢ (φ \land A ∖ B = \emptyset) \to A ∖ B = \emptyset$
31	30	mpteq1d	$⊢ (φ \land A ∖ B = \emptyset) \to (x \in (A ∖ B) ⟼ Z) = (x \in \emptyset ⟼ Z)$
32		mpt0	$⊢ (x \in \emptyset ⟼ Z) = \emptyset$
33	31 32	eqtrdi	$⊢ (φ \land A ∖ B = \emptyset) \to (x \in (A ∖ B) ⟼ Z) = \emptyset$
34	33	cnveqd	$⊢ (φ \land A ∖ B = \emptyset) \to {(x \in (A ∖ B) ⟼ Z)}^{-1} = \emptyset^{-1}$
35		cnv0	$⊢ \emptyset^{-1} = \emptyset$
36	34 35	eqtrdi	$⊢ (φ \land A ∖ B = \emptyset) \to {(x \in (A ∖ B) ⟼ Z)}^{-1} = \emptyset$
37	36	imaeq1d	$⊢ (φ \land A ∖ B = \emptyset) \to {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}] = \emptyset [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}]$
38		0ima	$⊢ \emptyset [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}] = \emptyset$
39	37 38	eqtrdi	$⊢ (φ \land A ∖ B = \emptyset) \to {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}] = \emptyset$
40		eqid	$⊢ (x \in (A ∖ B) ⟼ Z) = (x \in (A ∖ B) ⟼ Z)$
41		simpr	$⊢ (φ \land A ∖ B \neq \emptyset) \to A ∖ B \neq \emptyset$
42	40 41	rnmptc	$⊢ (φ \land A ∖ B \neq \emptyset) \to ran (x \in (A ∖ B) ⟼ Z) = \{Z\}$
43	42	difeq1d	$⊢ (φ \land A ∖ B \neq \emptyset) \to ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\} = \{Z\} ∖ \{Z\}$
44		difid	$⊢ \{Z\} ∖ \{Z\} = \emptyset$
45	43 44	eqtrdi	$⊢ (φ \land A ∖ B \neq \emptyset) \to ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\} = \emptyset$
46	45	imaeq2d	$⊢ (φ \land A ∖ B \neq \emptyset) \to {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}] = {(x \in (A ∖ B) ⟼ Z)}^{-1} [\emptyset]$
47		ima0	$⊢ {(x \in (A ∖ B) ⟼ Z)}^{-1} [\emptyset] = \emptyset$
48	46 47	eqtrdi	$⊢ (φ \land A ∖ B \neq \emptyset) \to {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}] = \emptyset$
49	39 48	pm2.61dane	$⊢ φ \to {(x \in (A ∖ B) ⟼ Z)}^{-1} [ran (x \in (A ∖ B) ⟼ Z) ∖ \{Z\}] = \emptyset$
50	29 49	eqtrd	$⊢ φ \to (x \in (A ∖ B) ⟼ Z) supp Z = \emptyset$
51		0fin	$⊢ \emptyset \in Fin$
52	50 51	eqeltrdi	$⊢ φ \to (x \in (A ∖ B) ⟼ Z) supp Z \in Fin$
53	25 5 27 52	isfsuppd	$⊢ φ \to {finSupp}_{Z} ((x \in (A ∖ B) ⟼ Z))$
54	22 53	fsuppun	$⊢ φ \to ((x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ Z)) supp Z \in Fin$
55	12 54	eqeltrid	$⊢ φ \to F supp Z \in Fin$
56	7 5 9 55	isfsuppd	$⊢ φ \to {finSupp}_{Z} (F)$

Metamath Proof Explorer

Theorem mptiffisupp

Proof