:: MODCAT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let R be Ring;
mode LeftMod_DOMAIN of R -> non empty set means :Def1: :: MODCAT_1:def 1
for x being Element of it holds x is strict LeftMod of R;
existence
ex b1 being non empty set st
for x being Element of b1 holds x is strict LeftMod of R
proof end;
end;

:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def 1 :
for R being Ring
for b2 being non empty set holds
( b2 is LeftMod_DOMAIN of R iff for x being Element of b2 holds x is strict LeftMod of R );

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
:: original: Element
redefine mode Element of V -> LeftMod of R;
coherence
for b1 being Element of V holds b1 is LeftMod of R
by Def1;
end;

registration
let R be Ring;
let V be LeftMod_DOMAIN of R;
cluster strict Element of V;
existence
ex b1 being Element of V st b1 is strict
proof end;
end;

definition
let R be Ring;
mode LModMorphism_DOMAIN of R -> non empty set means :Def2: :: MODCAT_1:def 2
for x being Element of it holds x is strict LModMorphism of R;
existence
ex b1 being non empty set st
for x being Element of b1 holds x is strict LModMorphism of R
proof end;
end;

:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def 2 :
for R being Ring
for b2 being non empty set holds
( b2 is LModMorphism_DOMAIN of R iff for x being Element of b2 holds x is strict LModMorphism of R );

definition
let R be Ring;
let M be LModMorphism_DOMAIN of R;
:: original: Element
redefine mode Element of M -> LModMorphism of R;
coherence
for b1 being Element of M holds b1 is LModMorphism of R
by Def2;
end;

registration
let R be Ring;
let M be LModMorphism_DOMAIN of R;
cluster strict Element of M;
existence
ex b1 being Element of M st b1 is strict
proof end;
end;

theorem :: MODCAT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MODCAT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: MODCAT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R
proof end;

definition
let R be Ring;
let G, H be LeftMod of R;
mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means :Def3: :: MODCAT_1:def 3
for x being Element of it holds x is strict Morphism of G,H;
existence
ex b1 being LModMorphism_DOMAIN of R st
for x being Element of b1 holds x is strict Morphism of G,H
proof end;
end;

:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def 3 :
for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of R holds
( b4 is LModMorphism_DOMAIN of G,H iff for x being Element of b4 holds x is strict Morphism of G,H );

theorem Th4: :: MODCAT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for R being Ring
for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
proof end;

theorem :: MODCAT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G, H being LeftMod of R
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
proof end;

definition
let R be Ring;
let G, H be LeftMod of R;
func Morphs G,H -> LModMorphism_DOMAIN of G,H means :Def4: :: MODCAT_1:def 4
for x being set holds
( x in it iff x is strict Morphism of G,H );
existence
ex b1 being LModMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is strict Morphism of G,H )
proof end;
uniqueness
for b1, b2 being LModMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff x is strict Morphism of G,H ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Morphs MODCAT_1:def 4 :
for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of G,H holds
( b4 = Morphs G,H iff for x being set holds
( x in b4 iff x is strict Morphism of G,H ) );

definition
let R be Ring;
let G, H be LeftMod of R;
let M be LModMorphism_DOMAIN of G,H;
:: original: Element
redefine mode Element of M -> Morphism of G,H;
coherence
for b1 being Element of M holds b1 is Morphism of G,H
by Def3;
end;

definition
let x, y be set ;
let R be Ring;
pred GO x,y,R means :Def5: :: MODCAT_1:def 5
ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = LoopStr(# the carrier of G,the add of G,the Zero of G #) & x2 = the lmult of G ) );
end;

:: deftheorem Def5 defines GO MODCAT_1:def 5 :
for x, y being set
for R being Ring holds
( GO x,y,R iff ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = LoopStr(# the carrier of G,the add of G,the Zero of G #) & x2 = the lmult of G ) ) );

theorem Th6: :: MODCAT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for x, y1, y2 being set st GO x,y1,R & GO x,y2,R holds
y1 = y2
proof end;

theorem Th7: :: MODCAT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for UN being Universe ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,{{} }:],{{} } : verum } & GO x, TrivialLMod R,R )
proof end;

