begin
theorem LMPX1:
:: deftheorem defPrj defines ProjSet GROUP_12:def 1 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Subset of (product F) holds
( b4 = ProjSet (F,i) iff for x being set holds
( x in b4 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) );
theorem LMP1:
theorem LMPX2:
theorem LMPX3:
theorem LMP2:
theorem LMP2x:
:: deftheorem defPrjGroup defines ProjGroup GROUP_12:def 2 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being strict Subgroup of product F holds
( b4 = ProjGroup (F,i) iff the carrier of b4 = ProjSet (F,i) );
Lm1:
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
definition
let I be non
empty set ;
let F be
Group-like associative multMagma-Family of
I;
let i be
Element of
I;
func 1ProdHom (
F,
i)
-> Homomorphism of
(F . i),
(ProjGroup (F,i)) means :
1Def:
for
x being
Element of
(F . i) holds
it . x = (1_ (product F)) +* (
i,
x);
existence
ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st
for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x)
uniqueness
for b1, b2 being Homomorphism of (F . i),(ProjGroup (F,i)) st ( for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds b2 . x = (1_ (product F)) +* (i,x) ) holds
b1 = b2
end;
:: deftheorem 1Def defines 1ProdHom GROUP_12:def 3 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Homomorphism of (F . i),(ProjGroup (F,i)) holds
( b4 = 1ProdHom (F,i) iff for x being Element of (F . i) holds b4 . x = (1_ (product F)) +* (i,x) );
theorem
theorem LMP400:
theorem LMP500:
theorem THA1:
theorem THA2:
theorem LST:
theorem