Metamath Proof Explorer

Theorem ofsubeq0

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

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

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
2 1 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐹 Fn 𝐴 )
3 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐺 : 𝐴 ⟶ ℂ )
4 3 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐺 Fn 𝐴 )
5 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐴 ∈ 𝑉 )
6 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
7 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
9 2 4 5 5 6 7 8 ofval ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
10 c0ex ⊢ 0 ∈ V
11 10 fvconst2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
13 9 12 eqeq12d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) = 0 ) )
14 1 ffvelrnda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
15 3 ffvelrnda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
16 14 15 subeq0ad ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
17 13 16 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
18 17 ralbidva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
19 2 4 5 5 6 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f − 𝐺 ) Fn 𝐴 )
20 10 fconst ⊢ ( 𝐴 × { 0 } ) : 𝐴 ⟶ { 0 }
21 ffn ⊢ ( ( 𝐴 × { 0 } ) : 𝐴 ⟶ { 0 } → ( 𝐴 × { 0 } ) Fn 𝐴 )
22 20 21 ax-mp ⊢ ( 𝐴 × { 0 } ) Fn 𝐴
23 eqfnfv ⊢ ( ( ( 𝐹 ∘f − 𝐺 ) Fn 𝐴 ∧ ( 𝐴 × { 0 } ) Fn 𝐴 ) → ( ( 𝐹 ∘f − 𝐺 ) = ( 𝐴 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) )
24 19 22 23 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ( 𝐹 ∘f − 𝐺 ) = ( 𝐴 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) )
25 eqfnfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
26 2 4 25 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
27 18 24 26 3bitr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ( 𝐹 ∘f − 𝐺 ) = ( 𝐴 × { 0 } ) ↔ 𝐹 = 𝐺 ) )