let R be commutative Ring; for S being non empty multiplicatively-closed Subset of R holds S ~ R is Ring
let S be non empty multiplicatively-closed Subset of R; S ~ R is Ring
A1:
for x, y being Element of (S ~ R) holds x + y = y + x
A4:
for x, y, z being Element of (S ~ R) holds (x + y) + z = x + (y + z)
proof
let x,
y,
z be
Element of
(S ~ R);
(x + y) + z = x + (y + z)
consider a being
Element of
Frac S such that A5:
x = Class (
(EqRel S),
a)
by Th32;
consider b being
Element of
Frac S such that A6:
y = Class (
(EqRel S),
b)
by Th32;
consider c being
Element of
Frac S such that A7:
z = Class (
(EqRel S),
c)
by Th32;
A8:
y + z = Class (
(EqRel S),
(b + c))
by A6, A7, Th35;
x + y = Class (
(EqRel S),
(a + b))
by A5, A6, Th35;
then (x + y) + z =
Class (
(EqRel S),
((a + b) + c))
by A7, Th35
.=
Class (
(EqRel S),
(a + (b + c)))
by Th19
.=
x + (y + z)
by A8, A5, Th35
;
hence
(x + y) + z = x + (y + z)
;
verum
end;
A9:
for x being Element of (S ~ R) holds x + (0. (S ~ R)) = x
A11:
for x being Element of (S ~ R) holds x is right_complementable
proof
let x be
Element of
(S ~ R);
x is right_complementable
ex
y being
Element of
(S ~ R) st
x + y = 0. (S ~ R)
proof
consider a,
b being
Element of
Frac S such that A12:
x = Class (
(EqRel S),
a)
and
0. (S ~ R) = Class (
(EqRel S),
b)
and
the
addF of
(S ~ R) . (
x,
(0. (S ~ R)))
= Class (
(EqRel S),
(a + b))
by Def6;
reconsider u1 =
a `1 as
Element of
R ;
reconsider u2 =
a `2 as
Element of
S by Lm17;
reconsider u =
[(- u1),u2] as
Element of
Frac S by Def3;
A13:
a + u =
[((u1 * u2) + (- (u1 * u2))),(u2 * u2)]
by VECTSP_1:9
.=
[(0. R),(u2 * u2)]
by RLVECT_1:5
;
reconsider s =
1. R as
Element of
S by C0SP1:def 4;
reconsider u3 =
u2 * u2 as
Element of
S by C0SP1:def 4;
(((0. R) * (1. R)) - ((0. R) * u3)) * s = 0. R
;
then
a + u,
0. (
R,
S)
Fr_Eq S
by A13;
then A14:
Class (
(EqRel S),
(a + u)) =
Class (
(EqRel S),
(0. (R,S)))
by Th26
.=
0. (S ~ R)
by Def6
;
A15:
the
carrier of
(S ~ R) = Class (EqRel S)
by Def6;
reconsider y =
Class (
(EqRel S),
u) as
Element of
(S ~ R) by A15, EQREL_1:def 3;
x + y = 0. (S ~ R)
by A14, A12, Th35;
hence
ex
y being
Element of
(S ~ R) st
x + y = 0. (S ~ R)
;
verum
end;
hence
x is
right_complementable
;
verum
end;
A16:
for x, y, z being Element of (S ~ R) holds (x + y) * z = (x * z) + (y * z)
proof
let x,
y,
z be
Element of
(S ~ R);
(x + y) * z = (x * z) + (y * z)
consider a being
Element of
Frac S such that A17:
x = Class (
(EqRel S),
a)
by Th32;
consider b being
Element of
Frac S such that A18:
y = Class (
(EqRel S),
b)
by Th32;
consider c being
Element of
Frac S such that A19:
z = Class (
(EqRel S),
c)
by Th32;
A21:
x * z = Class (
(EqRel S),
(a * c))
by A17, A19, Th33;
A22:
y * z = Class (
(EqRel S),
(b * c))
by A18, A19, Th33;
x + y = Class (
(EqRel S),
(a + b))
by A17, A18, Th35;
then (x + y) * z =
Class (
(EqRel S),
((a + b) * c))
by A19, Th33
.=
Class (
(EqRel S),
((a * c) + (b * c)))
by Th29, Th26
.=
(x * z) + (y * z)
by A21, A22, Th35
;
hence
(x + y) * z = (x * z) + (y * z)
;
verum
end;
A23:
for x, y, z being Element of (S ~ R) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
A25:
for x, y, z being Element of (S ~ R) holds (x * y) * z = x * (y * z)
proof
let x,
y,
z be
Element of
(S ~ R);
(x * y) * z = x * (y * z)
consider a being
Element of
Frac S such that A26:
x = Class (
(EqRel S),
a)
by Th32;
consider b being
Element of
Frac S such that A27:
y = Class (
(EqRel S),
b)
by Th32;
consider c being
Element of
Frac S such that A28:
z = Class (
(EqRel S),
c)
by Th32;
A29:
y * z = Class (
(EqRel S),
(b * c))
by A27, A28, Th33;
x * y = Class (
(EqRel S),
(a * b))
by A26, A27, Th33;
then (x * y) * z =
Class (
(EqRel S),
((a * b) * c))
by A28, Th33
.=
Class (
(EqRel S),
(a * (b * c)))
by Th20
.=
x * (y * z)
by A26, A29, Th33
;
hence
(x * y) * z = x * (y * z)
;
verum
end;
for x being Element of (S ~ R) holds
( x * (1. (S ~ R)) = x & (1. (S ~ R)) * x = x )
hence
S ~ R is Ring
by A1, A4, A9, A11, A23, A25, VECTSP_1:def 6, VECTSP_1:def 7, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16; verum