Theorem ofsubid

Description: Function analogue of subid . (Contributed by Steve Rodriguez, 5-Nov-2015)

	Ref	Expression
Assertion	ofsubid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f − 𝐹 ) = ( 𝐴 × { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐴 ∈ 𝑉 )
2		ffn	⊢ ( 𝐹 : 𝐴 ⟶ ℂ → 𝐹 Fn 𝐴 )
3	2	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 Fn 𝐴 )
4		c0ex	⊢ 0 ∈ V
5	4	fconst	⊢ ( 𝐴 × { 0 } ) : 𝐴 ⟶ { 0 }
6		ffn	⊢ ( ( 𝐴 × { 0 } ) : 𝐴 ⟶ { 0 } → ( 𝐴 × { 0 } ) Fn 𝐴 )
7	5 6	mp1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐴 × { 0 } ) Fn 𝐴 )
8		eqidd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9		ffvelcdm	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
10	9	subidd	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) = 0 )
11	10	adantll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) = 0 )
12	4	fvconst2	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
13	12	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
14	11 13	eqtr4d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) )
15	1 3 3 7 8 8 14	offveq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f − 𝐹 ) = ( 𝐴 × { 0 } ) )