Metamath Proof Explorer


Theorem ofsubid

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

Ref Expression
Assertion ofsubid AVF:AFfF=A×0

Proof

Step Hyp Ref Expression
1 simpl AVF:AAV
2 ffn F:AFFnA
3 2 adantl AVF:AFFnA
4 c0ex 0V
5 4 fconst A×0:A0
6 ffn A×0:A0A×0FnA
7 5 6 mp1i AVF:AA×0FnA
8 eqidd AVF:AxAFx=Fx
9 ffvelcdm F:AxAFx
10 9 subidd F:AxAFxFx=0
11 10 adantll AVF:AxAFxFx=0
12 4 fvconst2 xAA×0x=0
13 12 adantl AVF:AxAA×0x=0
14 11 13 eqtr4d AVF:AxAFxFx=A×0x
15 1 3 3 7 8 8 14 offveq AVF:AFfF=A×0