fdifsuppconst

Description: A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024)

		Ref	Expression
	Hypothesis	fdifsuppconst.1	⊢ 𝐴 = ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) )
	Assertion	fdifsuppconst	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) = ( 𝐴 × { 𝑍 } ) )

Proof

Step	Hyp	Ref	Expression
1		fdifsuppconst.1	⊢ 𝐴 = ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) )
2		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
3	2	biimpi	⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
4	3	ad2antrr	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) → 𝐹 Fn dom 𝐹 )
5		difssd	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ⊆ dom 𝐹 )
6	1 5	eqsstrid	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) → 𝐴 ⊆ dom 𝐹 )
7	4 6	fnssresd	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
8		fnconstg	⊢ ( 𝑍 ∈ 𝑊 → ( 𝐴 × { 𝑍 } ) Fn 𝐴 )
9	8	adantl	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) → ( 𝐴 × { 𝑍 } ) Fn 𝐴 )
10	4	adantr	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 Fn dom 𝐹 )
11		dmexg	⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
12	11	ad3antlr	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → dom 𝐹 ∈ V )
13		simplr	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑍 ∈ 𝑊 )
14	1	eleq2i	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) )
15	14	biimpi	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) )
16	15	adantl	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) )
17	10 12 13 16	fvdifsupp	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 )
18		simpr	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
19	18	fvresd	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
20		fvconst2g	⊢ ( ( 𝑍 ∈ 𝑊 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝑍 } ) ‘ 𝑥 ) = 𝑍 )
21	20	adantll	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝑍 } ) ‘ 𝑥 ) = 𝑍 )
22	17 19 21	3eqtr4d	⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐴 × { 𝑍 } ) ‘ 𝑥 ) )
23	7 9 22	eqfnfvd	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) = ( 𝐴 × { 𝑍 } ) )
24	23	3impa	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) = ( 𝐴 × { 𝑍 } ) )

Metamath Proof Explorer

Theorem fdifsuppconst

Proof