:: FUNCT_8 semantic presentation
begin
definition
let A be set ;
attrA is symmetrical means :Def1: :: FUNCT_8:def 1
for x being complex number st x in A holds
- x in A;
end;
:: deftheorem Def1 defines symmetrical FUNCT_8:def_1_:_
for A being set holds
( A is symmetrical iff for x being complex number st x in A holds
- x in A );
registration
cluster complex-membered symmetrical for Element of K6(COMPLEX);
existence
ex b1 being Subset of COMPLEX st b1 is symmetrical
proof
take [#] COMPLEX ; ::_thesis: [#] COMPLEX is symmetrical
let x be complex number ; :: according to FUNCT_8:def_1 ::_thesis: ( x in [#] COMPLEX implies - x in [#] COMPLEX )
thus ( x in [#] COMPLEX implies - x in [#] COMPLEX ) by XCMPLX_0:def_2; ::_thesis: verum
end;
end;
registration
cluster complex-membered ext-real-membered real-membered symmetrical for Element of K6(REAL);
existence
ex b1 being Subset of REAL st b1 is symmetrical
proof
take [#] REAL ; ::_thesis: [#] REAL is symmetrical
let x be complex number ; :: according to FUNCT_8:def_1 ::_thesis: ( x in [#] REAL implies - x in [#] REAL )
for x being Real st x in REAL holds
- x in REAL ;
hence ( x in [#] REAL implies - x in [#] REAL ) ; ::_thesis: verum
end;
end;
definition
let R be Relation;
attrR is with_symmetrical_domain means :Def2: :: FUNCT_8:def 2
dom R is symmetrical ;
end;
:: deftheorem Def2 defines with_symmetrical_domain FUNCT_8:def_2_:_
for R being Relation holds
( R is with_symmetrical_domain iff dom R is symmetrical );
registration
cluster empty Relation-like -> with_symmetrical_domain for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is with_symmetrical_domain
proof
A1: {} is symmetrical
proof
assume not {} is symmetrical ; ::_thesis: contradiction
then ex x being complex number st
( x in {} & not - x in {} ) by Def1;
hence contradiction ; ::_thesis: verum
end;
dom {} = {} ;
hence for b1 being Relation st b1 is empty holds
b1 is with_symmetrical_domain by A1, Def2; ::_thesis: verum
end;
end;
registration
let R be with_symmetrical_domain Relation;
cluster dom R -> symmetrical ;
coherence
dom R is symmetrical by Def2;
end;
definition
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
attrF is quasi_even means :Def3: :: FUNCT_8:def 3
for x being Real st x in dom F & - x in dom F holds
F . (- x) = F . x;
end;
:: deftheorem Def3 defines quasi_even FUNCT_8:def_3_:_
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is quasi_even iff for x being Real st x in dom F & - x in dom F holds
F . (- x) = F . x );
definition
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
attrF is even means :Def4: :: FUNCT_8:def 4
( F is with_symmetrical_domain & F is quasi_even );
end;
:: deftheorem Def4 defines even FUNCT_8:def_4_:_
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is even iff ( F is with_symmetrical_domain & F is quasi_even ) );
registration
let X, Y be complex-membered set ;
cluster Function-like with_symmetrical_domain quasi_even -> even for Element of K6(K7(X,Y));
coherence
for b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_even holds
b1 is even by Def4;
cluster Function-like even -> with_symmetrical_domain quasi_even for Element of K6(K7(X,Y));
coherence
for b1 being PartFunc of X,Y st b1 is even holds
( b1 is with_symmetrical_domain & b1 is quasi_even ) by Def4;
end;
definition
let A be set ;
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
predF is_even_on A means :Def5: :: FUNCT_8:def 5
( A c= dom F & F | A is even );
end;
:: deftheorem Def5 defines is_even_on FUNCT_8:def_5_:_
for A being set
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is_even_on A iff ( A c= dom F & F | A is even ) );
definition
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
attrF is quasi_odd means :Def6: :: FUNCT_8:def 6
for x being Real st x in dom F & - x in dom F holds
F . (- x) = - (F . x);
end;
:: deftheorem Def6 defines quasi_odd FUNCT_8:def_6_:_
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is quasi_odd iff for x being Real st x in dom F & - x in dom F holds
F . (- x) = - (F . x) );
definition
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
attrF is odd means :Def7: :: FUNCT_8:def 7
( F is with_symmetrical_domain & F is quasi_odd );
end;
:: deftheorem Def7 defines odd FUNCT_8:def_7_:_
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is odd iff ( F is with_symmetrical_domain & F is quasi_odd ) );
registration
let X, Y be complex-membered set ;
cluster Function-like with_symmetrical_domain quasi_odd -> odd for Element of K6(K7(X,Y));
coherence
for b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_odd holds
b1 is odd by Def7;
cluster Function-like odd -> with_symmetrical_domain quasi_odd for Element of K6(K7(X,Y));
coherence
for b1 being PartFunc of X,Y st b1 is odd holds
( b1 is with_symmetrical_domain & b1 is quasi_odd ) by Def7;
end;
definition
let A be set ;
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
predF is_odd_on A means :Def8: :: FUNCT_8:def 8
( A c= dom F & F | A is odd );
end;
:: deftheorem Def8 defines is_odd_on FUNCT_8:def_8_:_
for A being set
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is_odd_on A iff ( A c= dom F & F | A is odd ) );
theorem :: FUNCT_8:1
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL holds
( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) + (F . (- x)) = 0 ) ) )
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL holds
( F is_odd_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; ::_thesis: ( F is_odd_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_odd_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 ; ::_thesis: F is_odd_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; ::_thesis: ( x in A implies F . (- x) = - (F . x) )
assume x in A ; ::_thesis: F . (- x) = - (F . x)
then (F . x) + (F . (- x)) = 0 by A3;
hence F . (- x) = - (F . x) ; ::_thesis: 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; ::_thesis: ( 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) ; ::_thesis: (F | A) . (- x) = - ((F | A) . x)
(F | A) . (- x) = (F | A) /. (- x) by A7, PARTFUN1:def_6
.= F /. (- x) by A2, A4, A7, PARTFUN2:17
.= F . (- x) by A2, A4, A7, PARTFUN1:def_6
.= - (F . x) by A5, A6
.= - (F /. x) by A2, A4, 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) ; ::_thesis: verum
end;
then ( F | A is with_symmetrical_domain & F | A is quasi_odd ) by A4, Def2, Def6;
hence F is_odd_on A by A2, Def8; ::_thesis: verum
end;
( F is_odd_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_odd_on A ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) + (F . (- x)) = 0 ) )
then A9: A c= dom F by Def8;
A10: F | A is odd by A8, Def8;
for x being Real st x in A holds
(F . x) + (F . (- x)) = 0
proof
let x be Real; ::_thesis: ( x in A implies (F . x) + (F . (- x)) = 0 )
assume A11: x in A ; ::_thesis: (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;
(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 A14, PARTFUN1:def_6
.= ((F | A) . x) + ((F | A) . (- x)) by A12, PARTFUN1:def_6
.= ((F | A) . x) + (- ((F | A) . x)) by A10, A12, A14, Def6
.= 0 ;
hence (F . x) + (F . (- x)) = 0 ; ::_thesis: verum
end;
hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) + (F . (- x)) = 0 ) ) by A8, Def8; ::_thesis: verum
end;
hence ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) + (F . (- x)) = 0 ) ) ) by A1; ::_thesis: verum
end;
theorem :: FUNCT_8:2
for A being 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 ) ) )
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: 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; ::_thesis: ( x in A implies F . (- x) = F . x )
assume x in A ; ::_thesis: F . (- x) = F . x
then (F . x) - (F . (- x)) = 0 by A3;
hence F . (- x) = F . x ; ::_thesis: 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; ::_thesis: ( 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) ; ::_thesis: (F | A) . (- x) = (F | A) . x
(F | A) . (- x) = (F | A) /. (- x) by A7, PARTFUN1:def_6
.= F /. (- x) by A2, A4, A7, PARTFUN2:17
.= F . (- x) by A2, A4, A7, PARTFUN1:def_6
.= F . x by A5, A6
.= F /. x by A2, A4, 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 ; ::_thesis: verum
end;
then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A4, Def2, Def3;
hence F is_even_on A by A2, Def5; ::_thesis: 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 ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) )
then A9: A c= dom F by Def5;
A10: F | A is even by A8, Def5;
for x being Real st x in A holds
(F . x) - (F . (- x)) = 0
proof
let x be Real; ::_thesis: ( x in A implies (F . x) - (F . (- x)) = 0 )
assume A11: x in A ; ::_thesis: (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;
(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 ; ::_thesis: verum
end;
hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) by A8, Def5; ::_thesis: 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; ::_thesis: verum
end;
theorem :: FUNCT_8:3
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) )
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) )
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & ( for x being Real st x in A holds
F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) ) )
assume that
A1: F is_odd_on A and
A2: for x being Real st x in A holds
F . x <> 0 ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) )
A3: A c= dom F by A1, Def8;
A4: F | A is odd by A1, Def8;
for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1
proof
let x be Real; ::_thesis: ( x in A implies (F . x) / (F . (- x)) = - 1 )
assume A5: x in A ; ::_thesis: (F . x) / (F . (- x)) = - 1
then A6: x in dom (F | A) by A3, RELAT_1:62;
A7: F . x = F /. x by A3, A5, PARTFUN1:def_6
.= (F | A) /. x by A3, A5, PARTFUN2:17
.= (F | A) . x by A6, PARTFUN1:def_6 ;
A8: - x in A by A5, Def1;
then A9: - x in dom (F | A) by A3, RELAT_1:62;
(F . x) / (F . (- x)) = (F /. x) / (F . (- x)) by A3, A5, PARTFUN1:def_6
.= (F /. x) / (F /. (- x)) by A3, A8, PARTFUN1:def_6
.= ((F | A) /. x) / (F /. (- x)) by A3, A5, PARTFUN2:17
.= ((F | A) /. x) / ((F | A) /. (- x)) by A3, A8, PARTFUN2:17
.= ((F | A) . x) / ((F | A) /. (- x)) by A6, PARTFUN1:def_6
.= ((F | A) . x) / ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= ((F | A) . x) / (- ((F | A) . x)) by A4, A6, A9, Def6
.= - (((F | A) . x) / ((F | A) . x)) by XCMPLX_1:188
.= - 1 by A2, A5, A7, XCMPLX_1:60 ;
hence (F . x) / (F . (- x)) = - 1 ; ::_thesis: verum
end;
hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) ) by A1, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:4
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) holds
F is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) holds
F is_odd_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) implies F is_odd_on A )
assume that
A1: A c= dom F and
A2: for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ; ::_thesis: F is_odd_on A
A3: dom (F | A) = A by A1, RELAT_1:62;
A4: for x being Real st x in A holds
F . (- x) = - (F . x)
proof
let x be Real; ::_thesis: ( x in A implies F . (- x) = - (F . x) )
assume x in A ; ::_thesis: F . (- x) = - (F . x)
then (F . x) / (F . (- x)) = - 1 by A2;
hence F . (- x) = - (F . x) by XCMPLX_1:195; ::_thesis: 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; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = - ((F | A) . x) )
assume that
A5: x in dom (F | A) and
A6: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = - ((F | A) . x)
(F | A) . (- x) = (F | A) /. (- x) by A6, PARTFUN1:def_6
.= F /. (- x) by A1, A3, A6, PARTFUN2:17
.= F . (- x) by A1, A3, A6, PARTFUN1:def_6
.= - (F . x) by A4, A5
.= - (F /. x) by A1, A3, A5, PARTFUN1:def_6
.= - ((F | A) /. x) by A1, A3, A5, PARTFUN2:17
.= - ((F | A) . x) by A5, PARTFUN1:def_6 ;
hence (F | A) . (- x) = - ((F | A) . x) ; ::_thesis: verum
end;
then ( F | A is with_symmetrical_domain & F | A is quasi_odd ) by A3, Def2, Def6;
hence F is_odd_on A by A1, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:5
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) ) )
assume that
A1: F is_even_on A and
A2: for x being Real st x in A holds
F . x <> 0 ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
A3: A c= dom F by A1, Def5;
A4: F | A is even by A1, Def5;
for x being Real st x in A holds
(F . x) / (F . (- x)) = 1
proof
let x be Real; ::_thesis: ( x in A implies (F . x) / (F . (- x)) = 1 )
assume A5: x in A ; ::_thesis: (F . x) / (F . (- x)) = 1
then A6: x in dom (F | A) by A3, RELAT_1:62;
A7: F . x = F /. x by A3, A5, PARTFUN1:def_6
.= (F | A) /. x by A3, A5, PARTFUN2:17
.= (F | A) . x by A6, PARTFUN1:def_6 ;
A8: - x in A by A5, Def1;
then A9: - x in dom (F | A) by A3, RELAT_1:62;
(F . x) / (F . (- x)) = (F /. x) / (F . (- x)) by A3, A5, PARTFUN1:def_6
.= (F /. x) / (F /. (- x)) by A3, A8, PARTFUN1:def_6
.= ((F | A) /. x) / (F /. (- x)) by A3, A5, PARTFUN2:17
.= ((F | A) /. x) / ((F | A) /. (- x)) by A3, A8, PARTFUN2:17
.= ((F | A) . x) / ((F | A) /. (- x)) by A6, PARTFUN1:def_6
.= ((F | A) . x) / ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= ((F | A) . x) / ((F | A) . x) by A4, A6, A9, Def3
.= 1 by A2, A5, A7, XCMPLX_1:60 ;
hence (F . x) / (F . (- x)) = 1 ; ::_thesis: verum
end;
hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) ) by A1, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:6
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) holds
F is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) holds
F is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) implies F is_even_on A )
assume that
A1: A c= dom F and
A2: for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ; ::_thesis: F is_even_on A
A3: dom (F | A) = A by A1, RELAT_1:62;
A4: for x being Real st x in A holds
F . (- x) = F . x
proof
let x be Real; ::_thesis: ( x in A implies F . (- x) = F . x )
assume x in A ; ::_thesis: F . (- x) = F . x
then (F . x) / (F . (- x)) = 1 by A2;
hence F . (- x) = F . x by XCMPLX_1:58; ::_thesis: 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; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x )
assume that
A5: x in dom (F | A) and
A6: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = (F | A) . x
(F | A) . (- x) = (F | A) /. (- x) by A6, PARTFUN1:def_6
.= F /. (- x) by A1, A3, A6, PARTFUN2:17
.= F . (- x) by A1, A3, A6, PARTFUN1:def_6
.= F . x by A4, A5
.= F /. x by A1, A3, A5, PARTFUN1:def_6
.= (F | A) /. x by A1, A3, A5, PARTFUN2:17
.= (F | A) . x by A5, PARTFUN1:def_6 ;
hence (F | A) . (- x) = (F | A) . x ; ::_thesis: verum
end;
then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A3, Def2, Def3;
hence F is_even_on A by A1, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:7
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A & F is_odd_on A holds
for x being Real st x in A holds
F . x = 0
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A & F is_odd_on A holds
for x being Real st x in A holds
F . x = 0
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & F is_odd_on A implies for x being Real st x in A holds
F . x = 0 )
assume that
A1: F is_even_on A and
A2: F is_odd_on A ; ::_thesis: for x being Real st x in A holds
F . x = 0
A3: F | A is even by A1, Def5;
A4: F | A is odd by A2, Def8;
let x be Real; ::_thesis: ( x in A implies F . x = 0 )
assume A5: x in A ; ::_thesis: F . x = 0
A6: A c= dom F by A1, Def5;
then A7: x in dom (F | A) by A5, RELAT_1:62;
- x in A by A5, Def1;
then A8: - x in dom (F | A) by A6, RELAT_1:62;
F . x = F /. x by A6, A5, PARTFUN1:def_6
.= (F | A) /. x by A6, A5, PARTFUN2:17
.= (F | A) . x by A7, PARTFUN1:def_6
.= (F | A) . (- x) by A3, A7, A8, Def3
.= - ((F | A) . x) by A4, A7, A8, Def6
.= - ((F | A) /. x) by A7, PARTFUN1:def_6
.= - (F /. x) by A6, A5, PARTFUN2:17
.= - (F . x) by A6, A5, PARTFUN1:def_6 ;
hence F . x = 0 ; ::_thesis: verum
end;
theorem :: FUNCT_8:8
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
for x being Real st x in A holds
F . x = F . (abs x)
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
for x being Real st x in A holds
F . x = F . (abs x)
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies for x being Real st x in A holds
F . x = F . (abs x) )
assume A1: F is_even_on A ; ::_thesis: for x being Real st x in A holds
F . x = F . (abs x)
then A2: A c= dom F by Def5;
A3: F | A is even by A1, Def5;
let x be Real; ::_thesis: ( x in A implies F . x = F . (abs x) )
assume A4: x in A ; ::_thesis: F . x = F . (abs x)
A5: x in dom (F | A) by A2, A4, RELAT_1:62;
A6: - x in A by A4, Def1;
then A7: - x in dom (F | A) by A2, RELAT_1:62;
percases ( x < 0 or 0 < x or x = 0 ) ;
suppose x < 0 ; ::_thesis: F . x = F . (abs x)
then F . (abs x) = F . (- x) by ABSVALUE:def_1
.= F /. (- x) by A2, A6, PARTFUN1:def_6
.= (F | A) /. (- x) by A2, A6, PARTFUN2:17
.= (F | A) . (- x) by A7, PARTFUN1:def_6
.= (F | A) . x by A3, A5, A7, Def3
.= (F | A) /. x by A5, PARTFUN1:def_6
.= F /. x by A2, A4, PARTFUN2:17
.= F . x by A2, A4, PARTFUN1:def_6 ;
hence F . x = F . (abs x) ; ::_thesis: verum
end;
suppose 0 < x ; ::_thesis: F . x = F . (abs x)
hence F . x = F . (abs x) by ABSVALUE:def_1; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: F . x = F . (abs x)
hence F . x = F . (abs x) by ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
theorem :: FUNCT_8:9
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
F . x = F . (abs x) ) holds
F is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
F . x = F . (abs x) ) holds
F is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds
F . x = F . (abs x) ) implies F is_even_on A )
assume that
A1: A c= dom F and
A2: for x being Real st x in A holds
F . x = F . (abs x) ; ::_thesis: F is_even_on A
A3: dom (F | A) = A by A1, RELAT_1:62;
A4: for x being Real st x in A holds
- x in A by Def1;
A5: for x being Real st x in A holds
F . (- x) = F . x
proof
let x be Real; ::_thesis: ( x in A implies F . (- x) = F . x )
assume A6: x in A ; ::_thesis: F . (- x) = F . x
percases ( x < 0 or 0 < x or x = 0 ) ;
suppose x < 0 ; ::_thesis: F . (- x) = F . x
then F . (- x) = F . (abs x) by ABSVALUE:def_1
.= F . x by A2, A6 ;
hence F . (- x) = F . x ; ::_thesis: verum
end;
suppose 0 < x ; ::_thesis: F . (- x) = F . x
then abs (- x) = - (- x) by ABSVALUE:def_1
.= x ;
hence F . (- x) = F . x by A2, A4, A6; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: F . (- x) = F . x
hence F . (- x) = F . x ; ::_thesis: verum
end;
end;
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; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x )
assume that
A7: x in dom (F | A) and
A8: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = (F | A) . x
(F | A) . (- x) = (F | A) /. (- x) by A8, PARTFUN1:def_6
.= F /. (- x) by A1, A3, A8, PARTFUN2:17
.= F . (- x) by A1, A3, A8, PARTFUN1:def_6
.= F . x by A5, A7
.= F /. x by A1, A3, A7, PARTFUN1:def_6
.= (F | A) /. x by A1, A3, A7, PARTFUN2:17
.= (F | A) . x by A7, PARTFUN1:def_6 ;
hence (F | A) . (- x) = (F | A) . x ; ::_thesis: verum
end;
then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A3, Def2, Def3;
hence F is_even_on A by A1, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:10
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F + G is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F + G is_odd_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F + G is_odd_on A )
assume that
A1: F is_odd_on A and
A2: G is_odd_on A ; ::_thesis: F + G is_odd_on A
A3: A c= dom G by A2, Def8;
A4: G | A is odd by A2, Def8;
A5: A c= dom F by A1, Def8;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F + G) by VALUED_1:def_1;
then A8: dom ((F + G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is odd by A1, Def8;
for x being Real st x in dom ((F + G) | A) & - x in dom ((F + G) | A) holds
((F + G) | A) . (- x) = - (((F + G) | A) . x)
proof
let x be Real; ::_thesis: ( x in dom ((F + G) | A) & - x in dom ((F + G) | A) implies ((F + G) | A) . (- x) = - (((F + G) | A) . x) )
assume that
A10: x in dom ((F + G) | A) and
A11: - x in dom ((F + G) | A) ; ::_thesis: ((F + G) | A) . (- x) = - (((F + G) | A) . x)
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F + G) | A) . (- x) = ((F + G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F + G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F + G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) + (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_1
.= (F /. (- x)) + (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) + (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) + (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) + ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) + ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) + ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= (- ((F | A) . x)) + ((G | A) . (- x)) by A9, A12, A14, Def6
.= (- ((F | A) . x)) + (- ((G | A) . x)) by A4, A13, A15, Def6
.= - (((F | A) . x) + ((G | A) . x))
.= - (((F | A) /. x) + ((G | A) . x)) by A12, PARTFUN1:def_6
.= - (((F | A) /. x) + ((G | A) /. x)) by A13, PARTFUN1:def_6
.= - ((F /. x) + ((G | A) /. x)) by A5, A8, A10, PARTFUN2:17
.= - ((F /. x) + (G /. x)) by A3, A8, A10, PARTFUN2:17
.= - ((F . x) + (G /. x)) by A5, A8, A10, PARTFUN1:def_6
.= - ((F . x) + (G . x)) by A3, A8, A10, PARTFUN1:def_6
.= - ((F + G) . x) by A6, A7, A8, A10, VALUED_1:def_1
.= - ((F + G) /. x) by A6, A7, A8, A10, PARTFUN1:def_6
.= - (((F + G) | A) /. x) by A6, A7, A8, A10, PARTFUN2:17
.= - (((F + G) | A) . x) by A10, PARTFUN1:def_6 ;
hence ((F + G) | A) . (- x) = - (((F + G) | A) . x) ; ::_thesis: verum
end;
then ( (F + G) | A is with_symmetrical_domain & (F + G) | A is quasi_odd ) by A8, Def2, Def6;
hence F + G is_odd_on A by A6, A7, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:11
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F + G is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F + G is_even_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F + G is_even_on A )
assume that
A1: F is_even_on A and
A2: G is_even_on A ; ::_thesis: F + G is_even_on A
A3: A c= dom G by A2, Def5;
A4: G | A is even by A2, Def5;
A5: A c= dom F by A1, Def5;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F + G) by VALUED_1:def_1;
then A8: dom ((F + G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is even by A1, Def5;
for x being Real st x in dom ((F + G) | A) & - x in dom ((F + G) | A) holds
((F + G) | A) . (- x) = ((F + G) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F + G) | A) & - x in dom ((F + G) | A) implies ((F + G) | A) . (- x) = ((F + G) | A) . x )
assume that
A10: x in dom ((F + G) | A) and
A11: - x in dom ((F + G) | A) ; ::_thesis: ((F + G) | A) . (- x) = ((F + G) | A) . x
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F + G) | A) . (- x) = ((F + G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F + G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F + G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) + (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_1
.= (F /. (- x)) + (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) + (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) + (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) + ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) + ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) + ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= ((F | A) . x) + ((G | A) . (- x)) by A9, A12, A14, Def3
.= ((F | A) . x) + ((G | A) . x) by A4, A13, A15, Def3
.= ((F | A) /. x) + ((G | A) . x) by A12, PARTFUN1:def_6
.= ((F | A) /. x) + ((G | A) /. x) by A13, PARTFUN1:def_6
.= (F /. x) + ((G | A) /. x) by A5, A8, A10, PARTFUN2:17
.= (F /. x) + (G /. x) by A3, A8, A10, PARTFUN2:17
.= (F . x) + (G /. x) by A5, A8, A10, PARTFUN1:def_6
.= (F . x) + (G . x) by A3, A8, A10, PARTFUN1:def_6
.= (F + G) . x by A6, A7, A8, A10, VALUED_1:def_1
.= (F + G) /. x by A6, A7, A8, A10, PARTFUN1:def_6
.= ((F + G) | A) /. x by A6, A7, A8, A10, PARTFUN2:17
.= ((F + G) | A) . x by A10, PARTFUN1:def_6 ;
hence ((F + G) | A) . (- x) = ((F + G) | A) . x ; ::_thesis: verum
end;
then ( (F + G) | A is with_symmetrical_domain & (F + G) | A is quasi_even ) by A8, Def2, Def3;
hence F + G is_even_on A by A6, A7, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:12
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F - G is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F - G is_odd_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F - G is_odd_on A )
assume that
A1: F is_odd_on A and
A2: G is_odd_on A ; ::_thesis: F - G is_odd_on A
A3: A c= dom G by A2, Def8;
A4: G | A is odd by A2, Def8;
A5: A c= dom F by A1, Def8;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F - G) by VALUED_1:12;
then A8: dom ((F - G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is odd by A1, Def8;
for x being Real st x in dom ((F - G) | A) & - x in dom ((F - G) | A) holds
((F - G) | A) . (- x) = - (((F - G) | A) . x)
proof
let x be Real; ::_thesis: ( x in dom ((F - G) | A) & - x in dom ((F - G) | A) implies ((F - G) | A) . (- x) = - (((F - G) | A) . x) )
assume that
A10: x in dom ((F - G) | A) and
A11: - x in dom ((F - G) | A) ; ::_thesis: ((F - G) | A) . (- x) = - (((F - G) | A) . x)
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F - G) | A) . (- x) = ((F - G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F - G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F - G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) - (G . (- x)) by A6, A7, A8, A11, VALUED_1:13
.= (F /. (- x)) - (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) - (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) - (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) - ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) - ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) - ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= (- ((F | A) . x)) - ((G | A) . (- x)) by A9, A12, A14, Def6
.= (- ((F | A) . x)) - (- ((G | A) . x)) by A4, A13, A15, Def6
.= - (((F | A) . x) - ((G | A) . x))
.= - (((F | A) /. x) - ((G | A) . x)) by A12, PARTFUN1:def_6
.= - (((F | A) /. x) - ((G | A) /. x)) by A13, PARTFUN1:def_6
.= - ((F /. x) - ((G | A) /. x)) by A5, A8, A10, PARTFUN2:17
.= - ((F /. x) - (G /. x)) by A3, A8, A10, PARTFUN2:17
.= - ((F . x) - (G /. x)) by A5, A8, A10, PARTFUN1:def_6
.= - ((F . x) - (G . x)) by A3, A8, A10, PARTFUN1:def_6
.= - ((F - G) . x) by A6, A7, A8, A10, VALUED_1:13
.= - ((F - G) /. x) by A6, A7, A8, A10, PARTFUN1:def_6
.= - (((F - G) | A) /. x) by A6, A7, A8, A10, PARTFUN2:17
.= - (((F - G) | A) . x) by A10, PARTFUN1:def_6 ;
hence ((F - G) | A) . (- x) = - (((F - G) | A) . x) ; ::_thesis: verum
end;
then ( (F - G) | A is with_symmetrical_domain & (F - G) | A is quasi_odd ) by A8, Def2, Def6;
hence F - G is_odd_on A by A6, A7, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:13
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F - G is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F - G is_even_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F - G is_even_on A )
assume that
A1: F is_even_on A and
A2: G is_even_on A ; ::_thesis: F - G is_even_on A
A3: A c= dom G by A2, Def5;
A4: G | A is even by A2, Def5;
A5: A c= dom F by A1, Def5;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F - G) by VALUED_1:12;
then A8: dom ((F - G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is even by A1, Def5;
for x being Real st x in dom ((F - G) | A) & - x in dom ((F - G) | A) holds
((F - G) | A) . (- x) = ((F - G) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F - G) | A) & - x in dom ((F - G) | A) implies ((F - G) | A) . (- x) = ((F - G) | A) . x )
assume that
A10: x in dom ((F - G) | A) and
A11: - x in dom ((F - G) | A) ; ::_thesis: ((F - G) | A) . (- x) = ((F - G) | A) . x
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F - G) | A) . (- x) = ((F - G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F - G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F - G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) - (G . (- x)) by A6, A7, A8, A11, VALUED_1:13
.= (F /. (- x)) - (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) - (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) - (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) - ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) - ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) - ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= ((F | A) . x) - ((G | A) . (- x)) by A9, A12, A14, Def3
.= ((F | A) . x) - ((G | A) . x) by A4, A13, A15, Def3
.= ((F | A) /. x) - ((G | A) . x) by A12, PARTFUN1:def_6
.= ((F | A) /. x) - ((G | A) /. x) by A13, PARTFUN1:def_6
.= (F /. x) - ((G | A) /. x) by A5, A8, A10, PARTFUN2:17
.= (F /. x) - (G /. x) by A3, A8, A10, PARTFUN2:17
.= (F . x) - (G /. x) by A5, A8, A10, PARTFUN1:def_6
.= (F . x) - (G . x) by A3, A8, A10, PARTFUN1:def_6
.= (F - G) . x by A6, A7, A8, A10, VALUED_1:13
.= (F - G) /. x by A6, A7, A8, A10, PARTFUN1:def_6
.= ((F - G) | A) /. x by A6, A7, A8, A10, PARTFUN2:17
.= ((F - G) | A) . x by A10, PARTFUN1:def_6 ;
hence ((F - G) | A) . (- x) = ((F - G) | A) . x ; ::_thesis: verum
end;
then ( (F - G) | A is with_symmetrical_domain & (F - G) | A is quasi_even ) by A8, Def2, Def3;
hence F - G is_even_on A by A6, A7, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:14
for r being Real
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
r (#) F is_odd_on A
proof
let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
r (#) F is_odd_on A
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds
r (#) F is_odd_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies r (#) F is_odd_on A )
assume A1: F is_odd_on A ; ::_thesis: r (#) F is_odd_on A
then A2: A c= dom F by Def8;
then A3: A c= dom (r (#) F) by VALUED_1:def_5;
then A4: dom ((r (#) F) | A) = A by RELAT_1:62;
A5: F | A is odd by A1, Def8;
for x being Real st x in dom ((r (#) F) | A) & - x in dom ((r (#) F) | A) holds
((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x)
proof
let x be Real; ::_thesis: ( x in dom ((r (#) F) | A) & - x in dom ((r (#) F) | A) implies ((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x) )
assume that
A6: x in dom ((r (#) F) | A) and
A7: - x in dom ((r (#) F) | A) ; ::_thesis: ((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x)
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((r (#) F) | A) . (- x) = ((r (#) F) | A) /. (- x) by A7, PARTFUN1:def_6
.= (r (#) F) /. (- x) by A3, A4, A7, PARTFUN2:17
.= (r (#) F) . (- x) by A3, A4, A7, PARTFUN1:def_6
.= r * (F . (- x)) by A3, A4, A7, VALUED_1:def_5
.= r * (F /. (- x)) by A2, A4, A7, PARTFUN1:def_6
.= r * ((F | A) /. (- x)) by A2, A4, A7, PARTFUN2:17
.= r * ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= r * (- ((F | A) . x)) by A5, A8, A9, Def6
.= - (r * ((F | A) . x))
.= - (r * ((F | A) /. x)) by A8, PARTFUN1:def_6
.= - (r * (F /. x)) by A2, A4, A6, PARTFUN2:17
.= - (r * (F . x)) by A2, A4, A6, PARTFUN1:def_6
.= - ((r (#) F) . x) by A3, A4, A6, VALUED_1:def_5
.= - ((r (#) F) /. x) by A3, A4, A6, PARTFUN1:def_6
.= - (((r (#) F) | A) /. x) by A3, A4, A6, PARTFUN2:17
.= - (((r (#) F) | A) . x) by A6, PARTFUN1:def_6 ;
hence ((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x) ; ::_thesis: verum
end;
then ( (r (#) F) | A is with_symmetrical_domain & (r (#) F) | A is quasi_odd ) by A4, Def2, Def6;
hence r (#) F is_odd_on A by A3, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:15
for r being Real
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
r (#) F is_even_on A
proof
let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
r (#) F is_even_on A
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
r (#) F is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies r (#) F is_even_on A )
assume A1: F is_even_on A ; ::_thesis: r (#) F is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom (r (#) F) by VALUED_1:def_5;
then A4: dom ((r (#) F) | A) = A by RELAT_1:62;
A5: F | A is even by A1, Def5;
for x being Real st x in dom ((r (#) F) | A) & - x in dom ((r (#) F) | A) holds
((r (#) F) | A) . (- x) = ((r (#) F) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((r (#) F) | A) & - x in dom ((r (#) F) | A) implies ((r (#) F) | A) . (- x) = ((r (#) F) | A) . x )
assume that
A6: x in dom ((r (#) F) | A) and
A7: - x in dom ((r (#) F) | A) ; ::_thesis: ((r (#) F) | A) . (- x) = ((r (#) F) | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((r (#) F) | A) . (- x) = ((r (#) F) | A) /. (- x) by A7, PARTFUN1:def_6
.= (r (#) F) /. (- x) by A3, A4, A7, PARTFUN2:17
.= (r (#) F) . (- x) by A3, A4, A7, PARTFUN1:def_6
.= r * (F . (- x)) by A3, A4, A7, VALUED_1:def_5
.= r * (F /. (- x)) by A2, A4, A7, PARTFUN1:def_6
.= r * ((F | A) /. (- x)) by A2, A4, A7, PARTFUN2:17
.= r * ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= r * ((F | A) . x) by A5, A8, A9, Def3
.= r * ((F | A) /. x) by A8, PARTFUN1:def_6
.= r * (F /. x) by A2, A4, A6, PARTFUN2:17
.= r * (F . x) by A2, A4, A6, PARTFUN1:def_6
.= (r (#) F) . x by A3, A4, A6, VALUED_1:def_5
.= (r (#) F) /. x by A3, A4, A6, PARTFUN1:def_6
.= ((r (#) F) | A) /. x by A3, A4, A6, PARTFUN2:17
.= ((r (#) F) | A) . x by A6, PARTFUN1:def_6 ;
hence ((r (#) F) | A) . (- x) = ((r (#) F) | A) . x ; ::_thesis: verum
end;
then ( (r (#) F) | A is with_symmetrical_domain & (r (#) F) | A is quasi_even ) by A4, Def2, Def3;
hence r (#) F is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem Th16: :: FUNCT_8:16
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
- F is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds
- F is_odd_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies - F is_odd_on A )
assume A1: F is_odd_on A ; ::_thesis: - F is_odd_on A
then A2: A c= dom F by Def8;
then A3: A c= dom (- F) by VALUED_1:8;
then A4: dom ((- F) | A) = A by RELAT_1:62;
A5: F | A is odd by A1, Def8;
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; ::_thesis: ( 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) ; ::_thesis: ((- F) | A) . (- x) = - (((- F) | A) . x)
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((- F) | A) . (- x) = ((- F) | A) /. (- x) by A7, PARTFUN1:def_6
.= (- F) /. (- x) by A3, A4, A7, PARTFUN2:17
.= (- F) . (- x) by A3, A4, A7, PARTFUN1:def_6
.= - (F . (- x)) by VALUED_1:8
.= - (F /. (- x)) by A2, A4, A7, PARTFUN1:def_6
.= - ((F | A) /. (- x)) by A2, A4, A7, PARTFUN2:17
.= - ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= - (- ((F | A) . x)) by A5, A8, A9, Def6
.= - (- ((F | A) /. x)) by A8, PARTFUN1:def_6
.= - (- (F /. x)) by A2, A4, A6, PARTFUN2:17
.= - (- (F . x)) by A2, A4, A6, PARTFUN1:def_6
.= - ((- F) . x) by VALUED_1:8
.= - ((- F) /. x) by A3, A4, A6, PARTFUN1:def_6
.= - (((- F) | A) /. x) by A3, A4, A6, PARTFUN2:17
.= - (((- F) | A) . x) by A6, PARTFUN1:def_6 ;
hence ((- F) | A) . (- x) = - (((- F) | A) . x) ; ::_thesis: verum
end;
then ( (- F) | A is with_symmetrical_domain & (- F) | A is quasi_odd ) by A4, Def2, Def6;
hence - F is_odd_on A by A3, Def8; ::_thesis: verum
end;
theorem Th17: :: FUNCT_8:17
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
- F is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
- F is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies - F is_even_on A )
assume A1: F is_even_on A ; ::_thesis: - F is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom (- F) by VALUED_1:8;
then A4: dom ((- F) | A) = A by RELAT_1:62;
A5: F | A is even by A1, Def5;
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; ::_thesis: ( 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) ; ::_thesis: ((- F) | A) . (- x) = ((- F) | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((- F) | A) . (- x) = ((- F) | A) /. (- x) by A7, PARTFUN1:def_6
.= (- F) /. (- x) by A3, A4, A7, PARTFUN2:17
.= (- F) . (- x) by A3, A4, A7, PARTFUN1:def_6
.= - (F . (- x)) by VALUED_1:8
.= - (F /. (- x)) by A2, A4, A7, PARTFUN1:def_6
.= - ((F | A) /. (- x)) by A2, A4, A7, PARTFUN2:17
.= - ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= - ((F | A) . x) by A5, A8, A9, Def3
.= - ((F | A) /. x) by A8, PARTFUN1:def_6
.= - (F /. x) by A2, A4, A6, PARTFUN2:17
.= - (F . x) by A2, A4, A6, PARTFUN1:def_6
.= (- F) . x by VALUED_1:8
.= (- F) /. x by A3, A4, A6, PARTFUN1:def_6
.= ((- F) | A) /. x by A3, A4, A6, PARTFUN2:17
.= ((- F) | A) . x by A6, PARTFUN1:def_6 ;
hence ((- F) | A) . (- x) = ((- F) | A) . x ; ::_thesis: verum
end;
then ( (- F) | A is with_symmetrical_domain & (- F) | A is quasi_even ) by A4, Def2, Def3;
hence - F is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem Th18: :: FUNCT_8:18
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
F " is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds
F " is_odd_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies F " is_odd_on A )
assume A1: F is_odd_on A ; ::_thesis: F " is_odd_on A
then A2: A c= dom F by Def8;
then A3: A c= dom (F ") by VALUED_1:def_7;
then A4: dom ((F ") | A) = A by RELAT_1:62;
A5: F | A is odd by A1, Def8;
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; ::_thesis: ( 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) ; ::_thesis: ((F ") | A) . (- x) = - (((F ") | A) . x)
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((F ") | A) . (- x) = ((F ") | A) /. (- x) by A7, PARTFUN1:def_6
.= (F ") /. (- x) by A3, A4, A7, PARTFUN2:17
.= (F ") . (- x) by A3, A4, A7, PARTFUN1:def_6
.= (F . (- x)) " by A3, A4, A7, VALUED_1:def_7
.= (F /. (- x)) " by A2, A4, A7, PARTFUN1:def_6
.= ((F | A) /. (- x)) " by A2, A4, A7, PARTFUN2:17
.= ((F | A) . (- x)) " by A9, PARTFUN1:def_6
.= (- ((F | A) . x)) " by A5, A8, A9, Def6
.= (- ((F | A) /. x)) " by A8, PARTFUN1:def_6
.= (- (F /. x)) " by A2, A4, A6, PARTFUN2:17
.= (- (F . x)) " by A2, A4, A6, PARTFUN1:def_6
.= - ((F . x) ") by XCMPLX_1:222
.= - ((F ") . x) by A3, A4, A6, VALUED_1:def_7
.= - ((F ") /. x) by A3, A4, A6, PARTFUN1:def_6
.= - (((F ") | A) /. x) by A3, A4, A6, PARTFUN2:17
.= - (((F ") | A) . x) by A6, PARTFUN1:def_6 ;
hence ((F ") | A) . (- x) = - (((F ") | A) . x) ; ::_thesis: verum
end;
then ( (F ") | A is with_symmetrical_domain & (F ") | A is quasi_odd ) by A4, Def2, Def6;
hence F " is_odd_on A by A3, Def8; ::_thesis: verum
end;
theorem Th19: :: FUNCT_8:19
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
F " is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
F " is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies F " is_even_on A )
assume A1: F is_even_on A ; ::_thesis: F " is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom (F ") by VALUED_1:def_7;
then A4: dom ((F ") | A) = A by RELAT_1:62;
A5: F | A is even by A1, Def5;
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; ::_thesis: ( 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) ; ::_thesis: ((F ") | A) . (- x) = ((F ") | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((F ") | A) . (- x) = ((F ") | A) /. (- x) by A7, PARTFUN1:def_6
.= (F ") /. (- x) by A3, A4, A7, PARTFUN2:17
.= (F ") . (- x) by A3, A4, A7, PARTFUN1:def_6
.= (F . (- x)) " by A3, A4, A7, VALUED_1:def_7
.= (F /. (- x)) " by A2, A4, A7, PARTFUN1:def_6
.= ((F | A) /. (- x)) " by A2, A4, A7, PARTFUN2:17
.= ((F | A) . (- x)) " by A9, PARTFUN1:def_6
.= ((F | A) . x) " by A5, A8, A9, Def3
.= ((F | A) /. x) " by A8, PARTFUN1:def_6
.= (F /. x) " by A2, A4, A6, PARTFUN2:17
.= (F . x) " by A2, A4, A6, PARTFUN1:def_6
.= (F ") . x by A3, A4, A6, VALUED_1:def_7
.= (F ") /. x by A3, A4, A6, PARTFUN1:def_6
.= ((F ") | A) /. x by A3, A4, A6, PARTFUN2:17
.= ((F ") | A) . x by A6, PARTFUN1:def_6 ;
hence ((F ") | A) . (- x) = ((F ") | A) . x ; ::_thesis: verum
end;
then ( (F ") | A is with_symmetrical_domain & (F ") | A is quasi_even ) by A4, Def2, Def3;
hence F " is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem Th20: :: FUNCT_8:20
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
|.F.| is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds
|.F.| is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies |.F.| is_even_on A )
assume A1: F is_odd_on A ; ::_thesis: |.F.| is_even_on A
then A2: A c= dom F by Def8;
then A3: A c= dom |.F.| by VALUED_1:def_11;
then A4: dom (|.F.| | A) = A by RELAT_1:62;
A5: F | A is odd by A1, Def8;
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; ::_thesis: ( 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) ; ::_thesis: (|.F.| | A) . (- x) = (|.F.| | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
(|.F.| | A) . (- x) = (|.F.| | A) /. (- x) by A7, PARTFUN1:def_6
.= |.F.| /. (- x) by A3, A4, A7, PARTFUN2:17
.= |.F.| . (- x) by A3, A4, A7, PARTFUN1:def_6
.= |.(F . (- x)).| by A3, A4, A7, VALUED_1:def_11
.= |.(F /. (- x)).| by A2, A4, A7, PARTFUN1:def_6
.= |.((F | A) /. (- x)).| by A2, A4, A7, PARTFUN2:17
.= |.((F | A) . (- x)).| by A9, PARTFUN1:def_6
.= |.(- ((F | A) . x)).| by A5, A8, A9, Def6
.= |.(- ((F | A) /. x)).| by A8, PARTFUN1:def_6
.= |.(- (F /. x)).| by A2, A4, A6, PARTFUN2:17
.= |.(- (F . x)).| by A2, A4, A6, PARTFUN1:def_6
.= |.(F . x).| by COMPLEX1:52
.= |.F.| . x by A3, A4, A6, VALUED_1:def_11
.= |.F.| /. x by A3, A4, A6, PARTFUN1:def_6
.= (|.F.| | A) /. x by A3, A4, A6, PARTFUN2:17
.= (|.F.| | A) . x by A6, PARTFUN1:def_6 ;
hence (|.F.| | A) . (- x) = (|.F.| | A) . x ; ::_thesis: verum
end;
then ( |.F.| | A is with_symmetrical_domain & |.F.| | A is quasi_even ) by A4, Def2, Def3;
hence |.F.| is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem Th21: :: FUNCT_8:21
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
|.F.| is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
|.F.| is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies |.F.| is_even_on A )
assume A1: F is_even_on A ; ::_thesis: |.F.| is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom |.F.| by VALUED_1:def_11;
then A4: dom (|.F.| | A) = A by RELAT_1:62;
A5: F | A is even by A1, Def5;
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; ::_thesis: ( 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) ; ::_thesis: (|.F.| | A) . (- x) = (|.F.| | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
(|.F.| | A) . (- x) = (|.F.| | A) /. (- x) by A7, PARTFUN1:def_6
.= |.F.| /. (- x) by A3, A4, A7, PARTFUN2:17
.= |.F.| . (- x) by A3, A4, A7, PARTFUN1:def_6
.= |.(F . (- x)).| by A3, A4, A7, VALUED_1:def_11
.= |.(F /. (- x)).| by A2, A4, A7, PARTFUN1:def_6
.= |.((F | A) /. (- x)).| by A2, A4, A7, PARTFUN2:17
.= |.((F | A) . (- x)).| by A9, PARTFUN1:def_6
.= |.((F | A) . x).| by A5, A8, A9, Def3
.= |.((F | A) /. x).| by A8, PARTFUN1:def_6
.= |.(F /. x).| by A2, A4, A6, PARTFUN2:17
.= |.(F . x).| by A2, A4, A6, PARTFUN1:def_6
.= |.F.| . x by A3, A4, A6, VALUED_1:def_11
.= |.F.| /. x by A3, A4, A6, PARTFUN1:def_6
.= (|.F.| | A) /. x by A3, A4, A6, PARTFUN2:17
.= (|.F.| | A) . x by A6, PARTFUN1:def_6 ;
hence (|.F.| | A) . (- x) = (|.F.| | A) . x ; ::_thesis: verum
end;
then ( |.F.| | A is with_symmetrical_domain & |.F.| | A is quasi_even ) by A4, Def2, Def3;
hence |.F.| is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem Th22: :: FUNCT_8:22
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F (#) G is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F (#) G is_even_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F (#) G is_even_on A )
assume that
A1: F is_odd_on A and
A2: G is_odd_on A ; ::_thesis: F (#) G is_even_on A
A3: A c= dom G by A2, Def8;
A4: G | A is odd by A2, Def8;
A5: A c= dom F by A1, Def8;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def_4;
then A8: dom ((F (#) G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is odd by A1, Def8;
for x being Real st x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) holds
((F (#) G) | A) . (- x) = ((F (#) G) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) implies ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x )
assume that
A10: x in dom ((F (#) G) | A) and
A11: - x in dom ((F (#) G) | A) ; ::_thesis: ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F (#) G) | A) . (- x) = ((F (#) G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F (#) G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F (#) G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) * (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_4
.= (F /. (- x)) * (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) * (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) * (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) * ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) * ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) * ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= (- ((F | A) . x)) * ((G | A) . (- x)) by A9, A12, A14, Def6
.= (- ((F | A) . x)) * (- ((G | A) . x)) by A4, A13, A15, Def6
.= ((F | A) . x) * ((G | A) . x)
.= ((F | A) /. x) * ((G | A) . x) by A12, PARTFUN1:def_6
.= ((F | A) /. x) * ((G | A) /. x) by A13, PARTFUN1:def_6
.= (F /. x) * ((G | A) /. x) by A5, A8, A10, PARTFUN2:17
.= (F /. x) * (G /. x) by A3, A8, A10, PARTFUN2:17
.= (F . x) * (G /. x) by A5, A8, A10, PARTFUN1:def_6
.= (F . x) * (G . x) by A3, A8, A10, PARTFUN1:def_6
.= (F (#) G) . x by A6, A7, A8, A10, VALUED_1:def_4
.= (F (#) G) /. x by A6, A7, A8, A10, PARTFUN1:def_6
.= ((F (#) G) | A) /. x by A6, A7, A8, A10, PARTFUN2:17
.= ((F (#) G) | A) . x by A10, PARTFUN1:def_6 ;
hence ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x ; ::_thesis: verum
end;
then ( (F (#) G) | A is with_symmetrical_domain & (F (#) G) | A is quasi_even ) by A8, Def2, Def3;
hence F (#) G is_even_on A by A6, A7, Def5; ::_thesis: verum
end;
theorem Th23: :: FUNCT_8:23
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F (#) G is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F (#) G is_even_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F (#) G is_even_on A )
assume that
A1: F is_even_on A and
A2: G is_even_on A ; ::_thesis: F (#) G is_even_on A
A3: A c= dom G by A2, Def5;
A4: G | A is even by A2, Def5;
A5: A c= dom F by A1, Def5;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def_4;
then A8: dom ((F (#) G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is even by A1, Def5;
for x being Real st x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) holds
((F (#) G) | A) . (- x) = ((F (#) G) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) implies ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x )
assume that
A10: x in dom ((F (#) G) | A) and
A11: - x in dom ((F (#) G) | A) ; ::_thesis: ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F (#) G) | A) . (- x) = ((F (#) G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F (#) G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F (#) G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) * (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_4
.= (F /. (- x)) * (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) * (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) * (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) * ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) * ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) * ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= ((F | A) . x) * ((G | A) . (- x)) by A9, A12, A14, Def3
.= ((F | A) . x) * ((G | A) . x) by A4, A13, A15, Def3
.= ((F | A) /. x) * ((G | A) . x) by A12, PARTFUN1:def_6
.= ((F | A) /. x) * ((G | A) /. x) by A13, PARTFUN1:def_6
.= (F /. x) * ((G | A) /. x) by A5, A8, A10, PARTFUN2:17
.= (F /. x) * (G /. x) by A3, A8, A10, PARTFUN2:17
.= (F . x) * (G /. x) by A5, A8, A10, PARTFUN1:def_6
.= (F . x) * (G . x) by A3, A8, A10, PARTFUN1:def_6
.= (F (#) G) . x by A6, A7, A8, A10, VALUED_1:def_4
.= (F (#) G) /. x by A6, A7, A8, A10, PARTFUN1:def_6
.= ((F (#) G) | A) /. x by A6, A7, A8, A10, PARTFUN2:17
.= ((F (#) G) | A) . x by A10, PARTFUN1:def_6 ;
hence ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x ; ::_thesis: verum
end;
then ( (F (#) G) | A is with_symmetrical_domain & (F (#) G) | A is quasi_even ) by A8, Def2, Def3;
hence F (#) G is_even_on A by A6, A7, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:24
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds
F (#) G is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds
F (#) G is_odd_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_odd_on A implies F (#) G is_odd_on A )
assume that
A1: F is_even_on A and
A2: G is_odd_on A ; ::_thesis: F (#) G is_odd_on A
A3: A c= dom G by A2, Def8;
A4: G | A is odd by A2, Def8;
A5: A c= dom F by A1, Def5;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def_4;
then A8: dom ((F (#) G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is even by A1, Def5;
for x being Real st x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) holds
((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x)
proof
let x be Real; ::_thesis: ( x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) implies ((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x) )
assume that
A10: x in dom ((F (#) G) | A) and
A11: - x in dom ((F (#) G) | A) ; ::_thesis: ((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x)
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F (#) G) | A) . (- x) = ((F (#) G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F (#) G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F (#) G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) * (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_4
.= (F /. (- x)) * (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) * (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) * (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) * ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) * ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) * ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= ((F | A) . x) * ((G | A) . (- x)) by A9, A12, A14, Def3
.= ((F | A) . x) * (- ((G | A) . x)) by A4, A13, A15, Def6
.= - (((F | A) . x) * ((G | A) . x))
.= - (((F | A) /. x) * ((G | A) . x)) by A12, PARTFUN1:def_6
.= - (((F | A) /. x) * ((G | A) /. x)) by A13, PARTFUN1:def_6
.= - ((F /. x) * ((G | A) /. x)) by A5, A8, A10, PARTFUN2:17
.= - ((F /. x) * (G /. x)) by A3, A8, A10, PARTFUN2:17
.= - ((F . x) * (G /. x)) by A5, A8, A10, PARTFUN1:def_6
.= - ((F . x) * (G . x)) by A3, A8, A10, PARTFUN1:def_6
.= - ((F (#) G) . x) by A6, A7, A8, A10, VALUED_1:def_4
.= - ((F (#) G) /. x) by A6, A7, A8, A10, PARTFUN1:def_6
.= - (((F (#) G) | A) /. x) by A6, A7, A8, A10, PARTFUN2:17
.= - (((F (#) G) | A) . x) by A10, PARTFUN1:def_6 ;
hence ((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x) ; ::_thesis: verum
end;
then ( (F (#) G) | A is with_symmetrical_domain & (F (#) G) | A is quasi_odd ) by A8, Def2, Def6;
hence F (#) G is_odd_on A by A6, A7, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:25
for r being Real
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
r + F is_even_on A
proof
let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
r + F is_even_on A
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
r + F is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies r + F is_even_on A )
assume A1: F is_even_on A ; ::_thesis: r + F is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom (r + F) by VALUED_1:def_2;
then A4: dom ((r + F) | A) = A by RELAT_1:62;
A5: F | A is even by A1, Def5;
for x being Real st x in dom ((r + F) | A) & - x in dom ((r + F) | A) holds
((r + F) | A) . (- x) = ((r + F) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((r + F) | A) & - x in dom ((r + F) | A) implies ((r + F) | A) . (- x) = ((r + F) | A) . x )
assume that
A6: x in dom ((r + F) | A) and
A7: - x in dom ((r + F) | A) ; ::_thesis: ((r + F) | A) . (- x) = ((r + F) | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((r + F) | A) . (- x) = ((r + F) | A) /. (- x) by A7, PARTFUN1:def_6
.= (r + F) /. (- x) by A3, A4, A7, PARTFUN2:17
.= (r + F) . (- x) by A3, A4, A7, PARTFUN1:def_6
.= r + (F . (- x)) by A3, A4, A7, VALUED_1:def_2
.= r + (F /. (- x)) by A2, A4, A7, PARTFUN1:def_6
.= r + ((F | A) /. (- x)) by A2, A4, A7, PARTFUN2:17
.= r + ((F | A) . (- x)) by A9, PARTFUN1:def_6
.= r + ((F | A) . x) by A5, A8, A9, Def3
.= r + ((F | A) /. x) by A8, PARTFUN1:def_6
.= r + (F /. x) by A2, A4, A6, PARTFUN2:17
.= r + (F . x) by A2, A4, A6, PARTFUN1:def_6
.= (r + F) . x by A3, A4, A6, VALUED_1:def_2
.= (r + F) /. x by A3, A4, A6, PARTFUN1:def_6
.= ((r + F) | A) /. x by A3, A4, A6, PARTFUN2:17
.= ((r + F) | A) . x by A6, PARTFUN1:def_6 ;
hence ((r + F) | A) . (- x) = ((r + F) | A) . x ; ::_thesis: verum
end;
then ( (r + F) | A is with_symmetrical_domain & (r + F) | A is quasi_even ) by A4, Def2, Def3;
hence r + F is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:26
for r being Real
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
F - r is_even_on A
proof
let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
F - r is_even_on A
let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds
F - r is_even_on A
let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies F - r is_even_on A )
assume A1: F is_even_on A ; ::_thesis: F - r is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom (F - r) by VALUED_1:3;
then A4: dom ((F - r) | A) = A by RELAT_1:62;
A5: F | A is even by A1, Def5;
for x being Real st x in dom ((F - r) | A) & - x in dom ((F - r) | A) holds
((F - r) | A) . (- x) = ((F - r) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F - r) | A) & - x in dom ((F - r) | A) implies ((F - r) | A) . (- x) = ((F - r) | A) . x )
assume that
A6: x in dom ((F - r) | A) and
A7: - x in dom ((F - r) | A) ; ::_thesis: ((F - r) | A) . (- x) = ((F - r) | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
((F - r) | A) . (- x) = ((F - r) | A) /. (- x) by A7, PARTFUN1:def_6
.= (F - r) /. (- x) by A3, A4, A7, PARTFUN2:17
.= (F - r) . (- x) by A3, A4, A7, PARTFUN1:def_6
.= (F . (- x)) - r by A2, A4, A7, VALUED_1:3
.= (F /. (- x)) - r by A2, A4, A7, PARTFUN1:def_6
.= ((F | A) /. (- x)) - r by A2, A4, A7, PARTFUN2:17
.= ((F | A) . (- x)) - r by A9, PARTFUN1:def_6
.= ((F | A) . x) - r by A5, A8, A9, Def3
.= ((F | A) /. x) - r by A8, PARTFUN1:def_6
.= (F /. x) - r by A2, A4, A6, PARTFUN2:17
.= (F . x) - r by A2, A4, A6, PARTFUN1:def_6
.= (F - r) . x by A2, A4, A6, VALUED_1:3
.= (F - r) /. x by A3, A4, A6, PARTFUN1:def_6
.= ((F - r) | A) /. x by A3, A4, A6, PARTFUN2:17
.= ((F - r) | A) . x by A6, PARTFUN1:def_6 ;
hence ((F - r) | A) . (- x) = ((F - r) | A) . x ; ::_thesis: verum
end;
then ( (F - r) | A is with_symmetrical_domain & (F - r) | A is quasi_even ) by A4, Def2, Def3;
hence F - r is_even_on A by A3, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:27
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
F ^2 is_even_on A by Th23;
theorem :: FUNCT_8:28
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
F ^2 is_even_on A by Th22;
theorem :: FUNCT_8:29
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F /" G is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds
F /" G is_even_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F /" G is_even_on A )
assume that
A1: F is_odd_on A and
A2: G is_odd_on A ; ::_thesis: F /" G is_even_on A
A3: A c= dom G by A2, Def8;
A4: G | A is odd by A2, Def8;
A5: A c= dom F by A1, Def8;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A8: dom ((F /" G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is odd by A1, Def8;
for x being Real st x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) holds
((F /" G) | A) . (- x) = ((F /" G) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = ((F /" G) | A) . x )
assume that
A10: x in dom ((F /" G) | A) and
A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = ((F /" G) | A) . x
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F /" G) | A) . (- x) = ((F /" G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F /" G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F /" G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) / (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) / (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) / ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) / ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) / ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= (- ((F | A) . x)) / ((G | A) . (- x)) by A9, A12, A14, Def6
.= (- ((F | A) . x)) / (- ((G | A) . x)) by A4, A13, A15, Def6
.= ((F | A) . x) / ((G | A) . x) by XCMPLX_1:191
.= ((F | A) /. x) / ((G | A) . x) by A12, PARTFUN1:def_6
.= ((F | A) /. x) / ((G | A) /. x) by A13, PARTFUN1:def_6
.= (F /. x) / ((G | A) /. x) by A5, A8, A10, PARTFUN2:17
.= (F /. x) / (G /. x) by A3, A8, A10, PARTFUN2:17
.= (F . x) / (G /. x) by A5, A8, A10, PARTFUN1:def_6
.= (F . x) / (G . x) by A3, A8, A10, PARTFUN1:def_6
.= (F /" G) . x by VALUED_1:17
.= (F /" G) /. x by A6, A7, A8, A10, PARTFUN1:def_6
.= ((F /" G) | A) /. x by A6, A7, A8, A10, PARTFUN2:17
.= ((F /" G) | A) . x by A10, PARTFUN1:def_6 ;
hence ((F /" G) | A) . (- x) = ((F /" G) | A) . x ; ::_thesis: verum
end;
then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_even ) by A8, Def2, Def3;
hence F /" G is_even_on A by A6, A7, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:30
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F /" G is_even_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F /" G is_even_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F /" G is_even_on A )
assume that
A1: F is_even_on A and
A2: G is_even_on A ; ::_thesis: F /" G is_even_on A
A3: A c= dom G by A2, Def5;
A4: G | A is even by A2, Def5;
A5: A c= dom F by A1, Def5;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A8: dom ((F /" G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is even by A1, Def5;
for x being Real st x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) holds
((F /" G) | A) . (- x) = ((F /" G) | A) . x
proof
let x be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = ((F /" G) | A) . x )
assume that
A10: x in dom ((F /" G) | A) and
A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = ((F /" G) | A) . x
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F /" G) | A) . (- x) = ((F /" G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F /" G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F /" G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) / (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) / (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) / ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) / ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) / ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= ((F | A) . x) / ((G | A) . (- x)) by A9, A12, A14, Def3
.= ((F | A) . x) / ((G | A) . x) by A4, A13, A15, Def3
.= ((F | A) /. x) / ((G | A) . x) by A12, PARTFUN1:def_6
.= ((F | A) /. x) / ((G | A) /. x) by A13, PARTFUN1:def_6
.= (F /. x) / ((G | A) /. x) by A5, A8, A10, PARTFUN2:17
.= (F /. x) / (G /. x) by A3, A8, A10, PARTFUN2:17
.= (F . x) / (G /. x) by A5, A8, A10, PARTFUN1:def_6
.= (F . x) / (G . x) by A3, A8, A10, PARTFUN1:def_6
.= (F /" G) . x by VALUED_1:17
.= (F /" G) /. x by A6, A7, A8, A10, PARTFUN1:def_6
.= ((F /" G) | A) /. x by A6, A7, A8, A10, PARTFUN2:17
.= ((F /" G) | A) . x by A10, PARTFUN1:def_6 ;
hence ((F /" G) | A) . (- x) = ((F /" G) | A) . x ; ::_thesis: verum
end;
then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_even ) by A8, Def2, Def3;
hence F /" G is_even_on A by A6, A7, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:31
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_even_on A holds
F /" G is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_even_on A holds
F /" G is_odd_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_even_on A implies F /" G is_odd_on A )
assume that
A1: F is_odd_on A and
A2: G is_even_on A ; ::_thesis: F /" G is_odd_on A
A3: A c= dom G by A2, Def5;
A4: G | A is even by A2, Def5;
A5: A c= dom F by A1, Def8;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A8: dom ((F /" G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is odd by A1, Def8;
for x being Real st x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) holds
((F /" G) | A) . (- x) = - (((F /" G) | A) . x)
proof
let x be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) )
assume that
A10: x in dom ((F /" G) | A) and
A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = - (((F /" G) | A) . x)
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F /" G) | A) . (- x) = ((F /" G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F /" G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F /" G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) / (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) / (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) / ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) / ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) / ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= (- ((F | A) . x)) / ((G | A) . (- x)) by A9, A12, A14, Def6
.= (- ((F | A) . x)) / ((G | A) . x) by A4, A13, A15, Def3
.= - (((F | A) . x) / ((G | A) . x))
.= - (((F | A) /. x) / ((G | A) . x)) by A12, PARTFUN1:def_6
.= - (((F | A) /. x) / ((G | A) /. x)) by A13, PARTFUN1:def_6
.= - ((F /. x) / ((G | A) /. x)) by A5, A8, A10, PARTFUN2:17
.= - ((F /. x) / (G /. x)) by A3, A8, A10, PARTFUN2:17
.= - ((F . x) / (G /. x)) by A5, A8, A10, PARTFUN1:def_6
.= - ((F . x) / (G . x)) by A3, A8, A10, PARTFUN1:def_6
.= - ((F /" G) . x) by VALUED_1:17
.= - ((F /" G) /. x) by A6, A7, A8, A10, PARTFUN1:def_6
.= - (((F /" G) | A) /. x) by A6, A7, A8, A10, PARTFUN2:17
.= - (((F /" G) | A) . x) by A10, PARTFUN1:def_6 ;
hence ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ; ::_thesis: verum
end;
then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_odd ) by A8, Def2, Def6;
hence F /" G is_odd_on A by A6, A7, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:32
for A being symmetrical Subset of COMPLEX
for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds
F /" G is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds
F /" G is_odd_on A
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_odd_on A implies F /" G is_odd_on A )
assume that
A1: F is_even_on A and
A2: G is_odd_on A ; ::_thesis: F /" G is_odd_on A
A3: A c= dom G by A2, Def8;
A4: G | A is odd by A2, Def8;
A5: A c= dom F by A1, Def5;
then A6: A c= (dom F) /\ (dom G) by A3, XBOOLE_1:19;
A7: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A8: dom ((F /" G) | A) = A by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9: F | A is even by A1, Def5;
for x being Real st x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) holds
((F /" G) | A) . (- x) = - (((F /" G) | A) . x)
proof
let x be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) )
assume that
A10: x in dom ((F /" G) | A) and
A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = - (((F /" G) | A) . x)
A12: x in dom (F | A) by A5, A8, A10, RELAT_1:62;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:62;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:62;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:62;
((F /" G) | A) . (- x) = ((F /" G) | A) /. (- x) by A11, PARTFUN1:def_6
.= (F /" G) /. (- x) by A6, A7, A8, A11, PARTFUN2:17
.= (F /" G) . (- x) by A6, A7, A8, A11, PARTFUN1:def_6
.= (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6
.= (F /. (- x)) / (G /. (- x)) by A3, A8, A11, PARTFUN1:def_6
.= ((F | A) /. (- x)) / (G /. (- x)) by A5, A8, A11, PARTFUN2:17
.= ((F | A) /. (- x)) / ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:17
.= ((F | A) . (- x)) / ((G | A) /. (- x)) by A14, PARTFUN1:def_6
.= ((F | A) . (- x)) / ((G | A) . (- x)) by A15, PARTFUN1:def_6
.= ((F | A) . x) / ((G | A) . (- x)) by A9, A12, A14, Def3
.= ((F | A) . x) / (- ((G | A) . x)) by A4, A13, A15, Def6
.= - (((F | A) . x) / ((G | A) . x)) by XCMPLX_1:188
.= - (((F | A) /. x) / ((G | A) . x)) by A12, PARTFUN1:def_6
.= - (((F | A) /. x) / ((G | A) /. x)) by A13, PARTFUN1:def_6
.= - ((F /. x) / ((G | A) /. x)) by A5, A8, A10, PARTFUN2:17
.= - ((F /. x) / (G /. x)) by A3, A8, A10, PARTFUN2:17
.= - ((F . x) / (G /. x)) by A5, A8, A10, PARTFUN1:def_6
.= - ((F . x) / (G . x)) by A3, A8, A10, PARTFUN1:def_6
.= - ((F /" G) . x) by VALUED_1:17
.= - ((F /" G) /. x) by A6, A7, A8, A10, PARTFUN1:def_6
.= - (((F /" G) | A) /. x) by A6, A7, A8, A10, PARTFUN2:17
.= - (((F /" G) | A) . x) by A10, PARTFUN1:def_6 ;
hence ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ; ::_thesis: verum
end;
then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_odd ) by A8, Def2, Def6;
hence F /" G is_odd_on A by A6, A7, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:33
for F being PartFunc of REAL,REAL st F is odd holds
- F is odd
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies - F is odd )
A1: dom F = dom (- F) by VALUED_1:8;
assume A2: F is odd ; ::_thesis: - F is odd
for x being Real st x in dom (- F) & - x in dom (- F) holds
(- F) . (- x) = - ((- F) . x)
proof
let x be Real; ::_thesis: ( x in dom (- F) & - x in dom (- F) implies (- F) . (- x) = - ((- F) . x) )
assume A3: ( x in dom (- F) & - x in dom (- F) ) ; ::_thesis: (- F) . (- x) = - ((- F) . x)
(- F) . (- x) = - (F . (- x)) by VALUED_1:8
.= - (- (F . x)) by A2, A1, A3, Def6
.= - ((- F) . x) by VALUED_1:8 ;
hence (- F) . (- x) = - ((- F) . x) ; ::_thesis: verum
end;
then ( - F is with_symmetrical_domain & - F is quasi_odd ) by A2, A1, Def2, Def6;
hence - F is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:34
for F being PartFunc of REAL,REAL st F is even holds
- F is even
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies - F is even )
A1: dom F = dom (- F) by VALUED_1:8;
assume A2: F is even ; ::_thesis: - F is even
for x being Real st x in dom (- F) & - x in dom (- F) holds
(- F) . (- x) = (- F) . x
proof
let x be Real; ::_thesis: ( x in dom (- F) & - x in dom (- F) implies (- F) . (- x) = (- F) . x )
assume A3: ( x in dom (- F) & - x in dom (- F) ) ; ::_thesis: (- F) . (- x) = (- F) . x
(- F) . (- x) = - (F . (- x)) by VALUED_1:8
.= - (F . x) by A2, A1, A3, Def3
.= (- F) . x by VALUED_1:8 ;
hence (- F) . (- x) = (- F) . x ; ::_thesis: verum
end;
then ( - F is with_symmetrical_domain & - F is quasi_even ) by A2, A1, Def2, Def3;
hence - F is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:35
for F being PartFunc of REAL,REAL st F is odd holds
F " is odd
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies F " is odd )
A1: dom F = dom (F ") by VALUED_1:def_7;
assume A2: F is odd ; ::_thesis: F " is odd
for x being Real st x in dom (F ") & - x in dom (F ") holds
(F ") . (- x) = - ((F ") . x)
proof
let x be Real; ::_thesis: ( x in dom (F ") & - x in dom (F ") implies (F ") . (- x) = - ((F ") . x) )
assume that
A3: x in dom (F ") and
A4: - x in dom (F ") ; ::_thesis: (F ") . (- x) = - ((F ") . x)
(F ") . (- x) = (F . (- x)) " by A4, VALUED_1:def_7
.= (- (F . x)) " by A2, A1, A3, A4, Def6
.= - ((F . x) ") by XCMPLX_1:222
.= - ((F ") . x) by A3, VALUED_1:def_7 ;
hence (F ") . (- x) = - ((F ") . x) ; ::_thesis: verum
end;
then ( F " is with_symmetrical_domain & F " is quasi_odd ) by A2, A1, Def2, Def6;
hence F " is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:36
for F being PartFunc of REAL,REAL st F is even holds
F " is even
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies F " is even )
A1: dom F = dom (F ") by VALUED_1:def_7;
assume A2: F is even ; ::_thesis: F " is even
for x being Real st x in dom (F ") & - x in dom (F ") holds
(F ") . (- x) = (F ") . x
proof
let x be Real; ::_thesis: ( x in dom (F ") & - x in dom (F ") implies (F ") . (- x) = (F ") . x )
assume that
A3: x in dom (F ") and
A4: - x in dom (F ") ; ::_thesis: (F ") . (- x) = (F ") . x
(F ") . (- x) = (F . (- x)) " by A4, VALUED_1:def_7
.= (F . x) " by A2, A1, A3, A4, Def3
.= (F ") . x by A3, VALUED_1:def_7 ;
hence (F ") . (- x) = (F ") . x ; ::_thesis: verum
end;
then ( F " is with_symmetrical_domain & F " is quasi_even ) by A2, A1, Def2, Def3;
hence F " is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:37
for F being PartFunc of REAL,REAL st F is odd holds
|.F.| is even
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies |.F.| is even )
A1: dom F = dom |.F.| by VALUED_1:def_11;
assume A2: F is odd ; ::_thesis: |.F.| is even
for x being Real st x in dom |.F.| & - x in dom |.F.| holds
|.F.| . (- x) = |.F.| . x
proof
let x be Real; ::_thesis: ( x in dom |.F.| & - x in dom |.F.| implies |.F.| . (- x) = |.F.| . x )
assume that
A3: x in dom |.F.| and
A4: - x in dom |.F.| ; ::_thesis: |.F.| . (- x) = |.F.| . x
|.F.| . (- x) = |.(F . (- x)).| by A4, VALUED_1:def_11
.= |.(- (F . x)).| by A2, A1, A3, A4, Def6
.= |.(F . x).| by COMPLEX1:52
.= |.F.| . x by A3, VALUED_1:def_11 ;
hence |.F.| . (- x) = |.F.| . x ; ::_thesis: verum
end;
then ( |.F.| is with_symmetrical_domain & |.F.| is quasi_even ) by A2, A1, Def2, Def3;
hence |.F.| is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:38
for F being PartFunc of REAL,REAL st F is even holds
|.F.| is even
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies |.F.| is even )
A1: dom F = dom |.F.| by VALUED_1:def_11;
assume A2: F is even ; ::_thesis: |.F.| is even
for x being Real st x in dom |.F.| & - x in dom |.F.| holds
|.F.| . (- x) = |.F.| . x
proof
let x be Real; ::_thesis: ( x in dom |.F.| & - x in dom |.F.| implies |.F.| . (- x) = |.F.| . x )
assume that
A3: x in dom |.F.| and
A4: - x in dom |.F.| ; ::_thesis: |.F.| . (- x) = |.F.| . x
|.F.| . (- x) = |.(F . (- x)).| by A4, VALUED_1:def_11
.= |.(F . x).| by A2, A1, A3, A4, Def3
.= |.F.| . x by A3, VALUED_1:def_11 ;
hence |.F.| . (- x) = |.F.| . x ; ::_thesis: verum
end;
then ( |.F.| is with_symmetrical_domain & |.F.| is quasi_even ) by A2, A1, Def2, Def3;
hence |.F.| is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:39
for F being PartFunc of REAL,REAL st F is odd holds
F ^2 is even
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies F ^2 is even )
A1: dom F = dom (F ^2) by VALUED_1:11;
assume A2: F is odd ; ::_thesis: F ^2 is even
for x being Real st x in dom (F ^2) & - x in dom (F ^2) holds
(F ^2) . (- x) = (F ^2) . x
proof
let x be Real; ::_thesis: ( x in dom (F ^2) & - x in dom (F ^2) implies (F ^2) . (- x) = (F ^2) . x )
assume A3: ( x in dom (F ^2) & - x in dom (F ^2) ) ; ::_thesis: (F ^2) . (- x) = (F ^2) . x
(F ^2) . (- x) = (F . (- x)) ^2 by VALUED_1:11
.= (- (F . x)) ^2 by A2, A1, A3, Def6
.= (F . x) ^2
.= (F ^2) . x by VALUED_1:11 ;
hence (F ^2) . (- x) = (F ^2) . x ; ::_thesis: verum
end;
then ( F ^2 is with_symmetrical_domain & F ^2 is quasi_even ) by A2, A1, Def2, Def3;
hence F ^2 is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:40
for F being PartFunc of REAL,REAL st F is even holds
F ^2 is even
proof
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies F ^2 is even )
A1: dom F = dom (F ^2) by VALUED_1:11;
assume A2: F is even ; ::_thesis: F ^2 is even
for x being Real st x in dom (F ^2) & - x in dom (F ^2) holds
(F ^2) . (- x) = (F ^2) . x
proof
let x be Real; ::_thesis: ( x in dom (F ^2) & - x in dom (F ^2) implies (F ^2) . (- x) = (F ^2) . x )
assume A3: ( x in dom (F ^2) & - x in dom (F ^2) ) ; ::_thesis: (F ^2) . (- x) = (F ^2) . x
(F ^2) . (- x) = (F . (- x)) ^2 by VALUED_1:11
.= (F . x) ^2 by A2, A1, A3, Def3
.= (F ^2) . x by VALUED_1:11 ;
hence (F ^2) . (- x) = (F ^2) . x ; ::_thesis: verum
end;
then ( F ^2 is with_symmetrical_domain & F ^2 is quasi_even ) by A2, A1, Def2, Def3;
hence F ^2 is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:41
for r being Real
for F being PartFunc of REAL,REAL st F is even holds
r + F is even
proof
let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is even holds
r + F is even
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies r + F is even )
A1: dom F = dom (r + F) by VALUED_1:def_2;
assume A2: F is even ; ::_thesis: r + F is even
for x being Real st x in dom (r + F) & - x in dom (r + F) holds
(r + F) . (- x) = (r + F) . x
proof
let x be Real; ::_thesis: ( x in dom (r + F) & - x in dom (r + F) implies (r + F) . (- x) = (r + F) . x )
assume that
A3: x in dom (r + F) and
A4: - x in dom (r + F) ; ::_thesis: (r + F) . (- x) = (r + F) . x
(r + F) . (- x) = r + (F . (- x)) by A4, VALUED_1:def_2
.= r + (F . x) by A2, A1, A3, A4, Def3
.= (r + F) . x by A3, VALUED_1:def_2 ;
hence (r + F) . (- x) = (r + F) . x ; ::_thesis: verum
end;
then ( r + F is with_symmetrical_domain & r + F is quasi_even ) by A2, A1, Def2, Def3;
hence r + F is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:42
for r being Real
for F being PartFunc of REAL,REAL st F is even holds
F - r is even
proof
let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is even holds
F - r is even
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies F - r is even )
A1: dom F = dom (F - r) by VALUED_1:3;
assume A2: F is even ; ::_thesis: F - r is even
for x being Real st x in dom (F - r) & - x in dom (F - r) holds
(F - r) . (- x) = (F - r) . x
proof
let x be Real; ::_thesis: ( x in dom (F - r) & - x in dom (F - r) implies (F - r) . (- x) = (F - r) . x )
assume that
A3: x in dom (F - r) and
A4: - x in dom (F - r) ; ::_thesis: (F - r) . (- x) = (F - r) . x
A5: x in dom F by A3, VALUED_1:3;
- x in dom F by A4, VALUED_1:3;
then (F - r) . (- x) = (F . (- x)) - r by VALUED_1:3
.= (F . x) - r by A2, A1, A3, A4, Def3
.= (F - r) . x by A5, VALUED_1:3 ;
hence (F - r) . (- x) = (F - r) . x ; ::_thesis: verum
end;
then ( F - r is with_symmetrical_domain & F - r is quasi_even ) by A2, A1, Def2, Def3;
hence F - r is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:43
for r being Real
for F being PartFunc of REAL,REAL st F is odd holds
r (#) F is odd
proof
let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is odd holds
r (#) F is odd
let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies r (#) F is odd )
A1: dom F = dom (r (#) F) by VALUED_1:def_5;
assume A2: F is odd ; ::_thesis: r (#) F is odd
for x being Real st x in dom (r (#) F) & - x in dom (r (#) F) holds
(r (#) F) . (- x) = - ((r (#) F) . x)
proof
let x be Real; ::_thesis: ( x in dom (r (#) F) & - x in dom (r (#) F) implies (r (#) F) . (- x) = - ((r (#) F) . x) )
assume that
A3: x in dom (r (#) F) and
A4: - x in dom (r (#) F) ; ::_thesis: (r (#) F) . (- x) = - ((r (#) F) . x)
(r (#) F) . (- x) = r * (F . (- x)) by A4, VALUED_1:def_5
.= r * (- (F . x)) by A2, A1, A3, A4, Def6
.= - (r * (F . x))
.= - ((r (#) F) . x) by A3, VALUED_1:def_5 ;
hence (r (#) F) . (- x) = - ((r (#) F) . x) ; ::_thesis: verum
end;
then ( r (#) F is with_symmetrical_domain & r (#) F is quasi_odd ) by A2, A1, Def2, Def6;
hence r (#) F is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:44
for r being Real
for F being PartFunc of REAL,REAL st F is even holds
r (#) F is even
proof
let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is even holds
r (#) F is even
let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies r (#) F is even )
A1: dom F = dom (r (#) F) by VALUED_1:def_5;
assume A2: F is even ; ::_thesis: r (#) F is even
for x being Real st x in dom (r (#) F) & - x in dom (r (#) F) holds
(r (#) F) . (- x) = (r (#) F) . x
proof
let x be Real; ::_thesis: ( x in dom (r (#) F) & - x in dom (r (#) F) implies (r (#) F) . (- x) = (r (#) F) . x )
assume that
A3: x in dom (r (#) F) and
A4: - x in dom (r (#) F) ; ::_thesis: (r (#) F) . (- x) = (r (#) F) . x
(r (#) F) . (- x) = r * (F . (- x)) by A4, VALUED_1:def_5
.= r * (F . x) by A2, A1, A3, A4, Def3
.= (r (#) F) . x by A3, VALUED_1:def_5 ;
hence (r (#) F) . (- x) = (r (#) F) . x ; ::_thesis: verum
end;
then ( r (#) F is with_symmetrical_domain & r (#) F is quasi_even ) by A2, A1, Def2, Def3;
hence r (#) F is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:45
for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds
F + G is odd
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F + G is odd )
assume that
A1: F is odd and
A2: G is odd and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F + G is odd
A4: (dom F) /\ (dom G) = dom (F + G) by VALUED_1:def_1;
then A5: dom (F + G) c= dom G by XBOOLE_1:17;
A6: dom (F + G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F + G) & - x in dom (F + G) holds
(F + G) . (- x) = - ((F + G) . x)
proof
let x be Real; ::_thesis: ( x in dom (F + G) & - x in dom (F + G) implies (F + G) . (- x) = - ((F + G) . x) )
assume that
A7: x in dom (F + G) and
A8: - x in dom (F + G) ; ::_thesis: (F + G) . (- x) = - ((F + G) . x)
(F + G) . (- x) = (F . (- x)) + (G . (- x)) by A8, VALUED_1:def_1
.= (- (F . x)) + (G . (- x)) by A1, A6, A7, A8, Def6
.= (- (F . x)) + (- (G . x)) by A2, A5, A7, A8, Def6
.= - ((F . x) + (G . x))
.= - ((F + G) . x) by A7, VALUED_1:def_1 ;
hence (F + G) . (- x) = - ((F + G) . x) ; ::_thesis: verum
end;
then ( F + G is with_symmetrical_domain & F + G is quasi_odd ) by A3, A4, Def2, Def6;
hence F + G is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:46
for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds
F + G is even
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F + G is even )
assume that
A1: F is even and
A2: G is even and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F + G is even
A4: (dom F) /\ (dom G) = dom (F + G) by VALUED_1:def_1;
then A5: dom (F + G) c= dom G by XBOOLE_1:17;
A6: dom (F + G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F + G) & - x in dom (F + G) holds
(F + G) . (- x) = (F + G) . x
proof
let x be Real; ::_thesis: ( x in dom (F + G) & - x in dom (F + G) implies (F + G) . (- x) = (F + G) . x )
assume that
A7: x in dom (F + G) and
A8: - x in dom (F + G) ; ::_thesis: (F + G) . (- x) = (F + G) . x
(F + G) . (- x) = (F . (- x)) + (G . (- x)) by A8, VALUED_1:def_1
.= (F . x) + (G . (- x)) by A1, A6, A7, A8, Def3
.= (F . x) + (G . x) by A2, A5, A7, A8, Def3
.= (F + G) . x by A7, VALUED_1:def_1 ;
hence (F + G) . (- x) = (F + G) . x ; ::_thesis: verum
end;
then ( F + G is with_symmetrical_domain & F + G is quasi_even ) by A3, A4, Def2, Def3;
hence F + G is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:47
for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds
F - G is odd
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F - G is odd )
assume that
A1: F is odd and
A2: G is odd and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F - G is odd
A4: (dom F) /\ (dom G) = dom (F - G) by VALUED_1:12;
then A5: dom (F - G) c= dom G by XBOOLE_1:17;
A6: dom (F - G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F - G) & - x in dom (F - G) holds
(F - G) . (- x) = - ((F - G) . x)
proof
let x be Real; ::_thesis: ( x in dom (F - G) & - x in dom (F - G) implies (F - G) . (- x) = - ((F - G) . x) )
assume that
A7: x in dom (F - G) and
A8: - x in dom (F - G) ; ::_thesis: (F - G) . (- x) = - ((F - G) . x)
(F - G) . (- x) = (F . (- x)) - (G . (- x)) by A8, VALUED_1:13
.= (- (F . x)) - (G . (- x)) by A1, A6, A7, A8, Def6
.= (- (F . x)) - (- (G . x)) by A2, A5, A7, A8, Def6
.= - ((F . x) - (G . x))
.= - ((F - G) . x) by A7, VALUED_1:13 ;
hence (F - G) . (- x) = - ((F - G) . x) ; ::_thesis: verum
end;
then ( F - G is with_symmetrical_domain & F - G is quasi_odd ) by A3, A4, Def2, Def6;
hence F - G is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:48
for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds
F - G is even
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F - G is even )
assume that
A1: F is even and
A2: G is even and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F - G is even
A4: (dom F) /\ (dom G) = dom (F - G) by VALUED_1:12;
then A5: dom (F - G) c= dom G by XBOOLE_1:17;
A6: dom (F - G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F - G) & - x in dom (F - G) holds
(F - G) . (- x) = (F - G) . x
proof
let x be Real; ::_thesis: ( x in dom (F - G) & - x in dom (F - G) implies (F - G) . (- x) = (F - G) . x )
assume that
A7: x in dom (F - G) and
A8: - x in dom (F - G) ; ::_thesis: (F - G) . (- x) = (F - G) . x
(F - G) . (- x) = (F . (- x)) - (G . (- x)) by A8, VALUED_1:13
.= (F . x) - (G . (- x)) by A1, A6, A7, A8, Def3
.= (F . x) - (G . x) by A2, A5, A7, A8, Def3
.= (F - G) . x by A7, VALUED_1:13 ;
hence (F - G) . (- x) = (F - G) . x ; ::_thesis: verum
end;
then ( F - G is with_symmetrical_domain & F - G is quasi_even ) by A3, A4, Def2, Def3;
hence F - G is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:49
for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds
F (#) G is even
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F (#) G is even )
assume that
A1: F is odd and
A2: G is odd and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F (#) G is even
A4: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def_4;
then A5: dom (F (#) G) c= dom G by XBOOLE_1:17;
A6: dom (F (#) G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F (#) G) & - x in dom (F (#) G) holds
(F (#) G) . (- x) = (F (#) G) . x
proof
let x be Real; ::_thesis: ( x in dom (F (#) G) & - x in dom (F (#) G) implies (F (#) G) . (- x) = (F (#) G) . x )
assume that
A7: x in dom (F (#) G) and
A8: - x in dom (F (#) G) ; ::_thesis: (F (#) G) . (- x) = (F (#) G) . x
(F (#) G) . (- x) = (F . (- x)) * (G . (- x)) by A8, VALUED_1:def_4
.= (- (F . x)) * (G . (- x)) by A1, A6, A7, A8, Def6
.= (- (F . x)) * (- (G . x)) by A2, A5, A7, A8, Def6
.= (F . x) * (G . x)
.= (F (#) G) . x by A7, VALUED_1:def_4 ;
hence (F (#) G) . (- x) = (F (#) G) . x ; ::_thesis: verum
end;
then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_even ) by A3, A4, Def2, Def3;
hence F (#) G is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:50
for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds
F (#) G is even
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F (#) G is even )
assume that
A1: F is even and
A2: G is even and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F (#) G is even
A4: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def_4;
then A5: dom (F (#) G) c= dom G by XBOOLE_1:17;
A6: dom (F (#) G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F (#) G) & - x in dom (F (#) G) holds
(F (#) G) . (- x) = (F (#) G) . x
proof
let x be Real; ::_thesis: ( x in dom (F (#) G) & - x in dom (F (#) G) implies (F (#) G) . (- x) = (F (#) G) . x )
assume that
A7: x in dom (F (#) G) and
A8: - x in dom (F (#) G) ; ::_thesis: (F (#) G) . (- x) = (F (#) G) . x
(F (#) G) . (- x) = (F . (- x)) * (G . (- x)) by A8, VALUED_1:def_4
.= (F . x) * (G . (- x)) by A1, A6, A7, A8, Def3
.= (F . x) * (G . x) by A2, A5, A7, A8, Def3
.= (F (#) G) . x by A7, VALUED_1:def_4 ;
hence (F (#) G) . (- x) = (F (#) G) . x ; ::_thesis: verum
end;
then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_even ) by A3, A4, Def2, Def3;
hence F (#) G is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:51
for F, G being PartFunc of REAL,REAL st F is even & G is odd & (dom F) /\ (dom G) is symmetrical holds
F (#) G is odd
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is odd & (dom F) /\ (dom G) is symmetrical implies F (#) G is odd )
assume that
A1: F is even and
A2: G is odd and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F (#) G is odd
A4: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def_4;
then A5: dom (F (#) G) c= dom G by XBOOLE_1:17;
A6: dom (F (#) G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F (#) G) & - x in dom (F (#) G) holds
(F (#) G) . (- x) = - ((F (#) G) . x)
proof
let x be Real; ::_thesis: ( x in dom (F (#) G) & - x in dom (F (#) G) implies (F (#) G) . (- x) = - ((F (#) G) . x) )
assume that
A7: x in dom (F (#) G) and
A8: - x in dom (F (#) G) ; ::_thesis: (F (#) G) . (- x) = - ((F (#) G) . x)
(F (#) G) . (- x) = (F . (- x)) * (G . (- x)) by A8, VALUED_1:def_4
.= (F . x) * (G . (- x)) by A1, A6, A7, A8, Def3
.= (F . x) * (- (G . x)) by A2, A5, A7, A8, Def6
.= - ((F . x) * (G . x))
.= - ((F (#) G) . x) by A7, VALUED_1:def_4 ;
hence (F (#) G) . (- x) = - ((F (#) G) . x) ; ::_thesis: verum
end;
then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_odd ) by A3, A4, Def2, Def6;
hence F (#) G is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:52
for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds
F /" G is even
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F /" G is even )
assume that
A1: F is odd and
A2: G is odd and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is even
A4: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F /" G) & - x in dom (F /" G) holds
(F /" G) . (- x) = (F /" G) . x
proof
let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = (F /" G) . x )
assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = (F /" G) . x
(F /" G) . (- x) = (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (- (F . x)) / (G . (- x)) by A1, A6, A7, Def6
.= (- (F . x)) / (- (G . x)) by A2, A5, A7, Def6
.= (F . x) / (G . x) by XCMPLX_1:191
.= (F /" G) . x by VALUED_1:17 ;
hence (F /" G) . (- x) = (F /" G) . x ; ::_thesis: verum
end;
then ( F /" G is with_symmetrical_domain & F /" G is quasi_even ) by A3, A4, Def2, Def3;
hence F /" G is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:53
for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds
F /" G is even
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F /" G is even )
assume that
A1: F is even and
A2: G is even and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is even
A4: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F /" G) & - x in dom (F /" G) holds
(F /" G) . (- x) = (F /" G) . x
proof
let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = (F /" G) . x )
assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = (F /" G) . x
(F /" G) . (- x) = (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F . x) / (G . (- x)) by A1, A6, A7, Def3
.= (F . x) / (G . x) by A2, A5, A7, Def3
.= (F /" G) . x by VALUED_1:17 ;
hence (F /" G) . (- x) = (F /" G) . x ; ::_thesis: verum
end;
then ( F /" G is with_symmetrical_domain & F /" G is quasi_even ) by A3, A4, Def2, Def3;
hence F /" G is even ; ::_thesis: verum
end;
theorem :: FUNCT_8:54
for F, G being PartFunc of REAL,REAL st F is odd & G is even & (dom F) /\ (dom G) is symmetrical holds
F /" G is odd
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is even & (dom F) /\ (dom G) is symmetrical implies F /" G is odd )
assume that
A1: F is odd and
A2: G is even and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is odd
A4: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F /" G) & - x in dom (F /" G) holds
(F /" G) . (- x) = - ((F /" G) . x)
proof
let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = - ((F /" G) . x) )
assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = - ((F /" G) . x)
(F /" G) . (- x) = (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (- (F . x)) / (G . (- x)) by A1, A6, A7, Def6
.= (- (F . x)) / (G . x) by A2, A5, A7, Def3
.= - ((F . x) / (G . x))
.= - ((F /" G) . x) by VALUED_1:17 ;
hence (F /" G) . (- x) = - ((F /" G) . x) ; ::_thesis: verum
end;
then ( F /" G is with_symmetrical_domain & F /" G is quasi_odd ) by A3, A4, Def2, Def6;
hence F /" G is odd ; ::_thesis: verum
end;
theorem :: FUNCT_8:55
for F, G being PartFunc of REAL,REAL st F is even & G is odd & (dom F) /\ (dom G) is symmetrical holds
F /" G is odd
proof
let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is odd & (dom F) /\ (dom G) is symmetrical implies F /" G is odd )
assume that
A1: F is even and
A2: G is odd and
A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is odd
A4: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
then A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4, XBOOLE_1:17;
for x being Real st x in dom (F /" G) & - x in dom (F /" G) holds
(F /" G) . (- x) = - ((F /" G) . x)
proof
let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = - ((F /" G) . x) )
assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = - ((F /" G) . x)
(F /" G) . (- x) = (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F . x) / (G . (- x)) by A1, A6, A7, Def3
.= (F . x) / (- (G . x)) by A2, A5, A7, Def6
.= - ((F . x) / (G . x)) by XCMPLX_1:188
.= - ((F /" G) . x) by VALUED_1:17 ;
hence (F /" G) . (- x) = - ((F /" G) . x) ; ::_thesis: verum
end;
then ( F /" G is with_symmetrical_domain & F /" G is quasi_odd ) by A3, A4, Def2, Def6;
hence F /" G is odd ; ::_thesis: verum
end;
begin
definition
func signum -> Function of REAL,REAL means :Def9: :: FUNCT_8:def 9
for x being Real holds it . x = sgn x;
existence
ex b1 being Function of REAL,REAL st
for x being Real holds b1 . x = sgn x
proof
deffunc H1( Element of REAL ) -> Element of REAL = sgn $1;
consider f being Function of REAL,REAL such that
A1: for x being Real holds f . x = H1(x) from FUNCT_2:sch_4();
take f ; ::_thesis: for x being Real holds f . x = sgn x
thus for x being Real holds f . x = sgn x by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for x being Real holds b1 . x = sgn x ) & ( for x being Real holds b2 . x = sgn x ) holds
b1 = b2
proof
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f1 . x = sgn x ) & ( for x being Real holds f2 . x = sgn x ) implies f1 = f2 )
assume A2: for x being Real holds f1 . x = sgn x ; ::_thesis: ( ex x being Real st not f2 . x = sgn x or f1 = f2 )
assume A3: for x being Real holds f2 . x = sgn x ; ::_thesis: f1 = f2
for x being Real holds f1 . x = f2 . x
proof
let x be Real; ::_thesis: f1 . x = f2 . x
thus f1 . x = sgn x by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines signum FUNCT_8:def_9_:_
for b1 being Function of REAL,REAL holds
( b1 = signum iff for x being Real holds b1 . x = sgn x );
theorem Th56: :: FUNCT_8:56
for x being real number st x > 0 holds
signum . x = 1
proof
let x be real number ; ::_thesis: ( x > 0 implies signum . x = 1 )
assume A1: 0 < x ; ::_thesis: signum . x = 1
x in REAL by XREAL_0:def_1;
then signum . x = sgn x by Def9
.= 1 by A1, ABSVALUE:def_2 ;
hence signum . x = 1 ; ::_thesis: verum
end;
theorem Th57: :: FUNCT_8:57
for x being real number st x < 0 holds
signum . x = - 1
proof
let x be real number ; ::_thesis: ( x < 0 implies signum . x = - 1 )
assume A1: 0 > x ; ::_thesis: signum . x = - 1
x in REAL by XREAL_0:def_1;
then signum . x = sgn x by Def9
.= - 1 by A1, ABSVALUE:def_2 ;
hence signum . x = - 1 ; ::_thesis: verum
end;
theorem Th58: :: FUNCT_8:58
signum . 0 = 0
proof
signum . 0 = sgn 0 by Def9
.= 0 by ABSVALUE:def_2 ;
hence signum . 0 = 0 ; ::_thesis: verum
end;
theorem Th59: :: FUNCT_8:59
for x being real number holds signum . (- x) = - (signum . x)
proof
let x be real number ; ::_thesis: signum . (- x) = - (signum . x)
percases ( x < 0 or 0 < x or x = 0 ) ;
supposeA1: x < 0 ; ::_thesis: signum . (- x) = - (signum . x)
then signum . x = - 1 by Th57;
hence signum . (- x) = - (signum . x) by A1, Th56; ::_thesis: verum
end;
supposeA2: 0 < x ; ::_thesis: signum . (- x) = - (signum . x)
then signum . x = 1 by Th56;
hence signum . (- x) = - (signum . x) by A2, Th57; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: signum . (- x) = - (signum . x)
hence signum . (- x) = - (signum . x) by Th58; ::_thesis: verum
end;
end;
end;
theorem :: FUNCT_8:60
for A being symmetrical Subset of REAL holds signum is_odd_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: signum is_odd_on A
A1: dom signum = REAL by FUNCT_2:def_1;
then A2: dom (signum | A) = A by RELAT_1:62;
for x being Real st x in dom (signum | A) & - x in dom (signum | A) holds
(signum | A) . (- x) = - ((signum | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (signum | A) & - x in dom (signum | A) implies (signum | A) . (- x) = - ((signum | A) . x) )
assume that
A3: x in dom (signum | A) and
A4: - x in dom (signum | A) ; ::_thesis: (signum | A) . (- x) = - ((signum | A) . x)
(signum | A) . (- x) = (signum | A) /. (- x) by A4, PARTFUN1:def_6
.= signum /. (- x) by A1, A4, PARTFUN2:17
.= - (signum /. x) by Th59
.= - ((signum | A) /. x) by A1, A3, PARTFUN2:17
.= - ((signum | A) . x) by A3, PARTFUN1:def_6 ;
hence (signum | A) . (- x) = - ((signum | A) . x) ; ::_thesis: verum
end;
then ( signum | A is with_symmetrical_domain & signum | A is quasi_odd ) by A2, Def2, Def6;
hence signum is_odd_on A by A1, Def8; ::_thesis: verum
end;
theorem Th61: :: FUNCT_8:61
for x being real number st x >= 0 holds
absreal . x = x
proof
let x be real number ; ::_thesis: ( x >= 0 implies absreal . x = x )
assume A1: 0 <= x ; ::_thesis: absreal . x = x
absreal . x = abs x by EUCLID:def_2
.= x by A1, ABSVALUE:def_1 ;
hence absreal . x = x ; ::_thesis: verum
end;
theorem Th62: :: FUNCT_8:62
for x being real number st x < 0 holds
absreal . x = - x
proof
let x be real number ; ::_thesis: ( x < 0 implies absreal . x = - x )
assume A1: 0 > x ; ::_thesis: absreal . x = - x
absreal . x = abs x by EUCLID:def_2
.= - x by A1, ABSVALUE:def_1 ;
hence absreal . x = - x ; ::_thesis: verum
end;
theorem Th63: :: FUNCT_8:63
for x being real number holds absreal . (- x) = absreal . x
proof
let x be real number ; ::_thesis: absreal . (- x) = absreal . x
percases ( x < 0 or 0 < x or x = 0 ) ;
supposeA1: x < 0 ; ::_thesis: absreal . (- x) = absreal . x
then absreal . (- x) = - x by Th61;
hence absreal . (- x) = absreal . x by A1, Th62; ::_thesis: verum
end;
supposeA2: 0 < x ; ::_thesis: absreal . (- x) = absreal . x
then absreal . (- x) = - (- x) by Th62
.= x ;
hence absreal . (- x) = absreal . x by A2, Th61; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: absreal . (- x) = absreal . x
hence absreal . (- x) = absreal . x ; ::_thesis: verum
end;
end;
end;
theorem :: FUNCT_8:64
for A being symmetrical Subset of REAL holds absreal is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: absreal is_even_on A
A1: dom absreal = REAL by FUNCT_2:def_1;
then A2: dom (absreal | A) = A by RELAT_1:62;
for x being Real st x in dom (absreal | A) & - x in dom (absreal | A) holds
(absreal | A) . (- x) = (absreal | A) . x
proof
let x be Real; ::_thesis: ( x in dom (absreal | A) & - x in dom (absreal | A) implies (absreal | A) . (- x) = (absreal | A) . x )
assume that
A3: x in dom (absreal | A) and
A4: - x in dom (absreal | A) ; ::_thesis: (absreal | A) . (- x) = (absreal | A) . x
(absreal | A) . (- x) = (absreal | A) /. (- x) by A4, PARTFUN1:def_6
.= absreal /. (- x) by A1, A4, PARTFUN2:17
.= absreal /. x by Th63
.= (absreal | A) /. x by A1, A3, PARTFUN2:17
.= (absreal | A) . x by A3, PARTFUN1:def_6 ;
hence (absreal | A) . (- x) = (absreal | A) . x ; ::_thesis: verum
end;
then ( absreal | A is with_symmetrical_domain & absreal | A is quasi_even ) by A2, Def2, Def3;
hence absreal is_even_on A by A1, Def5; ::_thesis: verum
end;
theorem Th65: :: FUNCT_8:65
for A being symmetrical Subset of REAL holds sin is_odd_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: sin is_odd_on A
A1: dom (sin | A) = A by RELAT_1:62, SIN_COS:24;
for x being Real st x in dom (sin | A) & - x in dom (sin | A) holds
(sin | A) . (- x) = - ((sin | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (sin | A) & - x in dom (sin | A) implies (sin | A) . (- x) = - ((sin | A) . x) )
assume that
A2: x in dom (sin | A) and
A3: - x in dom (sin | A) ; ::_thesis: (sin | A) . (- x) = - ((sin | A) . x)
(sin | A) . (- x) = (sin | A) /. (- x) by A3, PARTFUN1:def_6
.= sin /. (- x) by A3, PARTFUN2:17, SIN_COS:24
.= - (sin /. x) by SIN_COS:30
.= - ((sin | A) /. x) by A2, PARTFUN2:17, SIN_COS:24
.= - ((sin | A) . x) by A2, PARTFUN1:def_6 ;
hence (sin | A) . (- x) = - ((sin | A) . x) ; ::_thesis: verum
end;
then ( sin | A is with_symmetrical_domain & sin | A is quasi_odd ) by A1, Def2, Def6;
hence sin is_odd_on A by Def8, SIN_COS:24; ::_thesis: verum
end;
theorem Th66: :: FUNCT_8:66
for A being symmetrical Subset of REAL holds cos is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: cos is_even_on A
A1: dom (cos | A) = A by RELAT_1:62, SIN_COS:24;
for x being Real st x in dom (cos | A) & - x in dom (cos | A) holds
(cos | A) . (- x) = (cos | A) . x
proof
let x be Real; ::_thesis: ( x in dom (cos | A) & - x in dom (cos | A) implies (cos | A) . (- x) = (cos | A) . x )
assume that
A2: x in dom (cos | A) and
A3: - x in dom (cos | A) ; ::_thesis: (cos | A) . (- x) = (cos | A) . x
(cos | A) . (- x) = (cos | A) /. (- x) by A3, PARTFUN1:def_6
.= cos /. (- x) by A3, PARTFUN2:17, SIN_COS:24
.= cos /. x by SIN_COS:30
.= (cos | A) /. x by A2, PARTFUN2:17, SIN_COS:24
.= (cos | A) . x by A2, PARTFUN1:def_6 ;
hence (cos | A) . (- x) = (cos | A) . x ; ::_thesis: verum
end;
then ( cos | A is with_symmetrical_domain & cos | A is quasi_even ) by A1, Def2, Def3;
hence cos is_even_on A by Def5, SIN_COS:24; ::_thesis: verum
end;
registration
cluster sin -> odd ;
coherence
sin is odd
proof
for x being complex number st x in REAL holds
- x in REAL by XREAL_0:def_1;
then ( ( for x being Real st x in dom sin & - x in dom sin holds
sin . (- x) = - (sin . x) ) & REAL is symmetrical ) by Def1, SIN_COS:30;
then ( sin is with_symmetrical_domain & sin is quasi_odd ) by Def2, Def6, SIN_COS:24;
hence sin is odd ; ::_thesis: verum
end;
end;
registration
cluster cos -> even ;
coherence
cos is even
proof
for x being Real st x in dom cos & - x in dom cos holds
cos . (- x) = cos . x by SIN_COS:30;
then ( cos is with_symmetrical_domain & cos is quasi_even ) by Def2, Def3, SIN_COS:24;
hence cos is even ; ::_thesis: verum
end;
end;
theorem :: FUNCT_8:67
for A being symmetrical Subset of REAL holds sinh is_odd_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: sinh is_odd_on A
A1: dom sinh = REAL by FUNCT_2:def_1;
then A2: dom (sinh | A) = A by RELAT_1:62;
for x being Real st x in dom (sinh | A) & - x in dom (sinh | A) holds
(sinh | A) . (- x) = - ((sinh | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (sinh | A) & - x in dom (sinh | A) implies (sinh | A) . (- x) = - ((sinh | A) . x) )
assume that
A3: x in dom (sinh | A) and
A4: - x in dom (sinh | A) ; ::_thesis: (sinh | A) . (- x) = - ((sinh | A) . x)
(sinh | A) . (- x) = (sinh | A) /. (- x) by A4, PARTFUN1:def_6
.= sinh /. (- x) by A1, A4, PARTFUN2:17
.= - (sinh /. x) by SIN_COS2:19
.= - ((sinh | A) /. x) by A1, A3, PARTFUN2:17
.= - ((sinh | A) . x) by A3, PARTFUN1:def_6 ;
hence (sinh | A) . (- x) = - ((sinh | A) . x) ; ::_thesis: verum
end;
then ( sinh | A is with_symmetrical_domain & sinh | A is quasi_odd ) by A2, Def2, Def6;
hence sinh is_odd_on A by A1, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:68
for A being symmetrical Subset of REAL holds cosh is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: cosh is_even_on A
A1: dom cosh = REAL by FUNCT_2:def_1;
then A2: dom (cosh | A) = A by RELAT_1:62;
for x being Real st x in dom (cosh | A) & - x in dom (cosh | A) holds
(cosh | A) . (- x) = (cosh | A) . x
proof
let x be Real; ::_thesis: ( x in dom (cosh | A) & - x in dom (cosh | A) implies (cosh | A) . (- x) = (cosh | A) . x )
assume that
A3: x in dom (cosh | A) and
A4: - x in dom (cosh | A) ; ::_thesis: (cosh | A) . (- x) = (cosh | A) . x
(cosh | A) . (- x) = (cosh | A) /. (- x) by A4, PARTFUN1:def_6
.= cosh /. (- x) by A1, A4, PARTFUN2:17
.= cosh /. x by SIN_COS2:19
.= (cosh | A) /. x by A1, A3, PARTFUN2:17
.= (cosh | A) . x by A3, PARTFUN1:def_6 ;
hence (cosh | A) . (- x) = (cosh | A) . x ; ::_thesis: verum
end;
then ( cosh | A is with_symmetrical_domain & cosh | A is quasi_even ) by A2, Def2, Def3;
hence cosh is_even_on A by A1, Def5; ::_thesis: verum
end;
registration
cluster sinh -> odd ;
coherence
sinh is odd
proof
for x being complex number st x in REAL holds
- x in REAL by XREAL_0:def_1;
then A1: REAL is symmetrical by Def1;
( ( for x being Real st x in dom sinh & - x in dom sinh holds
sinh . (- x) = - (sinh . x) ) & dom sinh = REAL ) by FUNCT_2:def_1, SIN_COS2:19;
then ( sinh is with_symmetrical_domain & sinh is quasi_odd ) by A1, Def2, Def6;
hence sinh is odd ; ::_thesis: verum
end;
end;
registration
cluster cosh -> even ;
coherence
cosh is even
proof
for x being complex number st x in REAL holds
- x in REAL by XREAL_0:def_1;
then A1: REAL is symmetrical by Def1;
( ( for x being Real st x in dom cosh & - x in dom cosh holds
cosh . (- x) = cosh . x ) & dom cosh = REAL ) by FUNCT_2:def_1, SIN_COS2:19;
then ( cosh is with_symmetrical_domain & cosh is quasi_even ) by A1, Def2, Def3;
hence cosh is even ; ::_thesis: verum
end;
end;
theorem :: FUNCT_8:69
for A being symmetrical Subset of COMPLEX st A c= ].(- (PI / 2)),(PI / 2).[ holds
tan is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= ].(- (PI / 2)),(PI / 2).[ implies tan is_odd_on A )
assume A1: A c= ].(- (PI / 2)),(PI / 2).[ ; ::_thesis: tan is_odd_on A
then A2: A c= dom tan by SIN_COS9:1, XBOOLE_1:1;
A3: dom (tan | A) = A by A1, RELAT_1:62, SIN_COS9:1, XBOOLE_1:1;
A4: for x being Real st x in A holds
tan . (- x) = - (tan . x)
proof
let x be Real; ::_thesis: ( x in A implies tan . (- x) = - (tan . x) )
assume A5: x in A ; ::_thesis: tan . (- x) = - (tan . x)
then - x in A by Def1;
then tan . (- x) = tan (- x) by A1, SIN_COS9:13
.= - (tan x) by SIN_COS4:1
.= - (tan . x) by A1, A5, SIN_COS9:13 ;
hence tan . (- x) = - (tan . x) ; ::_thesis: verum
end;
for x being Real st x in dom (tan | A) & - x in dom (tan | A) holds
(tan | A) . (- x) = - ((tan | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (tan | A) & - x in dom (tan | A) implies (tan | A) . (- x) = - ((tan | A) . x) )
assume that
A6: x in dom (tan | A) and
A7: - x in dom (tan | A) ; ::_thesis: (tan | A) . (- x) = - ((tan | A) . x)
(tan | A) . (- x) = (tan | A) /. (- x) by A7, PARTFUN1:def_6
.= tan /. (- x) by A2, A3, A7, PARTFUN2:17
.= tan . (- x) by A2, A3, A7, PARTFUN1:def_6
.= - (tan . x) by A4, A6
.= - (tan /. x) by A2, A3, A6, PARTFUN1:def_6
.= - ((tan | A) /. x) by A2, A3, A6, PARTFUN2:17
.= - ((tan | A) . x) by A6, PARTFUN1:def_6 ;
hence (tan | A) . (- x) = - ((tan | A) . x) ; ::_thesis: verum
end;
then ( tan | A is with_symmetrical_domain & tan | A is quasi_odd ) by A3, Def2, Def6;
hence tan is_odd_on A by A2, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:70
for A being symmetrical Subset of COMPLEX st A c= dom tan holds
tan is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= dom tan implies tan is_odd_on A )
assume A1: A c= dom tan ; ::_thesis: tan is_odd_on A
A2: dom (tan | A) = A by A1, RELAT_1:62;
A3: for x being Real st x in A holds
tan . (- x) = - (tan . x)
proof
let x be Real; ::_thesis: ( x in A implies tan . (- x) = - (tan . x) )
assume A4: x in A ; ::_thesis: tan . (- x) = - (tan . x)
then A5: cos . x <> 0 by A1, FDIFF_8:1;
- x in A by Def1, A4;
then tan . (- x) = tan (- x) by A1, FDIFF_8:1, SIN_COS9:15
.= - (tan x) by SIN_COS4:1
.= - (tan . x) by A5, SIN_COS9:15 ;
hence tan . (- x) = - (tan . x) ; ::_thesis: verum
end;
for x being Real st x in dom (tan | A) & - x in dom (tan | A) holds
(tan | A) . (- x) = - ((tan | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (tan | A) & - x in dom (tan | A) implies (tan | A) . (- x) = - ((tan | A) . x) )
assume that
A6: x in dom (tan | A) and
A7: - x in dom (tan | A) ; ::_thesis: (tan | A) . (- x) = - ((tan | A) . x)
(tan | A) . (- x) = (tan | A) /. (- x) by A7, PARTFUN1:def_6
.= tan /. (- x) by A1, A2, A7, PARTFUN2:17
.= tan . (- x) by A1, A2, A7, PARTFUN1:def_6
.= - (tan . x) by A3, A6
.= - (tan /. x) by A1, A2, A6, PARTFUN1:def_6
.= - ((tan | A) /. x) by A1, A2, A6, PARTFUN2:17
.= - ((tan | A) . x) by A6, PARTFUN1:def_6 ;
hence (tan | A) . (- x) = - ((tan | A) . x) ; ::_thesis: verum
end;
then ( tan | A is with_symmetrical_domain & tan | A is quasi_odd ) by A2, Def2, Def6;
hence tan is_odd_on A by A1, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:71
for A being symmetrical Subset of COMPLEX st A c= dom cot holds
cot is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= dom cot implies cot is_odd_on A )
assume A1: A c= dom cot ; ::_thesis: cot is_odd_on A
A2: dom (cot | A) = A by A1, RELAT_1:62;
A3: for x being Real st x in A holds
cot . (- x) = - (cot . x)
proof
let x be Real; ::_thesis: ( x in A implies cot . (- x) = - (cot . x) )
assume A4: x in A ; ::_thesis: cot . (- x) = - (cot . x)
then A5: sin . x <> 0 by A1, FDIFF_8:2;
- x in A by A4, Def1;
then cot . (- x) = cot (- x) by A1, FDIFF_8:2, SIN_COS9:16
.= - (cot x) by SIN_COS4:3
.= - (cot . x) by A5, SIN_COS9:16 ;
hence cot . (- x) = - (cot . x) ; ::_thesis: verum
end;
for x being Real st x in dom (cot | A) & - x in dom (cot | A) holds
(cot | A) . (- x) = - ((cot | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (cot | A) & - x in dom (cot | A) implies (cot | A) . (- x) = - ((cot | A) . x) )
assume that
A6: x in dom (cot | A) and
A7: - x in dom (cot | A) ; ::_thesis: (cot | A) . (- x) = - ((cot | A) . x)
(cot | A) . (- x) = (cot | A) /. (- x) by A7, PARTFUN1:def_6
.= cot /. (- x) by A1, A2, A7, PARTFUN2:17
.= cot . (- x) by A1, A2, A7, PARTFUN1:def_6
.= - (cot . x) by A3, A6
.= - (cot /. x) by A1, A2, A6, PARTFUN1:def_6
.= - ((cot | A) /. x) by A1, A2, A6, PARTFUN2:17
.= - ((cot | A) . x) by A6, PARTFUN1:def_6 ;
hence (cot | A) . (- x) = - ((cot | A) . x) ; ::_thesis: verum
end;
then ( cot | A is with_symmetrical_domain & cot | A is quasi_odd ) by A2, Def2, Def6;
hence cot is_odd_on A by A1, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:72
for A being symmetrical Subset of COMPLEX st A c= [.(- 1),1.] holds
arctan is_odd_on A
proof
let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= [.(- 1),1.] implies arctan is_odd_on A )
assume A1: A c= [.(- 1),1.] ; ::_thesis: arctan is_odd_on A
then A2: A c= dom arctan by SIN_COS9:23, XBOOLE_1:1;
A3: dom (arctan | A) = A by A1, RELAT_1:62, SIN_COS9:23, XBOOLE_1:1;
A4: for x being Real st x in A holds
arctan . (- x) = - (arctan . x)
proof
let x be Real; ::_thesis: ( x in A implies arctan . (- x) = - (arctan . x) )
assume x in A ; ::_thesis: arctan . (- x) = - (arctan . x)
then ( - 1 <= x & x <= 1 ) by A1, XXREAL_1:1;
then arctan x = - (arctan (- x)) by SIN_COS9:67;
hence arctan . (- x) = - (arctan . x) ; ::_thesis: verum
end;
for x being Real st x in dom (arctan | A) & - x in dom (arctan | A) holds
(arctan | A) . (- x) = - ((arctan | A) . x)
proof
let x be Real; ::_thesis: ( x in dom (arctan | A) & - x in dom (arctan | A) implies (arctan | A) . (- x) = - ((arctan | A) . x) )
assume that
A5: x in dom (arctan | A) and
A6: - x in dom (arctan | A) ; ::_thesis: (arctan | A) . (- x) = - ((arctan | A) . x)
(arctan | A) . (- x) = (arctan | A) /. (- x) by A6, PARTFUN1:def_6
.= arctan /. (- x) by A2, A3, A6, PARTFUN2:17
.= arctan . (- x) by A2, A3, A6, PARTFUN1:def_6
.= - (arctan . x) by A4, A5
.= - (arctan /. x) by A2, A3, A5, PARTFUN1:def_6
.= - ((arctan | A) /. x) by A2, A3, A5, PARTFUN2:17
.= - ((arctan | A) . x) by A5, PARTFUN1:def_6 ;
hence (arctan | A) . (- x) = - ((arctan | A) . x) ; ::_thesis: verum
end;
then ( arctan | A is with_symmetrical_domain & arctan | A is quasi_odd ) by A3, Def2, Def6;
hence arctan is_odd_on A by A2, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:73
for A being symmetrical Subset of REAL holds |.sin.| is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: |.sin.| is_even_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence |.sin.| is_even_on A by Th20, Th65; ::_thesis: verum
end;
theorem :: FUNCT_8:74
for A being symmetrical Subset of REAL holds |.cos.| is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: |.cos.| is_even_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence |.cos.| is_even_on A by Th21, Th66; ::_thesis: verum
end;
theorem :: FUNCT_8:75
for A being symmetrical Subset of REAL holds sin " is_odd_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: sin " is_odd_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence sin " is_odd_on A by Th18, Th65; ::_thesis: verum
end;
theorem :: FUNCT_8:76
for A being symmetrical Subset of REAL holds cos " is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: cos " is_even_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence cos " is_even_on A by Th19, Th66; ::_thesis: verum
end;
theorem :: FUNCT_8:77
for A being symmetrical Subset of REAL holds - sin is_odd_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: - sin is_odd_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence - sin is_odd_on A by Th16, Th65; ::_thesis: verum
end;
theorem :: FUNCT_8:78
for A being symmetrical Subset of REAL holds - cos is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: - cos is_even_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence - cos is_even_on A by Th17, Th66; ::_thesis: verum
end;
theorem :: FUNCT_8:79
for A being symmetrical Subset of REAL holds sin ^2 is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: sin ^2 is_even_on A
( A is symmetrical Subset of COMPLEX & sin is_odd_on A ) by Th65, NUMBERS:11, XBOOLE_1:1;
hence sin ^2 is_even_on A by Th22; ::_thesis: verum
end;
theorem :: FUNCT_8:80
for A being symmetrical Subset of REAL holds cos ^2 is_even_on A
proof
let A be symmetrical Subset of REAL; ::_thesis: cos ^2 is_even_on A
( A is symmetrical Subset of COMPLEX & cos is_even_on A ) by Th66, NUMBERS:11, XBOOLE_1:1;
hence cos ^2 is_even_on A by Th23; ::_thesis: verum
end;
theorem Th81: :: FUNCT_8:81
for B being symmetrical Subset of REAL st B c= dom sec holds
sec is_even_on B
proof
let B be symmetrical Subset of REAL; ::_thesis: ( B c= dom sec implies sec is_even_on B )
assume A1: B c= dom sec ; ::_thesis: sec is_even_on B
then A2: dom (sec | B) = B by RELAT_1:62;
A3: for x being Real st x in B holds
sec . (- x) = sec . x
proof
let x be Real; ::_thesis: ( x in B implies sec . (- x) = sec . x )
assume A4: x in B ; ::_thesis: sec . (- x) = sec . x
then - x in B by Def1;
then sec . (- x) = (cos . (- x)) " by A1, RFUNCT_1:def_2
.= (cos . x) " by SIN_COS:30
.= sec . x by A1, A4, RFUNCT_1:def_2 ;
hence sec . (- x) = sec . x ; ::_thesis: verum
end;
for x being Real st x in dom (sec | B) & - x in dom (sec | B) holds
(sec | B) . (- x) = (sec | B) . x
proof
let x be Real; ::_thesis: ( x in dom (sec | B) & - x in dom (sec | B) implies (sec | B) . (- x) = (sec | B) . x )
assume that
A5: x in dom (sec | B) and
A6: - x in dom (sec | B) ; ::_thesis: (sec | B) . (- x) = (sec | B) . x
(sec | B) . (- x) = (sec | B) /. (- x) by A6, PARTFUN1:def_6
.= sec /. (- x) by A1, A2, A6, PARTFUN2:17
.= sec . (- x) by A1, A2, A6, PARTFUN1:def_6
.= sec . x by A3, A5
.= sec /. x by A1, A2, A5, PARTFUN1:def_6
.= (sec | B) /. x by A1, A2, A5, PARTFUN2:17
.= (sec | B) . x by A5, PARTFUN1:def_6 ;
hence (sec | B) . (- x) = (sec | B) . x ; ::_thesis: verum
end;
then ( sec | B is with_symmetrical_domain & sec | B is quasi_even ) by A2, Def2, Def3;
hence sec is_even_on B by A1, Def5; ::_thesis: verum
end;
theorem :: FUNCT_8:82
for B being symmetrical Subset of REAL st ( for x being real number st x in B holds
cos . x <> 0 ) holds
sec is_even_on B
proof
let B be symmetrical Subset of REAL; ::_thesis: ( ( for x being real number st x in B holds
cos . x <> 0 ) implies sec is_even_on B )
assume A1: for x being real number st x in B holds
cos . x <> 0 ; ::_thesis: sec is_even_on B
B c= dom sec
proof
let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in B or x in dom sec )
assume A2: x in B ; ::_thesis: x in dom sec
then cos . x <> 0 by A1;
then not cos . x in {0} by TARSKI:def_1;
then not x in cos " {0} by FUNCT_1:def_7;
then x in (dom cos) \ (cos " {0}) by A2, SIN_COS:24, XBOOLE_0:def_5;
hence x in dom sec by RFUNCT_1:def_2; ::_thesis: verum
end;
hence sec is_even_on B by Th81; ::_thesis: verum
end;
theorem Th83: :: FUNCT_8:83
for B being symmetrical Subset of REAL st B c= dom cosec holds
cosec is_odd_on B
proof
let B be symmetrical Subset of REAL; ::_thesis: ( B c= dom cosec implies cosec is_odd_on B )
assume A1: B c= dom cosec ; ::_thesis: cosec is_odd_on B
then A2: dom (cosec | B) = B by RELAT_1:62;
A3: for x being Real st x in B holds
cosec . (- x) = - (cosec . x)
proof
let x be Real; ::_thesis: ( x in B implies cosec . (- x) = - (cosec . x) )
assume A4: x in B ; ::_thesis: cosec . (- x) = - (cosec . x)
then - x in B by Def1;
then cosec . (- x) = (sin . (- x)) " by A1, RFUNCT_1:def_2
.= (- (sin . x)) " by SIN_COS:30
.= - ((sin . x) ") by XCMPLX_1:222
.= - (cosec . x) by A1, A4, RFUNCT_1:def_2 ;
hence cosec . (- x) = - (cosec . x) ; ::_thesis: verum
end;
for x being Real st x in dom (cosec | B) & - x in dom (cosec | B) holds
(cosec | B) . (- x) = - ((cosec | B) . x)
proof
let x be Real; ::_thesis: ( x in dom (cosec | B) & - x in dom (cosec | B) implies (cosec | B) . (- x) = - ((cosec | B) . x) )
assume that
A5: x in dom (cosec | B) and
A6: - x in dom (cosec | B) ; ::_thesis: (cosec | B) . (- x) = - ((cosec | B) . x)
(cosec | B) . (- x) = (cosec | B) /. (- x) by A6, PARTFUN1:def_6
.= cosec /. (- x) by A1, A2, A6, PARTFUN2:17
.= cosec . (- x) by A1, A2, A6, PARTFUN1:def_6
.= - (cosec . x) by A3, A5
.= - (cosec /. x) by A1, A2, A5, PARTFUN1:def_6
.= - ((cosec | B) /. x) by A1, A2, A5, PARTFUN2:17
.= - ((cosec | B) . x) by A5, PARTFUN1:def_6 ;
hence (cosec | B) . (- x) = - ((cosec | B) . x) ; ::_thesis: verum
end;
then ( cosec | B is with_symmetrical_domain & cosec | B is quasi_odd ) by A2, Def2, Def6;
hence cosec is_odd_on B by A1, Def8; ::_thesis: verum
end;
theorem :: FUNCT_8:84
for B being symmetrical Subset of REAL st ( for x being real number st x in B holds
sin . x <> 0 ) holds
cosec is_odd_on B
proof
let B be symmetrical Subset of REAL; ::_thesis: ( ( for x being real number st x in B holds
sin . x <> 0 ) implies cosec is_odd_on B )
assume A1: for x being real number st x in B holds
sin . x <> 0 ; ::_thesis: cosec is_odd_on B
B c= dom cosec
proof
let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in B or x in dom cosec )
assume A2: x in B ; ::_thesis: x in dom cosec
then sin . x <> 0 by A1;
then not sin . x in {0} by TARSKI:def_1;
then not x in sin " {0} by FUNCT_1:def_7;
then x in (dom sin) \ (sin " {0}) by A2, SIN_COS:24, XBOOLE_0:def_5;
hence x in dom cosec by RFUNCT_1:def_2; ::_thesis: verum
end;
hence cosec is_odd_on B by Th83; ::_thesis: verum
end;