Theorem 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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝑍 ) )
	mptiffisupp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	mptiffisupp.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	mptiffisupp.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
	mptiffisupp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion	mptiffisupp	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		mptiffisupp.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝑍 ) )
2		mptiffisupp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		mptiffisupp.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
4		mptiffisupp.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
5		mptiffisupp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
6	2	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝑍 ) ) ∈ V )
7	1 6	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ V )
8	1	funmpt2	⊢ Fun 𝐹
9	8	a1i	⊢ ( 𝜑 → Fun 𝐹 )
10		partfun	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝑍 ) ) = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) )
11	1 10	eqtri	⊢ 𝐹 = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) )
12	11	oveq1i	⊢ ( 𝐹 supp 𝑍 ) = ( ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ) supp 𝑍 )
13		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
14	13	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
15	14	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
16	15 4	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ∈ 𝑉 )
17	16	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) : ( 𝐴 ∩ 𝐵 ) ⟶ 𝑉 )
18		incom	⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
19		infi	⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∩ 𝐴 ) ∈ Fin )
20	3 19	syl	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ∈ Fin )
21	18 20	eqeltrrid	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
22	17 21 5	fidmfisupp	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) finSupp 𝑍 )
23		difexg	⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ∖ 𝐵 ) ∈ V )
24		mptexg	⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ V → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∈ V )
25	2 23 24	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∈ V )
26		funmpt	⊢ Fun ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 )
27	26	a1i	⊢ ( 𝜑 → Fun ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) )
28		supppreima	⊢ ( ( Fun ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) supp 𝑍 ) = ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) )
29	26 25 5 28	mp3an2i	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) supp 𝑍 ) = ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) )
30		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ( 𝐴 ∖ 𝐵 ) = ∅ )
31	30	mpteq1d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) = ( 𝑥 ∈ ∅ ↦ 𝑍 ) )
32		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ 𝑍 ) = ∅
33	31 32	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) = ∅ )
34	33	cnveqd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) = ◡ ∅ )
35		cnv0	⊢ ◡ ∅ = ∅
36	34 35	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) = ∅ )
37	36	imaeq1d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) = ( ∅ “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) )
38		0ima	⊢ ( ∅ “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) = ∅
39	37 38	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) = ∅ ) → ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) = ∅ )
40		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) = ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 )
41		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ( 𝐴 ∖ 𝐵 ) ≠ ∅ )
42	40 41	rnmptc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) = { 𝑍 } )
43	42	difeq1d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) = ( { 𝑍 } ∖ { 𝑍 } ) )
44		difid	⊢ ( { 𝑍 } ∖ { 𝑍 } ) = ∅
45	43 44	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) = ∅ )
46	45	imaeq2d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) = ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ∅ ) )
47		ima0	⊢ ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ∅ ) = ∅
48	46 47	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) = ∅ )
49	39 48	pm2.61dane	⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) “ ( ran ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ∖ { 𝑍 } ) ) = ∅ )
50	29 49	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) supp 𝑍 ) = ∅ )
51		0fi	⊢ ∅ ∈ Fin
52	50 51	eqeltrdi	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) supp 𝑍 ) ∈ Fin )
53	25 5 27 52	isfsuppd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) finSupp 𝑍 )
54	22 53	fsuppun	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝑍 ) ) supp 𝑍 ) ∈ Fin )
55	12 54	eqeltrid	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
56	7 5 9 55	isfsuppd	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )