begin
Lm1:
for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L
:: deftheorem VECTSP_2:def 1 :
canceled;
:: deftheorem VECTSP_2:def 2 :
canceled;
:: deftheorem VECTSP_2:def 3 :
canceled;
:: deftheorem VECTSP_2:def 4 :
canceled;
:: deftheorem Def5 defines domRing-like VECTSP_2:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
Lm2:
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y, z being Scalar of R st x + y = z holds
x = z - y
Lm3:
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, z, y being Scalar of R st x = z - y holds
x + y = z
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th42:
:: deftheorem VECTSP_2:def 6 :
canceled;
:: deftheorem Def7 defines " VECTSP_2:def 7 :
:: deftheorem defines / VECTSP_2:def 8 :
theorem Th43:
theorem
canceled;
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem
theorem Th53:
theorem Th54:
theorem
theorem
theorem
registration
let FS1,
FS2 be
1-sorted ;
let A be non
empty set ;
let a be
BinOp of
A;
let Z be
Element of
A;
let l be
Function of
[:the carrier of FS1,A:],
A;
let r be
Function of
[:A,the carrier of FS2:],
A;
cluster BiModStr(#
A,
a,
Z,
l,
r #)
-> non
empty ;
coherence
not BiModStr(# A,a,Z,l,r #) is empty
;
end;
:: deftheorem defines AbGr VECTSP_2:def 9 :
deffunc H1( Ring) -> VectSpStr of $1 = VectSpStr(# the carrier of $1,the addF of $1,(0. $1),the multF of $1 #);
Lm4:
for R being Ring holds
( H1(R) is Abelian & H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
:: deftheorem VECTSP_2:def 10 :
canceled;
:: deftheorem defines LeftModule VECTSP_2:def 11 :
deffunc H2( Ring) -> RightModStr of $1 = RightModStr(# the carrier of $1,the addF of $1,(0. $1),the multF of $1 #);
Lm5:
for R being Ring holds
( H2(R) is Abelian & H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable )
:: deftheorem VECTSP_2:def 12 :
canceled;
:: deftheorem VECTSP_2:def 13 :
canceled;
:: deftheorem defines RightModule VECTSP_2:def 14 :
:: deftheorem defines * VECTSP_2:def 15 :
deffunc H3( Ring, Ring) -> BiModStr of $1,$2 = BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of $1,1),(pr1 1,the carrier of $2) #);
Lm6:
for R1, R2 being Ring holds
( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
definition
let R1,
R2 be
Ring;
canceled;canceled;canceled;canceled;canceled;func BiModule R1,
R2 -> non
empty right_complementable Abelian add-associative right_zeroed strict BiModStr of
R1,
R2 equals
BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #);
coherence
BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #) is non empty right_complementable Abelian add-associative right_zeroed strict BiModStr of R1,R2
by Lm6;
end;
:: deftheorem VECTSP_2:def 16 :
canceled;
:: deftheorem VECTSP_2:def 17 :
canceled;
:: deftheorem VECTSP_2:def 18 :
canceled;
:: deftheorem VECTSP_2:def 19 :
canceled;
:: deftheorem VECTSP_2:def 20 :
canceled;
:: deftheorem defines BiModule VECTSP_2:def 21 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th71:
Lm7:
for R being Ring holds
( LeftModule R is vector-distributive & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th77:
:: deftheorem VECTSP_2:def 22 :
canceled;
:: deftheorem Def23 defines RightMod-like VECTSP_2:def 23 :
Lm8:
for R being Ring holds RightModule R is RightMod-like
Lm9:
for R1, R2 being Ring
for x, y being Scalar of R1
for p, q being Scalar of R2
for v, w being Vector of (BiModule R1,R2) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
:: deftheorem Def24 defines BiMod-like VECTSP_2:def 24 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
R1,
R2 being
Ring for
V being non
empty BiModStr of
R1,
R2 holds
( ( for
x,
y being
Scalar of
R1 for
p,
q being
Scalar of
R2 for
v,
w being
Vector of
V holds
(
x * (v + w) = (x * v) + (x * w) &
(x + y) * v = (x * v) + (y * v) &
(x * y) * v = x * (y * v) &
(1_ R1) * v = v &
(v + w) * p = (v * p) + (w * p) &
v * (p + q) = (v * p) + (v * q) &
v * (q * p) = (v * q) * p &
v * (1_ R2) = v &
x * (v * p) = (x * v) * p ) ) iff (
V is
RightMod-like &
V is
vector-distributive &
V is
scalar-distributive &
V is
scalar-associative &
V is
scalar-unital &
V is
BiMod-like ) )
by Def23, Def24, VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29;
theorem Th84:
registration
let R1,
R2 be
Ring;
cluster BiModule R1,
R2 -> non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict RightMod-like BiMod-like ;
coherence
( BiModule R1,R2 is Abelian & BiModule R1,R2 is add-associative & BiModule R1,R2 is right_zeroed & BiModule R1,R2 is right_complementable & BiModule R1,R2 is RightMod-like & BiModule R1,R2 is vector-distributive & BiModule R1,R2 is scalar-distributive & BiModule R1,R2 is scalar-associative & BiModule R1,R2 is scalar-unital & BiModule R1,R2 is BiMod-like )
by Th84;
end;
theorem
begin
theorem
theorem
theorem
theorem
theorem Th90:
theorem Th91:
theorem Th92:
theorem
theorem
theorem