definition
let UN be Universe;
let R be Ring;
func LModObjects UN,R -> set means :Def6: :: MODCAT_1:def 6
for y being set holds
( y in it iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,{{} }:],{{} } : verum } & GO x,y,R ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,{{} }:],{{} } : verum } & GO x,y,R ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,{{} }:],{{} } : verum } & GO x,y,R ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,{{} }:],{{} } : verum } & GO x,y,R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines LModObjects MODCAT_1:def 6 :
for UN being Universe
for R being Ring
for b3 being set holds
( b3 = LModObjects UN,R iff for y being set holds
( y in b3 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,{{} }:],{{} } : verum } & GO x,y,R ) ) );

theorem Th8: :: MODCAT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring holds TrivialLMod R in LModObjects UN,R
proof end;

registration
let UN be Universe;
let R be Ring;
cluster LModObjects UN,R -> non empty ;
coherence
not LModObjects UN,R is empty
by Th8;
end;

theorem Th9: :: MODCAT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring
for x being Element of LModObjects UN,R holds x is strict LeftMod of R
proof end;

definition
let UN be Universe;
let R be Ring;
:: original: LModObjects
redefine func LModObjects UN,R -> LeftMod_DOMAIN of R;
coherence
LModObjects UN,R is LeftMod_DOMAIN of R
proof end;
end;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func Morphs V -> LModMorphism_DOMAIN of R means :Def7: :: MODCAT_1:def 7
for x being set holds
( x in it iff ex G, H being strict Element of V st x is strict Morphism of G,H );
existence
ex b1 being LModMorphism_DOMAIN of R st
for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proof end;
uniqueness
for b1, b2 being LModMorphism_DOMAIN of R st ( for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Morphs MODCAT_1:def 7 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being LModMorphism_DOMAIN of R holds
( b3 = Morphs V iff for x being set holds
( x in b3 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
let F be Element of Morphs V;
func dom' F -> Element of V equals :: MODCAT_1:def 8
dom F;
coherence
dom F is Element of V
proof end;
func cod' F -> Element of V equals :: MODCAT_1:def 9
cod F;
coherence
cod F is Element of V
proof end;
end;

:: deftheorem defines dom' MODCAT_1:def 8 :
for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds dom' F = dom F;

:: deftheorem defines cod' MODCAT_1:def 9 :
for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds cod' F = cod F;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
let G be Element of V;
func ID G -> strict Element of Morphs V equals :: MODCAT_1:def 10
ID G;
coherence
ID G is strict Element of Morphs V
proof end;
end;

:: deftheorem defines ID MODCAT_1:def 10 :
for R being Ring
for V being LeftMod_DOMAIN of R
for G being Element of V holds ID G = ID G;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func dom V -> Function of Morphs V,V means :Def11: :: MODCAT_1:def 11
for f being Element of Morphs V holds it . f = dom' f;
existence
ex b1 being Function of Morphs V,V st
for f being Element of Morphs V holds b1 . f = dom' f
proof end;
uniqueness
for b1, b2 being Function of Morphs V,V st ( for f being Element of Morphs V holds b1 . f = dom' f ) & ( for f being Element of Morphs V holds b2 . f = dom' f ) holds
b1 = b2
proof end;
func cod V -> Function of Morphs V,V means :Def12: :: MODCAT_1:def 12
for f being Element of Morphs V holds it . f = cod' f;
existence
ex b1 being Function of Morphs V,V st
for f being Element of Morphs V holds b1 . f = cod' f
proof end;
uniqueness
for b1, b2 being Function of Morphs V,V st ( for f being Element of Morphs V holds b1 . f = cod' f ) & ( for f being Element of Morphs V holds b2 . f = cod' f ) holds
b1 = b2
proof end;
func ID V -> Function of V, Morphs V means :Def13: :: MODCAT_1:def 13
for G being Element of V holds it . G = ID G;
existence
ex b1 being Function of V, Morphs V st
for G being Element of V holds b1 . G = ID G
proof end;
uniqueness
for b1, b2 being Function of V, Morphs V st ( for G being Element of V holds b1 . G = ID G ) & ( for G being Element of V holds b2 . G = ID G ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines dom MODCAT_1:def 11 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of Morphs V,V holds
( b3 = dom V iff for f being Element of Morphs V holds b3 . f = dom' f );

:: deftheorem Def12 defines cod MODCAT_1:def 12 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of Morphs V,V holds
( b3 = cod V iff for f being Element of Morphs V holds b3 . f = cod' f );

:: deftheorem Def13 defines ID MODCAT_1:def 13 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of V, Morphs V holds
( b3 = ID V iff for G being Element of V holds b3 . G = ID G );

theorem Th10: :: MODCAT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proof end;

theorem Th11: :: MODCAT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
g * f in Morphs V
proof end;

theorem Th12: :: MODCAT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
proof end;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func comp V -> PartFunc of [:(Morphs V),(Morphs V):], Morphs V means :Def14: :: MODCAT_1:def 14
( ( for g, f being Element of Morphs V holds
( [g,f] in dom it iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds
it . [g,f] = g * f ) );
existence
ex b1 being PartFunc of [:(Morphs V),(Morphs V):], Morphs V st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . [g,f] = g * f ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):], Morphs V st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . [g,f] = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . [g,f] = g * f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines comp MODCAT_1:def 14 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being PartFunc of [:(Morphs V),(Morphs V):], Morphs V holds
( b3 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b3 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b3 holds
b3 . [g,f] = g * f ) ) );

theorem Th13: :: MODCAT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
proof end;

definition
let UN be Universe;
let R be Ring;
func LModCat UN,R -> strict CatStr equals :: MODCAT_1:def 15
CatStr(# (LModObjects UN,R),(Morphs (LModObjects UN,R)),(dom (LModObjects UN,R)),(cod (LModObjects UN,R)),(comp (LModObjects UN,R)),(ID (LModObjects UN,R)) #);
coherence
CatStr(# (LModObjects UN,R),(Morphs (LModObjects UN,R)),(dom (LModObjects UN,R)),(cod (LModObjects UN,R)),(comp (LModObjects UN,R)),(ID (LModObjects UN,R)) #) is strict CatStr
;
end;

:: deftheorem defines LModCat MODCAT_1:def 15 :
for UN being Universe
for R being Ring holds LModCat UN,R = CatStr(# (LModObjects UN,R),(Morphs (LModObjects UN,R)),(dom (LModObjects UN,R)),(cod (LModObjects UN,R)),(comp (LModObjects UN,R)),(ID (LModObjects UN,R)) #);

theorem Th14: :: MODCAT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat UN,R) holds
( [g,f] in dom the Comp of (LModCat UN,R) iff dom g = cod f )
proof end;

theorem Th15: :: MODCAT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring
for f being Morphism of (LModCat UN,R)
for f' being Element of Morphs (LModObjects UN,R)
for b being Object of (LModCat UN,R)
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
proof end;

theorem Th16: :: MODCAT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring
for b being Object of (LModCat UN,R)
for b' being Element of LModObjects UN,R st b = b' holds
id b = ID b'
proof end;

theorem Th17: :: MODCAT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring
for f being Morphism of (LModCat UN,R)
for f' being Element of Morphs (LModObjects UN,R) st f = f' holds
( dom f = dom f' & cod f = cod f' )
proof end;

theorem Th18: :: MODCAT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat UN,R)
for f', g' being Element of Morphs (LModObjects UN,R) st f = f' & g = g' holds
( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
proof end;

Lm1: for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat UN,R) st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
proof end;

Lm2: for UN being Universe
for R being Ring
for f, g, h being Morphism of (LModCat UN,R) st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
proof end;

Lm3: for UN being Universe
for R being Ring
for b being Object of (LModCat UN,R) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (LModCat UN,R) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat UN,R) st dom g = b holds
g * (id b) = g ) )
proof end;

registration
let UN be Universe;
let R be Ring;
cluster LModCat UN,R -> strict Category-like ;
coherence
LModCat UN,R is Category-like
proof end;
end;