let A be symmetrical Subset of COMPLEX; for F being PartFunc of REAL,REAL holds
( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )
let F be PartFunc of REAL,REAL; ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )
A1:
( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) implies F is_even_on A )
proof
assume that A2:
A c= dom F
and A3:
for
x being
Real st
x in A holds
(F . x) - (F . (- x)) = 0
;
F is_even_on A
A4:
dom (F | A) = A
by A2, RELAT_1:62;
A5:
for
x being
Real st
x in A holds
F . (- x) = F . x
proof
let x be
Real;
( x in A implies F . (- x) = F . x )
assume
x in A
;
F . (- x) = F . x
then
(F . x) - (F . (- x)) = 0
by A3;
hence
F . (- x) = F . x
;
verum
end;
for
x being
Real st
x in dom (F | A) &
- x in dom (F | A) holds
(F | A) . (- x) = (F | A) . x
proof
let x be
Real;
( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x )
assume that A6:
x in dom (F | A)
and A7:
- x in dom (F | A)
;
(F | A) . (- x) = (F | A) . x
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
(F | A) . (- x) =
(F | A) /. (- x)
by A7, PARTFUN1:def 6
.=
F /. (- x)
by A2, A4, A7, PARTFUN2:17
.=
F . (- x)
by A2, A7, PARTFUN1:def 6
.=
F . x
by A5, A6
.=
F /. x
by A2, A6, PARTFUN1:def 6
.=
(F | A) /. x
by A2, A4, A6, PARTFUN2:17
.=
(F | A) . x
by A6, PARTFUN1:def 6
;
hence
(F | A) . (- x) = (F | A) . x
;
verum
end;
then
(
F | A is
with_symmetrical_domain &
F | A is
quasi_even )
by A4;
hence
F is_even_on A
by A2;
verum
end;
( F is_even_on A implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )
proof
assume A8:
F is_even_on A
;
( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) )
then A9:
A c= dom F
;
A10:
F | A is
even
by A8;
for
x being
Real st
x in A holds
(F . x) - (F . (- x)) = 0
proof
let x be
Real;
( x in A implies (F . x) - (F . (- x)) = 0 )
assume A11:
x in A
;
(F . x) - (F . (- x)) = 0
then A12:
x in dom (F | A)
by A9, RELAT_1:62;
A13:
- x in A
by A11, Def1;
then A14:
- x in dom (F | A)
by A9, RELAT_1:62;
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
(F . x) - (F . (- x)) =
(F /. x) - (F . (- x))
by A9, A11, PARTFUN1:def 6
.=
(F /. x) - (F /. (- x))
by A9, A13, PARTFUN1:def 6
.=
((F | A) /. x) - (F /. (- x))
by A9, A11, PARTFUN2:17
.=
((F | A) /. x) - ((F | A) /. (- x))
by A9, A13, PARTFUN2:17
.=
((F | A) . x) - ((F | A) /. (- x))
by A12, PARTFUN1:def 6
.=
((F | A) . x) - ((F | A) . (- x))
by A14, PARTFUN1:def 6
.=
((F | A) . x) - ((F | A) . x)
by A10, A12, A14, Def3
.=
0
;
hence
(F . x) - (F . (- x)) = 0
;
verum
end;
hence
(
A c= dom F & ( for
x being
Real st
x in A holds
(F . x) - (F . (- x)) = 0 ) )
by A8;
verum
end;
hence
( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )
by A1; verum