:: Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski
::
:: Received June 20, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm2:
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 :: VECTSP_2:1
canceled;
theorem :: VECTSP_2:2
canceled;
theorem :: VECTSP_2:3
canceled;
theorem :: VECTSP_2:4
canceled;
theorem :: VECTSP_2:5
canceled;
theorem :: VECTSP_2:6
canceled;
theorem :: VECTSP_2:7
canceled;
theorem :: VECTSP_2:8
canceled;
theorem :: VECTSP_2:9
canceled;
theorem :: VECTSP_2:10
canceled;
theorem :: VECTSP_2:11
canceled;
theorem :: VECTSP_2:12
canceled;
theorem :: VECTSP_2:13
theorem :: VECTSP_2:14
canceled;
theorem :: VECTSP_2:15
canceled;
theorem :: VECTSP_2:16
canceled;
Lm3:
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
Lm4:
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 :: VECTSP_2:17
canceled;
theorem :: VECTSP_2:18
canceled;
theorem :: VECTSP_2:19
canceled;
theorem :: VECTSP_2:20
canceled;
theorem :: VECTSP_2:21
canceled;
theorem :: VECTSP_2:22
theorem :: VECTSP_2:23
canceled;
theorem :: VECTSP_2:24
canceled;
theorem :: VECTSP_2:25
canceled;
theorem :: VECTSP_2:26
canceled;
theorem :: VECTSP_2:27
canceled;
theorem :: VECTSP_2:28
canceled;
theorem :: VECTSP_2:29
canceled;
theorem :: VECTSP_2:30
canceled;
theorem :: VECTSP_2:31
canceled;
theorem :: VECTSP_2:32
canceled;
theorem :: VECTSP_2:33
canceled;
theorem Th34: :: VECTSP_2:34
theorem :: VECTSP_2:35
canceled;
theorem :: VECTSP_2:36
canceled;
theorem :: VECTSP_2:37
canceled;
theorem :: VECTSP_2:38
theorem :: VECTSP_2:39
theorem Th40: :: VECTSP_2:40
theorem Th41: :: VECTSP_2:41
theorem Th42: :: VECTSP_2:42
:: deftheorem VECTSP_2:def 6 :
canceled;
:: deftheorem Def7 defines " VECTSP_2:def 7 :
:: deftheorem defines / VECTSP_2:def 8 :
theorem Th43: :: VECTSP_2:43
theorem :: VECTSP_2:44
canceled;
theorem Th45: :: VECTSP_2:45
theorem Th46: :: VECTSP_2:46
theorem :: VECTSP_2:47
theorem Th48: :: VECTSP_2:48
theorem Th49: :: VECTSP_2:49
theorem Th50: :: VECTSP_2:50
theorem :: VECTSP_2:51
theorem :: VECTSP_2:52
theorem Th53: :: VECTSP_2:53
theorem Th54: :: VECTSP_2:54
theorem :: VECTSP_2:55
theorem :: VECTSP_2:56
theorem :: VECTSP_2:57
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 #);
Lm5:
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 #);
Lm6:
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) #);
Lm7:
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 :: VECTSP_2:def 21
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 Lm7;
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 :: VECTSP_2:58
canceled;
theorem :: VECTSP_2:59
canceled;
theorem :: VECTSP_2:60
canceled;
theorem :: VECTSP_2:61
canceled;
theorem :: VECTSP_2:62
canceled;
theorem :: VECTSP_2:63
canceled;
theorem :: VECTSP_2:64
canceled;
theorem :: VECTSP_2:65
canceled;
theorem :: VECTSP_2:66
canceled;
theorem :: VECTSP_2:67
canceled;
theorem :: VECTSP_2:68
canceled;
theorem :: VECTSP_2:69
canceled;
theorem :: VECTSP_2:70
canceled;
theorem Th71: :: VECTSP_2:71
Lm8:
for R being Ring holds LeftModule R is VectSp-like
theorem :: VECTSP_2:72
canceled;
theorem :: VECTSP_2:73
canceled;
theorem :: VECTSP_2:74
canceled;
theorem :: VECTSP_2:75
canceled;
theorem :: VECTSP_2:76
canceled;
theorem Th77: :: VECTSP_2:77
:: deftheorem VECTSP_2:def 22 :
canceled;
:: deftheorem Def23 defines RightMod-like VECTSP_2:def 23 :
Lm9:
for R being Ring holds RightModule R is RightMod-like
Lm10:
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 :: VECTSP_2:78
canceled;
theorem :: VECTSP_2:79
canceled;
theorem :: VECTSP_2:80
canceled;
theorem :: VECTSP_2:81
canceled;
theorem :: VECTSP_2:82
canceled;
theorem :: VECTSP_2:83
theorem Th84: :: VECTSP_2:84
theorem :: VECTSP_2:85
theorem :: VECTSP_2:86
theorem :: VECTSP_2:87
theorem :: VECTSP_2:88
theorem :: VECTSP_2:89
theorem Th37: :: VECTSP_2:90
theorem Th38: :: VECTSP_2:91
theorem Th39: :: VECTSP_2:92
theorem :: VECTSP_2:93
theorem :: VECTSP_2:94
theorem :: VECTSP_2:95