let UN be Universe; :: thesis: 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 ) )
let R be Ring; :: thesis: 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 ) )
set C = LModCat UN,R;
set V = LModObjects UN,R;
set X = Morphs (LModObjects UN,R);
let b be Object of (LModCat UN,R); :: thesis: ( 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 ) )
reconsider b' = b as Element of LModObjects UN,R ;
reconsider b'' = b' as LeftMod of R ;
A1:
id b = ID b'
by Th16;
hence A2: dom (id b) =
dom (ID b'')
by Th17
.=
b
by MOD_2:26
;
:: thesis: ( 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 ) )
thus A3: cod (id b) =
cod (ID b'')
by A1, Th17
.=
b
by MOD_2:26
; :: thesis: ( ( 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 ) )
thus
for f being Morphism of (LModCat UN,R) st cod f = b holds
(id b) * f = f
:: thesis: for g being Morphism of (LModCat UN,R) st dom g = b holds
g * (id b) = gproof
let f be
Morphism of
(LModCat UN,R);
:: thesis: ( cod f = b implies (id b) * f = f )
assume A4:
cod f = b
;
:: thesis: (id b) * f = f
reconsider f1 =
f as
Element of
Morphs (LModObjects UN,R) ;
ex
G,
H being
strict Element of
LModObjects UN,
R st
f1 is
strict Morphism of
G,
H
by Def7;
then reconsider f' =
f1 as
strict LModMorphism of
R ;
A5:
cod f' = b''
by A4, Th17;
thus (id b) * f =
(ID b'') * f'
by A1, A2, A4, Th18
.=
f
by A5, MOD_2:26
;
:: thesis: verum
end;
thus
for g being Morphism of (LModCat UN,R) st dom g = b holds
g * (id b) = g
:: thesis: verumproof
let f be
Morphism of
(LModCat UN,R);
:: thesis: ( dom f = b implies f * (id b) = f )
assume A6:
dom f = b
;
:: thesis: f * (id b) = f
reconsider f1 =
f as
Element of
Morphs (LModObjects UN,R) ;
ex
G,
H being
strict Element of
LModObjects UN,
R st
f1 is
strict Morphism of
G,
H
by Def7;
then reconsider f' =
f1 as
strict LModMorphism of
R ;
A7:
dom f' = b''
by A6, Th17;
thus f * (id b) =
f' * (ID b'')
by A1, A3, A6, Th18
.=
f
by A7, MOD_2:26
;
:: thesis: verum
end;