:: FUNCSDOM semantic presentation
begin
definition
let A be set ;
let B be non empty set ;
let F be BinOp of (Funcs (A,B));
let f, g be Element of Funcs (A,B);
:: original: .
redefine funcF . (f,g) -> Element of Funcs (A,B);
coherence
F . (f,g) is Element of Funcs (A,B)
proof
reconsider f = f, g = g as Element of Funcs (A,B) ;
F . (f,g) is Element of Funcs (A,B) ;
hence F . (f,g) is Element of Funcs (A,B) ; ::_thesis: verum
end;
end;
definition
let A, B, C, D be non empty set ;
let F be Function of [:C,D:],(Funcs (A,B));
let cd be Element of [:C,D:];
:: original: .
redefine funcF . cd -> Element of Funcs (A,B);
coherence
F . cd is Element of Funcs (A,B)
proof
F . cd is Element of Funcs (A,B) ;
hence F . cd is Element of Funcs (A,B) ; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let Z be set ;
let F be BinOp of X;
let f, g be Function of Z,X;
:: original: .:
redefine funcF .: (f,g) -> Element of Funcs (Z,X);
coherence
F .: (f,g) is Element of Funcs (Z,X)
proof
F .: (f,g) in Funcs (Z,X) by FUNCT_2:8;
hence F .: (f,g) is Element of Funcs (Z,X) ; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let Z be set ;
let F be BinOp of X;
let a be Element of X;
let f be Function of Z,X;
:: original: [;]
redefine funcF [;] (a,f) -> Element of Funcs (Z,X);
coherence
F [;] (a,f) is Element of Funcs (Z,X)
proof
F [;] (a,f) in Funcs (Z,X) by FUNCT_2:8;
hence F [;] (a,f) is Element of Funcs (Z,X) ; ::_thesis: verum
end;
end;
definition
let A be set ;
func RealFuncAdd A -> BinOp of (Funcs (A,REAL)) means :Def1: :: FUNCSDOM:def 1
for f, g being Element of Funcs (A,REAL) holds it . (f,g) = addreal .: (f,g);
existence
ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = addreal .: (f,g)
proof
deffunc H1( Element of Funcs (A,REAL), Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = addreal .: ($1,$2);
consider F being BinOp of (Funcs (A,REAL)) such that
A1: for x, y being Element of Funcs (A,REAL) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take F ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds F . (f,g) = addreal .: (f,g)
let f, g be Element of Funcs (A,REAL); ::_thesis: F . (f,g) = addreal .: (f,g)
thus F . (f,g) = addreal .: (f,g) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = addreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = addreal .: (f,g) ) holds
b1 = b2
proof
let it1, it2 be BinOp of (Funcs (A,REAL)); ::_thesis: ( ( for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = addreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = addreal .: (f,g) ) implies it1 = it2 )
assume that
A2: for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = addreal .: (f,g) and
A3: for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = addreal .: (f,g) ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,REAL)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of Funcs (A,REAL); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = addreal .: (f,g) by A2
.= it2 . (f,g) by A3 ; ::_thesis: verum
end;
hence it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines RealFuncAdd FUNCSDOM:def_1_:_
for A being set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = RealFuncAdd A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = addreal .: (f,g) );
definition
let A be set ;
func RealFuncMult A -> BinOp of (Funcs (A,REAL)) means :Def2: :: FUNCSDOM:def 2
for f, g being Element of Funcs (A,REAL) holds it . (f,g) = multreal .: (f,g);
existence
ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = multreal .: (f,g)
proof
deffunc H1( Element of Funcs (A,REAL), Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = multreal .: ($1,$2);
consider F being BinOp of (Funcs (A,REAL)) such that
A1: for x, y being Element of Funcs (A,REAL) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take F ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds F . (f,g) = multreal .: (f,g)
let f, g be Element of Funcs (A,REAL); ::_thesis: F . (f,g) = multreal .: (f,g)
thus F . (f,g) = multreal .: (f,g) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = multreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = multreal .: (f,g) ) holds
b1 = b2
proof
let it1, it2 be BinOp of (Funcs (A,REAL)); ::_thesis: ( ( for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = multreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = multreal .: (f,g) ) implies it1 = it2 )
assume that
A2: for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = multreal .: (f,g) and
A3: for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = multreal .: (f,g) ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,REAL)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of Funcs (A,REAL); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = multreal .: (f,g) by A2
.= it2 . (f,g) by A3 ; ::_thesis: verum
end;
hence it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines RealFuncMult FUNCSDOM:def_2_:_
for A being set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = RealFuncMult A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = multreal .: (f,g) );
definition
let A be set ;
func RealFuncExtMult A -> Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) means :Def3: :: FUNCSDOM:def 3
for a being Real
for f being Element of Funcs (A,REAL) holds it . (a,f) = multreal [;] (a,f);
existence
ex b1 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st
for a being Real
for f being Element of Funcs (A,REAL) holds b1 . (a,f) = multreal [;] (a,f)
proof
deffunc H1( Element of REAL , Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = multreal [;] ($1,$2);
consider F being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) such that
A1: for a being Element of REAL
for f being Element of Funcs (A,REAL) holds F . (a,f) = H1(a,f) from BINOP_1:sch_4();
take F ; ::_thesis: for a being Real
for f being Element of Funcs (A,REAL) holds F . (a,f) = multreal [;] (a,f)
let a be Real; ::_thesis: for f being Element of Funcs (A,REAL) holds F . (a,f) = multreal [;] (a,f)
let f be Element of Funcs (A,REAL); ::_thesis: F . (a,f) = multreal [;] (a,f)
thus F . (a,f) = multreal [;] (a,f) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st ( for a being Real
for f being Element of Funcs (A,REAL) holds b1 . (a,f) = multreal [;] (a,f) ) & ( for a being Real
for f being Element of Funcs (A,REAL) holds b2 . (a,f) = multreal [;] (a,f) ) holds
b1 = b2
proof
let it1, it2 be Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)); ::_thesis: ( ( for a being Real
for f being Element of Funcs (A,REAL) holds it1 . (a,f) = multreal [;] (a,f) ) & ( for a being Real
for f being Element of Funcs (A,REAL) holds it2 . (a,f) = multreal [;] (a,f) ) implies it1 = it2 )
assume that
A2: for a being Real
for f being Element of Funcs (A,REAL) holds it1 . (a,f) = multreal [;] (a,f) and
A3: for a being Real
for f being Element of Funcs (A,REAL) holds it2 . (a,f) = multreal [;] (a,f) ; ::_thesis: it1 = it2
now__::_thesis:_for_a_being_Real
for_f_being_Element_of_Funcs_(A,REAL)_holds_it1_._(a,f)_=_it2_._(a,f)
let a be Real; ::_thesis: for f being Element of Funcs (A,REAL) holds it1 . (a,f) = it2 . (a,f)
let f be Element of Funcs (A,REAL); ::_thesis: it1 . (a,f) = it2 . (a,f)
thus it1 . (a,f) = multreal [;] (a,f) by A2
.= it2 . (a,f) by A3 ; ::_thesis: verum
end;
hence it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines RealFuncExtMult FUNCSDOM:def_3_:_
for A being set
for b2 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) holds
( b2 = RealFuncExtMult A iff for a being Real
for f being Element of Funcs (A,REAL) holds b2 . (a,f) = multreal [;] (a,f) );
definition
let A be set ;
func RealFuncZero A -> Element of Funcs (A,REAL) equals :: FUNCSDOM:def 4
A --> 0;
coherence
A --> 0 is Element of Funcs (A,REAL)
proof
A --> 0 is Function of A,REAL by FUNCOP_1:45;
hence A --> 0 is Element of Funcs (A,REAL) by FUNCT_2:8; ::_thesis: verum
end;
end;
:: deftheorem defines RealFuncZero FUNCSDOM:def_4_:_
for A being set holds RealFuncZero A = A --> 0;
definition
let A be set ;
func RealFuncUnit A -> Element of Funcs (A,REAL) equals :: FUNCSDOM:def 5
A --> 1;
coherence
A --> 1 is Element of Funcs (A,REAL)
proof
A --> 1 is Function of A,REAL by FUNCOP_1:45;
hence A --> 1 is Element of Funcs (A,REAL) by FUNCT_2:8; ::_thesis: verum
end;
end;
:: deftheorem defines RealFuncUnit FUNCSDOM:def_5_:_
for A being set holds RealFuncUnit A = A --> 1;
Lm1: for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
proof
let A, B be non empty set ; ::_thesis: for x being Element of A
for f being Function of A,B holds x in dom f
let x be Element of A; ::_thesis: for f being Function of A,B holds x in dom f
let f be Function of A,B; ::_thesis: x in dom f
x in A ;
hence x in dom f by FUNCT_2:def_1; ::_thesis: verum
end;
theorem Th1: :: FUNCSDOM:1
for A being non empty set
for h, f, g being Element of Funcs (A,REAL) holds
( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
proof
let A be non empty set ; ::_thesis: for h, f, g being Element of Funcs (A,REAL) holds
( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
let h, f, g be Element of Funcs (A,REAL); ::_thesis: ( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
A1: now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_+_(g_._x)_)_implies_h_=_(RealFuncAdd_A)_._(f,g)_)
assume A2: for x being Element of A holds h . x = (f . x) + (g . x) ; ::_thesis: h = (RealFuncAdd A) . (f,g)
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(f,g))_._x_=_h_._x
let x be Element of A; ::_thesis: ((RealFuncAdd A) . (f,g)) . x = h . x
A3: x in dom (addreal .: (f,g)) by Lm1;
thus ((RealFuncAdd A) . (f,g)) . x = (addreal .: (f,g)) . x by Def1
.= addreal . ((f . x),(g . x)) by A3, FUNCOP_1:22
.= (f . x) + (g . x) by BINOP_2:def_9
.= h . x by A2 ; ::_thesis: verum
end;
hence h = (RealFuncAdd A) . (f,g) by FUNCT_2:63; ::_thesis: verum
end;
now__::_thesis:_(_h_=_(RealFuncAdd_A)_._(f,g)_implies_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_+_(g_._x)_)
assume A4: h = (RealFuncAdd A) . (f,g) ; ::_thesis: for x being Element of A holds h . x = (f . x) + (g . x)
let x be Element of A; ::_thesis: h . x = (f . x) + (g . x)
A5: x in dom (addreal .: (f,g)) by Lm1;
thus h . x = (addreal .: (f,g)) . x by A4, Def1
.= addreal . ((f . x),(g . x)) by A5, FUNCOP_1:22
.= (f . x) + (g . x) by BINOP_2:def_9 ; ::_thesis: verum
end;
hence ( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) ) by A1; ::_thesis: verum
end;
theorem Th2: :: FUNCSDOM:2
for A being non empty set
for h, f, g being Element of Funcs (A,REAL) holds
( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
proof
let A be non empty set ; ::_thesis: for h, f, g being Element of Funcs (A,REAL) holds
( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
let h, f, g be Element of Funcs (A,REAL); ::_thesis: ( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
A1: now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_*_(g_._x)_)_implies_h_=_(RealFuncMult_A)_._(f,g)_)
assume A2: for x being Element of A holds h . x = (f . x) * (g . x) ; ::_thesis: h = (RealFuncMult A) . (f,g)
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncMult_A)_._(f,g))_._x_=_h_._x
let x be Element of A; ::_thesis: ((RealFuncMult A) . (f,g)) . x = h . x
A3: x in dom (multreal .: (f,g)) by Lm1;
thus ((RealFuncMult A) . (f,g)) . x = (multreal .: (f,g)) . x by Def2
.= multreal . ((f . x),(g . x)) by A3, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def_11
.= h . x by A2 ; ::_thesis: verum
end;
hence h = (RealFuncMult A) . (f,g) by FUNCT_2:63; ::_thesis: verum
end;
now__::_thesis:_(_h_=_(RealFuncMult_A)_._(f,g)_implies_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_*_(g_._x)_)
assume A4: h = (RealFuncMult A) . (f,g) ; ::_thesis: for x being Element of A holds h . x = (f . x) * (g . x)
let x be Element of A; ::_thesis: h . x = (f . x) * (g . x)
A5: x in dom (multreal .: (f,g)) by Lm1;
thus h . x = (multreal .: (f,g)) . x by A4, Def2
.= multreal . ((f . x),(g . x)) by A5, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def_11 ; ::_thesis: verum
end;
hence ( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) by A1; ::_thesis: verum
end;
theorem :: FUNCSDOM:3
for A being non empty set holds RealFuncZero A <> RealFuncUnit A
proof
let A be non empty set ; ::_thesis: RealFuncZero A <> RealFuncUnit A
set a = the Element of A;
(RealFuncZero A) . the Element of A = 0 by FUNCOP_1:7;
hence RealFuncZero A <> RealFuncUnit A by FUNCOP_1:7; ::_thesis: verum
end;
theorem Th4: :: FUNCSDOM:4
for A being non empty set
for h, f being Element of Funcs (A,REAL)
for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
proof
let A be non empty set ; ::_thesis: for h, f being Element of Funcs (A,REAL)
for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let h, f be Element of Funcs (A,REAL); ::_thesis: for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let a be Real; ::_thesis: ( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
thus ( h = (RealFuncExtMult A) . [a,f] implies for x being Element of A holds h . x = a * (f . x) ) ::_thesis: ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . [a,f] )
proof
assume A1: h = (RealFuncExtMult A) . [a,f] ; ::_thesis: for x being Element of A holds h . x = a * (f . x)
let x be Element of A; ::_thesis: h . x = a * (f . x)
h = (RealFuncExtMult A) . (a,f) by A1;
hence h . x = (multreal [;] (a,f)) . x by Def3
.= multreal . (a,(f . x)) by FUNCOP_1:53
.= a * (f . x) by BINOP_2:def_11 ;
::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_a_*_(f_._x)_)_implies_h_=_(RealFuncExtMult_A)_._(a,f)_)
assume A2: for x being Element of A holds h . x = a * (f . x) ; ::_thesis: h = (RealFuncExtMult A) . (a,f)
for x being Element of A holds h . x = ((RealFuncExtMult A) . [a,f]) . x
proof
let x be Element of A; ::_thesis: h . x = ((RealFuncExtMult A) . [a,f]) . x
A3: multreal [;] (a,f) = (RealFuncExtMult A) . (a,f) by Def3;
thus h . x = a * (f . x) by A2
.= multreal . (a,(f . x)) by BINOP_2:def_11
.= ((RealFuncExtMult A) . [a,f]) . x by A3, FUNCOP_1:53 ; ::_thesis: verum
end;
hence h = (RealFuncExtMult A) . (a,f) by FUNCT_2:63; ::_thesis: verum
end;
hence ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . [a,f] ) ; ::_thesis: verum
end;
theorem Th5: :: FUNCSDOM:5
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f)
proof
let A be set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f)
let f, g be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f)
thus (RealFuncAdd A) . (f,g) = addreal .: (f,g) by Def1
.= addreal .: (g,f) by FUNCOP_1:65
.= (RealFuncAdd A) . (g,f) by Def1 ; ::_thesis: verum
end;
theorem Th6: :: FUNCSDOM:6
for A being set
for f, g, h being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h)
proof
let A be set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h)
let f, g, h be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h)
thus (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (f,(addreal .: (g,h))) by Def1
.= addreal .: (f,(addreal .: (g,h))) by Def1
.= addreal .: ((addreal .: (f,g)),h) by FUNCOP_1:61
.= (RealFuncAdd A) . ((addreal .: (f,g)),h) by Def1
.= (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h) by Def1 ; ::_thesis: verum
end;
theorem Th7: :: FUNCSDOM:7
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f)
proof
let A be set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f)
let f, g be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f)
thus (RealFuncMult A) . (f,g) = multreal .: (f,g) by Def2
.= multreal .: (g,f) by FUNCOP_1:65
.= (RealFuncMult A) . (g,f) by Def2 ; ::_thesis: verum
end;
theorem Th8: :: FUNCSDOM:8
for A being set
for f, g, h being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h)
proof
let A be set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h)
let f, g, h be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h)
thus (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (f,(multreal .: (g,h))) by Def2
.= multreal .: (f,(multreal .: (g,h))) by Def2
.= multreal .: ((multreal .: (f,g)),h) by FUNCOP_1:61
.= (RealFuncMult A) . ((multreal .: (f,g)),h) by Def2
.= (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h) by Def2 ; ::_thesis: verum
end;
theorem Th9: :: FUNCSDOM:9
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f
proof
let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f
let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . ((RealFuncUnit A),f) = f
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: (RealFuncMult A) . ((RealFuncUnit A),f) = f
then A1: f = {} ;
thus (RealFuncMult A) . ((RealFuncUnit A),f) = multreal .: ((RealFuncUnit A),f) by Def2
.= f by A1 ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncMult A) . ((RealFuncUnit A),f) = f
then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncMult_A)_._((RealFuncUnit_A),f))_._x_=_f_._x
let x be Element of A; ::_thesis: ((RealFuncMult A) . ((RealFuncUnit A),f)) . x = f . x
thus ((RealFuncMult A) . ((RealFuncUnit A),f)) . x = ((RealFuncUnit A) . x) * (f . x) by Th2
.= 1 * (f . x) by FUNCOP_1:7
.= f . x ; ::_thesis: verum
end;
hence (RealFuncMult A) . ((RealFuncUnit A),f) = f by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
theorem Th10: :: FUNCSDOM:10
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f
proof
let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f
let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . ((RealFuncZero A),f) = f
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: (RealFuncAdd A) . ((RealFuncZero A),f) = f
then A1: f = {} ;
thus (RealFuncAdd A) . ((RealFuncZero A),f) = addreal .: ((RealFuncZero A),f) by Def1
.= f by A1 ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncAdd A) . ((RealFuncZero A),f) = f
then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._((RealFuncZero_A),f))_._x_=_f_._x
let x be Element of A; ::_thesis: ((RealFuncAdd A) . ((RealFuncZero A),f)) . x = f . x
thus ((RealFuncAdd A) . ((RealFuncZero A),f)) . x = ((RealFuncZero A) . x) + (f . x) by Th1
.= 0 + (f . x) by FUNCOP_1:7
.= f . x ; ::_thesis: verum
end;
hence (RealFuncAdd A) . ((RealFuncZero A),f) = f by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
theorem Th11: :: FUNCSDOM:11
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
proof
let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
percases ( A = {} or A <> {} ) ;
supposeA1: A = {} ; ::_thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = {}
.= RealFuncZero A by A1 ;
::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(f,((RealFuncExtMult_A)_._[(-_1),f])))_._x_=_(RealFuncZero_A)_._x
let x be Element of A; ::_thesis: ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f]))) . x = (RealFuncZero A) . x
set y = f . x;
thus ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f]))) . x = (f . x) + (((RealFuncExtMult A) . [(- 1),f]) . x) by Th1
.= (f . x) + ((- 1) * (f . x)) by Th4
.= (RealFuncZero A) . x by FUNCOP_1:7 ; ::_thesis: verum
end;
hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
theorem Th12: :: FUNCSDOM:12
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (1,f) = f
proof
let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (1,f) = f
let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncExtMult A) . (1,f) = f
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: (RealFuncExtMult A) . (1,f) = f
then A1: f = {} ;
thus (RealFuncExtMult A) . (1,f) = multreal [;] (1,f) by Def3
.= f by A1 ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncExtMult A) . (1,f) = f
then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;
reconsider g = (RealFuncExtMult A) . (1,f) as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_g_._x_=_f_._x
let x be Element of A; ::_thesis: g . x = f . x
thus g . x = 1 * (f . x) by Th4
.= f . x ; ::_thesis: verum
end;
hence (RealFuncExtMult A) . (1,f) = f by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
theorem Th13: :: FUNCSDOM:13
for a, b being Real
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
proof
let a, b be Real; ::_thesis: for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
percases ( A = {} or A <> {} ) ;
supposeA1: A = {} ; ::_thesis: (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
(RealFuncExtMult A) . (b,f) = multreal [;] (b,f) by Def3;
hence (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = multreal [;] (a,(multreal [;] (b,f))) by Def3
.= multreal [;] ((a * b),f) by A1
.= (RealFuncExtMult A) . ((a * b),f) by Def3 ;
::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncExtMult_A)_._[a,((RealFuncExtMult_A)_._[b,f])])_._x_=_((RealFuncExtMult_A)_._[(a_*_b),f])_._x
let x be Element of A; ::_thesis: ((RealFuncExtMult A) . [a,((RealFuncExtMult A) . [b,f])]) . x = ((RealFuncExtMult A) . [(a * b),f]) . x
thus ((RealFuncExtMult A) . [a,((RealFuncExtMult A) . [b,f])]) . x = a * (((RealFuncExtMult A) . [b,f]) . x) by Th4
.= a * (b * (f . x)) by Th4
.= (a * b) * (f . x)
.= ((RealFuncExtMult A) . [(a * b),f]) . x by Th4 ; ::_thesis: verum
end;
hence (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f) by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
theorem Th14: :: FUNCSDOM:14
for a, b being Real
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
proof
let a, b be Real; ::_thesis: for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
percases ( A = {} or A <> {} ) ;
supposeA1: A = {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = {}
.= multreal [;] ((a + b),f) by A1
.= (RealFuncExtMult A) . ((a + b),f) by Def3 ;
::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
then reconsider A = A as non empty set ;
reconsider f = f as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(((RealFuncExtMult_A)_._[a,f]),((RealFuncExtMult_A)_._[b,f])))_._x_=_((RealFuncExtMult_A)_._[(a_+_b),f])_._x
let x be Element of A; ::_thesis: ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,f]))) . x = ((RealFuncExtMult A) . [(a + b),f]) . x
thus ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,f]))) . x = (((RealFuncExtMult A) . [a,f]) . x) + (((RealFuncExtMult A) . [b,f]) . x) by Th1
.= (a * (f . x)) + (((RealFuncExtMult A) . [b,f]) . x) by Th4
.= (a * (f . x)) + (b * (f . x)) by Th4
.= (a + b) * (f . x)
.= ((RealFuncExtMult A) . [(a + b),f]) . x by Th4 ; ::_thesis: verum
end;
hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f) by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
Lm2: for a being Real
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
proof
let a be Real; ::_thesis: for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
let A be set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
let f, g be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
percases ( A = {} or A <> {} ) ;
supposeA1: A = {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = {}
.= multreal [;] (a,((RealFuncAdd A) . (f,g))) by A1
.= (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) by Def3 ;
::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
then reconsider A = A as non empty set ;
reconsider f = f, g = g as Element of Funcs (A,REAL) ;
now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(((RealFuncExtMult_A)_._[a,f]),((RealFuncExtMult_A)_._[a,g])))_._x_=_((RealFuncExtMult_A)_._[a,((RealFuncAdd_A)_._(f,g))])_._x
let x be Element of A; ::_thesis: ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [a,g]))) . x = ((RealFuncExtMult A) . [a,((RealFuncAdd A) . (f,g))]) . x
thus ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [a,g]))) . x = (((RealFuncExtMult A) . [a,f]) . x) + (((RealFuncExtMult A) . [a,g]) . x) by Th1
.= (a * (f . x)) + (((RealFuncExtMult A) . [a,g]) . x) by Th4
.= (a * (f . x)) + (a * (g . x)) by Th4
.= a * ((f . x) + (g . x))
.= a * (((RealFuncAdd A) . (f,g)) . x) by Th1
.= ((RealFuncExtMult A) . [a,((RealFuncAdd A) . (f,g))]) . x by Th4 ; ::_thesis: verum
end;
hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) by FUNCT_2:63; ::_thesis: verum
end;
end;
end;
theorem Th15: :: FUNCSDOM:15
for A being set
for f, g, h being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h)))
proof
let A be set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h)))
let f, g, h be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h)))
A1: multreal .: (f,(addreal .: (g,h))) = addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))
proof
let a be Element of A; :: according to FUNCT_2:def_8 ::_thesis: (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a
then f = {} ;
hence (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a
then reconsider B = A as non empty set ;
reconsider ff = f, gg = g, hh = h as Element of Funcs (B,REAL) ;
reconsider b = a as Element of B ;
thus (multreal .: (f,(addreal .: (g,h)))) . a = multreal . ((f . b),((addreal .: (g,h)) . b)) by FUNCOP_1:37
.= multreal . ((f . b),(addreal . ((g . b),(h . b)))) by FUNCOP_1:37
.= (ff . b) * (addreal . ((gg . b),(hh . b))) by BINOP_2:def_11
.= (ff . b) * ((gg . b) + (hh . b)) by BINOP_2:def_9
.= ((ff . b) * (gg . b)) + ((ff . b) * (hh . b))
.= ((ff . b) * (gg . b)) + (multreal . ((ff . b),(hh . b))) by BINOP_2:def_11
.= (multreal . ((ff . b),(gg . b))) + (multreal . ((ff . b),(hh . b))) by BINOP_2:def_11
.= addreal . ((multreal . ((f . a),(g . a))),(multreal . ((f . a),(h . a)))) by BINOP_2:def_9
.= addreal . ((multreal . ((f . a),(g . a))),((multreal .: (ff,h)) . a)) by FUNCOP_1:37
.= addreal . (((multreal .: (ff,g)) . a),((multreal .: (ff,h)) . a)) by FUNCOP_1:37
.= (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a by FUNCOP_1:37 ; ::_thesis: verum
end;
end;
end;
thus (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncMult A) . (f,(addreal .: (g,h))) by Def1
.= multreal .: (f,(addreal .: (g,h))) by Def2
.= addreal .: ((multreal .: (f,g)),(multreal .: (f,h))) by A1
.= (RealFuncAdd A) . ((multreal .: (f,g)),(multreal .: (f,h))) by Def1
.= (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),(multreal .: (f,h))) by Def2
.= (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h))) by Def2 ; ::_thesis: verum
end;
theorem Th16: :: FUNCSDOM:16
for A being set
for f, g, h being Element of Funcs (A,REAL)
for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
proof
let A be set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL)
for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
let f, g, h be Element of Funcs (A,REAL); ::_thesis: for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
let a be Real; ::_thesis: (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
thus (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncMult A) . ((multreal [;] (a,f)),g) by Def3
.= multreal .: ((multreal [;] (a,f)),g) by Def2
.= multreal [;] (a,(multreal .: (f,g))) by FUNCOP_1:85
.= (RealFuncExtMult A) . (a,(multreal .: (f,g))) by Def3
.= (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g))) by Def2 ; ::_thesis: verum
end;
theorem Th17: :: FUNCSDOM:17
for x1 being set
for A being non empty set ex f, g being Element of Funcs (A,REAL) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) )
proof
let x1 be set ; ::_thesis: for A being non empty set ex f, g being Element of Funcs (A,REAL) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) )
let A be non empty set ; ::_thesis: ex f, g being Element of Funcs (A,REAL) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) )
deffunc H1( set ) -> Element of NAT = 1;
deffunc H2( set ) -> Element of NAT = 0 ;
defpred S1[ set ] means $1 = x1;
A1: for z being set st z in A holds
( ( S1[z] implies H1(z) in REAL ) & ( not S1[z] implies H2(z) in REAL ) ) ;
consider f being Function of A,REAL such that
A2: for z being set st z in A holds
( ( S1[z] implies f . z = H1(z) ) & ( not S1[z] implies f . z = H2(z) ) ) from FUNCT_2:sch_5(A1);
A3: for z being set st z in A holds
( ( S1[z] implies H2(z) in REAL ) & ( not S1[z] implies H1(z) in REAL ) ) ;
consider g being Function of A,REAL such that
A4: for z being set st z in A holds
( ( S1[z] implies g . z = H2(z) ) & ( not S1[z] implies g . z = H1(z) ) ) from FUNCT_2:sch_5(A3);
reconsider f = f, g = g as Element of Funcs (A,REAL) by FUNCT_2:8;
take f ; ::_thesis: ex g being Element of Funcs (A,REAL) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) )
take g ; ::_thesis: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) )
thus ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) by A2, A4; ::_thesis: verum
end;
theorem Th18: :: FUNCSDOM:18
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,REAL) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
proof
let x1, x2 be set ; ::_thesis: for A being non empty set
for f, g being Element of Funcs (A,REAL) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
let f, g be Element of Funcs (A,REAL); ::_thesis: ( x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) implies for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) )
assume that
A1: x1 in A and
A2: x2 in A and
A3: x1 <> x2 and
A4: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) ; ::_thesis: for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
A5: ( f . x2 = 0 & g . x2 = 1 ) by A2, A3, A4;
A6: ( f . x1 = 1 & g . x1 = 0 ) by A1, A4;
let a, b be Real; ::_thesis: ( (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A implies ( a = 0 & b = 0 ) )
reconsider x1 = x1, x2 = x2 as Element of A by A1, A2;
assume A7: (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A ; ::_thesis: ( a = 0 & b = 0 )
then A8: 0 = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2 by FUNCOP_1:7
.= (((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2) by Th1
.= (a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2) by Th4
.= 0 + (b * 1) by A5, Th4
.= b ;
0 = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1 by A7, FUNCOP_1:7
.= (((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1) by Th1
.= (a * (f . x1)) + (((RealFuncExtMult A) . [b,g]) . x1) by Th4
.= a + (b * 0) by A6, Th4
.= a ;
hence ( a = 0 & b = 0 ) by A8; ::_thesis: verum
end;
theorem :: FUNCSDOM:19
for x1, x2 being set
for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
proof
let x1, x2 be set ; ::_thesis: for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
let A be non empty set ; ::_thesis: ( x1 in A & x2 in A & x1 <> x2 implies ex f, g being Element of Funcs (A,REAL) st
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) )
assume A1: ( x1 in A & x2 in A & x1 <> x2 ) ; ::_thesis: ex f, g being Element of Funcs (A,REAL) st
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
consider f, g being Element of Funcs (A,REAL) such that
A2: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) by Th17;
take f ; ::_thesis: ex g being Element of Funcs (A,REAL) st
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
take g ; ::_thesis: for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
let a, b be Real; ::_thesis: ( (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A implies ( a = 0 & b = 0 ) )
assume (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A ; ::_thesis: ( a = 0 & b = 0 )
hence ( a = 0 & b = 0 ) by A1, A2, Th18; ::_thesis: verum
end;
theorem Th20: :: FUNCSDOM:20
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,REAL) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
proof
let x1, x2 be set ; ::_thesis: for A being non empty set
for f, g being Element of Funcs (A,REAL) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
let f, g be Element of Funcs (A,REAL); ::_thesis: ( A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) implies for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) )
assume that
A1: A = {x1,x2} and
A2: x1 <> x2 and
A3: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) ; ::_thesis: for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
x2 in A by A1, TARSKI:def_2;
then A4: ( f . x2 = 0 & g . x2 = 1 ) by A2, A3;
x1 in A by A1, TARSKI:def_2;
then A5: ( f . x1 = 1 & g . x1 = 0 ) by A3;
let h be Element of Funcs (A,REAL); ::_thesis: ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
reconsider x1 = x1, x2 = x2 as Element of A by A1, TARSKI:def_2;
take a = h . x1; ::_thesis: ex b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
take b = h . x2; ::_thesis: h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
now__::_thesis:_for_x_being_Element_of_A_holds_h_._x_=_((RealFuncAdd_A)_._(((RealFuncExtMult_A)_._[a,f]),((RealFuncExtMult_A)_._[b,g])))_._x
let x be Element of A; ::_thesis: h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x
A6: ( x = x1 or x = x2 ) by A1, TARSKI:def_2;
A7: ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2 = (((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2) by Th1
.= (a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2) by Th4
.= 0 + (b * 1) by A4, Th4
.= h . x2 ;
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1 = (((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1) by Th1
.= (a * (f . x1)) + (((RealFuncExtMult A) . [b,g]) . x1) by Th4
.= a + (b * 0) by A5, Th4
.= h . x1 ;
hence h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x by A6, A7; ::_thesis: verum
end;
hence h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) by FUNCT_2:63; ::_thesis: verum
end;
theorem :: FUNCSDOM:21
for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
proof
let x1, x2 be set ; ::_thesis: for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
let A be non empty set ; ::_thesis: ( A = {x1,x2} & x1 <> x2 implies ex f, g being Element of Funcs (A,REAL) st
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) )
assume A1: ( A = {x1,x2} & x1 <> x2 ) ; ::_thesis: ex f, g being Element of Funcs (A,REAL) st
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
consider f, g being Element of Funcs (A,REAL) such that
A2: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) by Th17;
take f ; ::_thesis: ex g being Element of Funcs (A,REAL) st
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
take g ; ::_thesis: for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
let h be Element of Funcs (A,REAL); ::_thesis: ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
thus ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) by A1, A2, Th20; ::_thesis: verum
end;
theorem Th22: :: FUNCSDOM:22
for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
proof
let x1, x2 be set ; ::_thesis: for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
let A be non empty set ; ::_thesis: ( A = {x1,x2} & x1 <> x2 implies ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) ) )
assume that
A1: A = {x1,x2} and
A2: x1 <> x2 ; ::_thesis: ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
consider f, g being Element of Funcs (A,REAL) such that
A3: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) by Th17;
take f ; ::_thesis: ex g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
take g ; ::_thesis: ( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
( x1 in A & x2 in A ) by A1, TARSKI:def_2;
hence ( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) ) by A1, A2, A3, Th18, Th20; ::_thesis: verum
end;
definition
let A be set ;
func RealVectSpace A -> strict RealLinearSpace equals :: FUNCSDOM:def 6
RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);
coherence
RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace
proof
set S = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);
A1: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is add-associative
proof
let u, v, w be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
thus (u + v) + w = u + (v + w) by Th6; ::_thesis: verum
end;
A2: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is right_complementable
proof
let u be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to ALGSTR_0:def_16 ::_thesis: u is right_complementable
reconsider u9 = u as Element of Funcs (A,REAL) ;
reconsider w = (RealFuncExtMult A) . [(- 1),u9] as VECTOR of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) ;
take w ; :: according to ALGSTR_0:def_11 ::_thesis: u + w = 0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)
thus u + w = 0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) by Th11; ::_thesis: verum
end;
A3: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is vector-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital )
proof
thus for a being real number
for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real by XREAL_0:def_1;
for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) by Lm2;
hence for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
thus for a, b being real number
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) by Th14;
hence for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
thus for a, b being real number
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) by Th13;
hence for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
let v be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
thus 1 * v = v by Th12; ::_thesis: verum
end;
A4: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is right_zeroed
proof
let u be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_4 ::_thesis: u + (0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)) = u
reconsider u9 = u as Element of Funcs (A,REAL) ;
thus u + (0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)) = (RealFuncAdd A) . ((RealFuncZero A),u9) by Th5
.= u by Th10 ; ::_thesis: verum
end;
RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is Abelian
proof
let u, v be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_2 ::_thesis: u + v = v + u
thus u + v = v + u by Th5; ::_thesis: verum
end;
hence RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace by A1, A4, A2, A3; ::_thesis: verum
end;
end;
:: deftheorem defines RealVectSpace FUNCSDOM:def_6_:_
for A being set holds RealVectSpace A = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);
theorem :: FUNCSDOM:23
ex V being strict RealLinearSpace ex u, v being Element of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
proof
set A = {0,1};
take V = RealVectSpace {0,1}; ::_thesis: ex u, v being Element of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
consider f, g being Element of Funcs ({0,1},REAL) such that
A1: for a, b being Real st (RealFuncAdd {0,1}) . (((RealFuncExtMult {0,1}) . [a,f]),((RealFuncExtMult {0,1}) . [b,g])) = RealFuncZero {0,1} holds
( a = 0 & b = 0 ) and
A2: for h being Element of Funcs ({0,1},REAL) ex a, b being Real st h = (RealFuncAdd {0,1}) . (((RealFuncExtMult {0,1}) . [a,f]),((RealFuncExtMult {0,1}) . [b,g])) by Th22;
reconsider u = f, v = g as Element of V ;
take u ; ::_thesis: ex v being Element of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
take v ; ::_thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
thus for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) by A1; ::_thesis: for w being Element of V ex a, b being Real st w = (a * u) + (b * v)
thus for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ::_thesis: verum
proof
let w be Element of V; ::_thesis: ex a, b being Real st w = (a * u) + (b * v)
reconsider h = w as Element of Funcs ({0,1},REAL) ;
consider a, b being Real such that
A3: h = (RealFuncAdd {0,1}) . (((RealFuncExtMult {0,1}) . [a,f]),((RealFuncExtMult {0,1}) . [b,g])) by A2;
h = (a * u) + (b * v) by A3;
hence ex a, b being Real st w = (a * u) + (b * v) ; ::_thesis: verum
end;
end;
definition
let A be non empty set ;
func RRing A -> strict doubleLoopStr equals :: FUNCSDOM:def 7
doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);
correctness
coherence
doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict doubleLoopStr ;
;
end;
:: deftheorem defines RRing FUNCSDOM:def_7_:_
for A being non empty set holds RRing A = doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);
registration
let A be non empty set ;
cluster RRing A -> non empty strict ;
coherence
not RRing A is empty ;
end;
Lm3: now__::_thesis:_for_A_being_non_empty_set_
for_h,_a_being_Element_of_(RRing_A)_st_a_=_RealFuncUnit_A_holds_
(_h_*_a_=_h_&_a_*_h_=_h_)
let A be non empty set ; ::_thesis: for h, a being Element of (RRing A) st a = RealFuncUnit A holds
( h * a = h & a * h = h )
set FR = RRing A;
let h, a be Element of (RRing A); ::_thesis: ( a = RealFuncUnit A implies ( h * a = h & a * h = h ) )
reconsider g = h as Element of Funcs (A,REAL) ;
assume A1: a = RealFuncUnit A ; ::_thesis: ( h * a = h & a * h = h )
hence h * a = (RealFuncMult A) . ((RealFuncUnit A),g) by Th7
.= h by Th9 ;
::_thesis: a * h = h
thus a * h = h by A1, Th9; ::_thesis: verum
end;
registration
let A be non empty set ;
cluster RRing A -> strict unital ;
coherence
RRing A is unital
proof
reconsider e = RealFuncUnit A as Element of (RRing A) ;
take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (RRing A) holds
( b1 * e = b1 & e * b1 = b1 )
thus for b1 being Element of the carrier of (RRing A) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm3; ::_thesis: verum
end;
end;
theorem :: FUNCSDOM:24
for A being non empty set holds 1. (RRing A) = RealFuncUnit A ;
theorem Th25: :: FUNCSDOM:25
for A being non empty set
for x, y, z being Element of (RRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof
let A be non empty set ; ::_thesis: for x, y, z being Element of (RRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
let x, y, z be Element of (RRing A); ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
set IT = RRing A;
reconsider f = x as Element of Funcs (A,REAL) ;
thus x + y = y + x by Th5; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (x + y) + z = x + (y + z) by Th6; ::_thesis: ( x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x + (0. (RRing A)) = (RealFuncAdd A) . ((RealFuncZero A),f) by Th5
.= x by Th10 ; ::_thesis: ( ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus ex t being Element of (RRing A) st x + t = 0. (RRing A) ::_thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof
set h = (RealFuncExtMult A) . [(- 1),f];
reconsider t = (RealFuncExtMult A) . [(- 1),f] as Element of (RRing A) ;
take t ; ::_thesis: x + t = 0. (RRing A)
thus x + t = 0. (RRing A) by Th11; ::_thesis: verum
end;
thus x * y = y * x by Th7; ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (x * y) * z = x * (y * z) by Th8; ::_thesis: ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (1. (RRing A)) = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7
.= x by Th9 ; ::_thesis: ( (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
hence (1. (RRing A)) * x = x by Th7; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: (y + z) * x = (y * x) + (z * x)
hence (y + z) * x = (x * y) + (x * z) by Th7
.= (y * x) + (x * z) by Th7
.= (y * x) + (z * x) by Th7 ;
::_thesis: verum
end;
registration
cluster non empty trivial V52() 1 -element right_complementable strict associative commutative right-distributive right_unital Abelian add-associative right_zeroed for doubleLoopStr ;
existence
ex b1 being 1 -element doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is right_unital & b1 is right-distributive )
proof
take L = Trivial-doubleLoopStr ; ::_thesis: ( L is strict & L is Abelian & L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is strict ; ::_thesis: ( L is Abelian & L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is Abelian ::_thesis: ( L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to RLVECT_1:def_2 ::_thesis: for b1 being Element of the carrier of L holds x + b1 = b1 + x
thus for b1 being Element of the carrier of L holds x + b1 = b1 + x by STRUCT_0:def_10; ::_thesis: verum
end;
thus L is add-associative ::_thesis: ( L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to RLVECT_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of L holds (x + b1) + b2 = x + (b1 + b2)
thus for b1, b2 being Element of the carrier of L holds (x + b1) + b2 = x + (b1 + b2) by STRUCT_0:def_10; ::_thesis: verum
end;
thus L is right_zeroed ::_thesis: ( L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to RLVECT_1:def_4 ::_thesis: x + (0. L) = x
thus x + (0. L) = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus L is right_complementable ::_thesis: ( L is associative & L is commutative & L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
take x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. L
thus x + x = 0. L by STRUCT_0:def_10; ::_thesis: verum
end;
thus L is associative ::_thesis: ( L is commutative & L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to GROUP_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of L holds (x * b1) * b2 = x * (b1 * b2)
thus for b1, b2 being Element of the carrier of L holds (x * b1) * b2 = x * (b1 * b2) by STRUCT_0:def_10; ::_thesis: verum
end;
thus L is commutative ::_thesis: ( L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of L holds x * b1 = b1 * x
thus for b1 being Element of the carrier of L holds x * b1 = b1 * x by STRUCT_0:def_10; ::_thesis: verum
end;
thus L is right_unital ::_thesis: L is right-distributive
proof
let x be Element of L; :: according to VECTSP_1:def_4 ::_thesis: x * (1. L) = x
thus x * (1. L) = x by STRUCT_0:def_10; ::_thesis: verum
end;
let x be Element of L; :: according to VECTSP_1:def_2 ::_thesis: for b1, b2 being Element of the carrier of L holds x * (b1 + b2) = (x * b1) + (x * b2)
thus for b1, b2 being Element of the carrier of L holds x * (b1 + b2) = (x * b1) + (x * b2) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
definition
mode Ring is non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
end;
theorem :: FUNCSDOM:26
for A being non empty set holds RRing A is commutative Ring
proof
let A be non empty set ; ::_thesis: RRing A is commutative Ring
A1: RRing A is Abelian
proof
let x be Element of (RRing A); :: according to RLVECT_1:def_2 ::_thesis: for b1 being Element of the carrier of (RRing A) holds x + b1 = b1 + x
thus for b1 being Element of the carrier of (RRing A) holds x + b1 = b1 + x by Th25; ::_thesis: verum
end;
A2: RRing A is add-associative
proof
let x be Element of (RRing A); :: according to RLVECT_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of (RRing A) holds (x + b1) + b2 = x + (b1 + b2)
thus for b1, b2 being Element of the carrier of (RRing A) holds (x + b1) + b2 = x + (b1 + b2) by Th25; ::_thesis: verum
end;
A3: RRing A is right_complementable
proof
let x be Element of (RRing A); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
consider t being Element of (RRing A) such that
A4: x + t = 0. (RRing A) by Th25;
take t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (RRing A)
thus x + t = 0. (RRing A) by A4; ::_thesis: verum
end;
A5: RRing A is right_zeroed
proof
let x be Element of (RRing A); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (RRing A)) = x
thus x + (0. (RRing A)) = x by Th25; ::_thesis: verum
end;
A6: RRing A is distributive
proof
let x be Element of (RRing A); :: according to VECTSP_1:def_7 ::_thesis: for b1, b2 being Element of the carrier of (RRing A) holds
( x * (b1 + b2) = (x * b1) + (x * b2) & (b1 + b2) * x = (b1 * x) + (b2 * x) )
thus for b1, b2 being Element of the carrier of (RRing A) holds
( x * (b1 + b2) = (x * b1) + (x * b2) & (b1 + b2) * x = (b1 * x) + (b2 * x) ) by Th25; ::_thesis: verum
end;
A7: RRing A is well-unital
proof
let x be Element of (RRing A); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x )
thus ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x ) by Th25; ::_thesis: verum
end;
A8: RRing A is associative
proof
let x be Element of (RRing A); :: according to GROUP_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of (RRing A) holds (x * b1) * b2 = x * (b1 * b2)
thus for b1, b2 being Element of the carrier of (RRing A) holds (x * b1) * b2 = x * (b1 * b2) by Th25; ::_thesis: verum
end;
RRing A is commutative
proof
let x be Element of (RRing A); :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of (RRing A) holds x * b1 = b1 * x
thus for b1 being Element of the carrier of (RRing A) holds x * b1 = b1 * x by Th25; ::_thesis: verum
end;
hence RRing A is commutative Ring by A1, A2, A5, A3, A8, A7, A6; ::_thesis: verum
end;
definition
attrc1 is strict ;
struct AlgebraStr -> doubleLoopStr , RLSStruct ;
aggrAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> AlgebraStr ;
end;
registration
cluster non empty for AlgebraStr ;
existence
not for b1 being AlgebraStr holds b1 is empty
proof
set X = the non empty set ;
set m = the BinOp of the non empty set ;
set M = the Function of [:REAL, the non empty set :], the non empty set ;
set u = the Element of the non empty set ;
take AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) ; ::_thesis: not AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty
thus not the carrier of AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
definition
let A be set ;
func RAlgebra A -> strict AlgebraStr equals :: FUNCSDOM:def 8
AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);
correctness
coherence
AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict AlgebraStr ;
;
end;
:: deftheorem defines RAlgebra FUNCSDOM:def_8_:_
for A being set holds RAlgebra A = AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);
registration
let A be non empty set ;
cluster RAlgebra A -> non empty strict ;
coherence
not RAlgebra A is empty ;
end;
Lm4: now__::_thesis:_for_A_being_non_empty_set_
for_x,_e_being_Element_of_(RAlgebra_A)_st_e_=_RealFuncUnit_A_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let A be non empty set ; ::_thesis: for x, e being Element of (RAlgebra A) st e = RealFuncUnit A holds
( x * e = x & e * x = x )
set F = RAlgebra A;
let x, e be Element of (RAlgebra A); ::_thesis: ( e = RealFuncUnit A implies ( x * e = x & e * x = x ) )
reconsider f = x as Element of Funcs (A,REAL) ;
assume A1: e = RealFuncUnit A ; ::_thesis: ( x * e = x & e * x = x )
hence x * e = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7
.= x by Th9 ;
::_thesis: e * x = x
thus e * x = x by A1, Th9; ::_thesis: verum
end;
registration
let A be non empty set ;
cluster RAlgebra A -> unital strict ;
coherence
RAlgebra A is unital
proof
reconsider e = RealFuncUnit A as Element of (RAlgebra A) ;
take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (RAlgebra A) holds
( b1 * e = b1 & e * b1 = b1 )
thus for b1 being Element of the carrier of (RAlgebra A) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm4; ::_thesis: verum
end;
end;
theorem :: FUNCSDOM:27
for A being non empty set holds 1. (RAlgebra A) = RealFuncUnit A ;
definition
let IT be non empty AlgebraStr ;
attrIT is vector-associative means :: FUNCSDOM:def 9
for x, y being Element of IT
for a being Real holds a * (x * y) = (a * x) * y;
end;
:: deftheorem defines vector-associative FUNCSDOM:def_9_:_
for IT being non empty AlgebraStr holds
( IT is vector-associative iff for x, y being Element of IT
for a being Real holds a * (x * y) = (a * x) * y );
registration
let A be set ;
cluster RAlgebra A -> non empty strict ;
coherence
not RAlgebra A is empty ;
end;
registration
let A be set ;
cluster RAlgebra A -> right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative ;
coherence
( RAlgebra A is strict & RAlgebra A is Abelian & RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
thus RAlgebra A is strict ; ::_thesis: ( RAlgebra A is Abelian & RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is Abelian ::_thesis: ( RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x, y be Element of (RAlgebra A); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
thus x + y = y + x by Th5; ::_thesis: verum
end;
thus RAlgebra A is add-associative ::_thesis: ( RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x, y, z be Element of (RAlgebra A); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = x + (y + z) by Th6; ::_thesis: verum
end;
thus RAlgebra A is right_zeroed ::_thesis: ( RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x be Element of (RAlgebra A); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (RAlgebra A)) = x
thus x + (0. (RAlgebra A)) = (RealFuncAdd A) . ((RealFuncZero A),x) by Th5
.= x by Th10 ; ::_thesis: verum
end;
thus RAlgebra A is right_complementable ::_thesis: ( RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x be Element of (RAlgebra A); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider f = x as Element of Funcs (A,REAL) ;
reconsider t = (RealFuncExtMult A) . [(- 1),f] as Element of (RAlgebra A) ;
take t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (RAlgebra A)
thus x + t = 0. (RAlgebra A) by Th11; ::_thesis: verum
end;
thus RAlgebra A is commutative ::_thesis: ( RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x, y be Element of (RAlgebra A); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
thus x * y = y * x by Th7; ::_thesis: verum
end;
thus RAlgebra A is associative ::_thesis: ( RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x, y, z be Element of (RAlgebra A); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
thus (x * y) * z = x * (y * z) by Th8; ::_thesis: verum
end;
thus RAlgebra A is right_unital ::_thesis: ( RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x be Element of (RAlgebra A); :: according to VECTSP_1:def_4 ::_thesis: x * (1. (RAlgebra A)) = x
thus x * (1. (RAlgebra A)) = (RealFuncMult A) . ((RealFuncUnit A),x) by Th7
.= x by Th9 ; ::_thesis: verum
end;
thus RAlgebra A is right-distributive ::_thesis: ( RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x, y, z be Element of (RAlgebra A); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: verum
end;
thus RAlgebra A is vector-associative ::_thesis: ( RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x, y be Element of (RAlgebra A); :: according to FUNCSDOM:def_9 ::_thesis: for a being Real holds a * (x * y) = (a * x) * y
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
thus (a * x) * y = a * (x * y) by Th16; ::_thesis: verum
end;
thus RAlgebra A is scalar-associative ::_thesis: ( RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of (RAlgebra A) holds (a * b) * b1 = a * (b * b1)
let x be Element of (RAlgebra A); ::_thesis: (a * b) * x = a * (b * x)
reconsider a = a, b = b as Element of REAL by XREAL_0:def_1;
(a * b) * x = a * (b * x) by Th13;
hence (a * b) * x = a * (b * x) ; ::_thesis: verum
end;
thus RAlgebra A is vector-distributive ::_thesis: RAlgebra A is scalar-distributive
proof
let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of (RAlgebra A) holds a * (b1 + b2) = (a * b1) + (a * b2)
let v, w be Element of (RAlgebra A); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider a = a as Element of REAL by XREAL_0:def_1;
a * (v + w) = (a * v) + (a * w) by Lm2;
hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of (RAlgebra A) holds (a + b) * b1 = (a * b1) + (b * b1)
let v be Element of (RAlgebra A); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Element of REAL by XREAL_0:def_1;
(a + b) * v = (a * v) + (b * v) by Th14;
hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
end;
registration
cluster non empty right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative for AlgebraStr ;
existence
ex b1 being non empty AlgebraStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is commutative & b1 is associative & b1 is right_unital & b1 is right-distributive & b1 is vector-associative & b1 is scalar-associative & b1 is vector-distributive & b1 is scalar-distributive )
proof
take RAlgebra {} ; ::_thesis: ( RAlgebra {} is strict & RAlgebra {} is Abelian & RAlgebra {} is add-associative & RAlgebra {} is right_zeroed & RAlgebra {} is right_complementable & RAlgebra {} is commutative & RAlgebra {} is associative & RAlgebra {} is right_unital & RAlgebra {} is right-distributive & RAlgebra {} is vector-associative & RAlgebra {} is scalar-associative & RAlgebra {} is vector-distributive & RAlgebra {} is scalar-distributive )
thus ( RAlgebra {} is strict & RAlgebra {} is Abelian & RAlgebra {} is add-associative & RAlgebra {} is right_zeroed & RAlgebra {} is right_complementable & RAlgebra {} is commutative & RAlgebra {} is associative & RAlgebra {} is right_unital & RAlgebra {} is right-distributive & RAlgebra {} is vector-associative & RAlgebra {} is scalar-associative & RAlgebra {} is vector-distributive & RAlgebra {} is scalar-distributive ) ; ::_thesis: verum
end;
end;
definition
mode Algebra is non empty right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ;
end;