Metamath Proof Explorer

Theorem ofnegsub

Description: Function analogue of negsub . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion ofnegsub ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f + ( ( 𝐴 × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐴 ∈ 𝑉 )
2 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
3 2 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐹 Fn 𝐴 )
4 ax-1cn ⊢ 1 ∈ ℂ
5 4 negcli ⊢ - 1 ∈ ℂ
6 fnconstg ⊢ ( - 1 ∈ ℂ → ( 𝐴 × { - 1 } ) Fn 𝐴 )
7 5 6 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐴 × { - 1 } ) Fn 𝐴 )
8 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐺 : 𝐴 ⟶ ℂ )
9 8 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐺 Fn 𝐴 )
10 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
11 7 9 1 1 10 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ( 𝐴 × { - 1 } ) ∘f · 𝐺 ) Fn 𝐴 )
12 3 9 1 1 10 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f − 𝐺 ) Fn 𝐴 )
13 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 5 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → - 1 ∈ ℂ )
15 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16 1 14 9 15 ofc1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐴 × { - 1 } ) ∘f · 𝐺 ) ‘ 𝑥 ) = ( - 1 · ( 𝐺 ‘ 𝑥 ) ) )
17 8 ffvelrnda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
18 17 mulm1d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( - 1 · ( 𝐺 ‘ 𝑥 ) ) = - ( 𝐺 ‘ 𝑥 ) )
19 16 18 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐴 × { - 1 } ) ∘f · 𝐺 ) ‘ 𝑥 ) = - ( 𝐺 ‘ 𝑥 ) )
20 2 ffvelrnda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
21 20 17 negsubd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) + - ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
22 3 9 1 1 10 13 15 ofval ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
23 21 22 eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) + - ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) )
24 1 3 11 12 13 19 23 offveq ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f + ( ( 𝐴 × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )