# Metamath Proof Explorer

## Theorem ofsubeq0

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

Ref Expression
Assertion ofsubeq0 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to \left({F}{-}_{f}{G}={A}×\left\{0\right\}↔{F}={G}\right)$

### Proof

Step Hyp Ref Expression
1 simp2 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to {F}:{A}⟶ℂ$
2 1 ffnd ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to {F}Fn{A}$
3 simp3 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to {G}:{A}⟶ℂ$
4 3 ffnd ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to {G}Fn{A}$
5 simp1 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to {A}\in {V}$
6 inidm ${⊢}{A}\cap {A}={A}$
7 eqidd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)={F}\left({x}\right)$
8 eqidd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to {G}\left({x}\right)={G}\left({x}\right)$
9 2 4 5 5 6 7 8 ofval ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to \left({F}{-}_{f}{G}\right)\left({x}\right)={F}\left({x}\right)-{G}\left({x}\right)$
10 c0ex ${⊢}0\in \mathrm{V}$
11 10 fvconst2 ${⊢}{x}\in {A}\to \left({A}×\left\{0\right\}\right)\left({x}\right)=0$
12 11 adantl ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to \left({A}×\left\{0\right\}\right)\left({x}\right)=0$
13 9 12 eqeq12d ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to \left(\left({F}{-}_{f}{G}\right)\left({x}\right)=\left({A}×\left\{0\right\}\right)\left({x}\right)↔{F}\left({x}\right)-{G}\left({x}\right)=0\right)$
14 1 ffvelrnda ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in ℂ$
15 3 ffvelrnda ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to {G}\left({x}\right)\in ℂ$
16 14 15 subeq0ad ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)-{G}\left({x}\right)=0↔{F}\left({x}\right)={G}\left({x}\right)\right)$
17 13 16 bitrd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\wedge {x}\in {A}\right)\to \left(\left({F}{-}_{f}{G}\right)\left({x}\right)=\left({A}×\left\{0\right\}\right)\left({x}\right)↔{F}\left({x}\right)={G}\left({x}\right)\right)$
18 17 ralbidva ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}{-}_{f}{G}\right)\left({x}\right)=\left({A}×\left\{0\right\}\right)\left({x}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
19 2 4 5 5 6 offn ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to \left({F}{-}_{f}{G}\right)Fn{A}$
20 10 fconst ${⊢}\left({A}×\left\{0\right\}\right):{A}⟶\left\{0\right\}$
21 ffn ${⊢}\left({A}×\left\{0\right\}\right):{A}⟶\left\{0\right\}\to \left({A}×\left\{0\right\}\right)Fn{A}$
22 20 21 ax-mp ${⊢}\left({A}×\left\{0\right\}\right)Fn{A}$
23 eqfnfv ${⊢}\left(\left({F}{-}_{f}{G}\right)Fn{A}\wedge \left({A}×\left\{0\right\}\right)Fn{A}\right)\to \left({F}{-}_{f}{G}={A}×\left\{0\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}{-}_{f}{G}\right)\left({x}\right)=\left({A}×\left\{0\right\}\right)\left({x}\right)\right)$
24 19 22 23 sylancl ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to \left({F}{-}_{f}{G}={A}×\left\{0\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}{-}_{f}{G}\right)\left({x}\right)=\left({A}×\left\{0\right\}\right)\left({x}\right)\right)$
25 eqfnfv ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
26 2 4 25 syl2anc ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
27 18 24 26 3bitr4d ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶ℂ\wedge {G}:{A}⟶ℂ\right)\to \left({F}{-}_{f}{G}={A}×\left\{0\right\}↔{F}={G}\right)$