let A be Ring; for X being non empty set
for f being Function of A,X st f is bijective holds
emb_Ring f is Ring
let X be non empty set ; for f being Function of A,X st f is bijective holds
emb_Ring f is Ring
let f be Function of A,X; ( f is bijective implies emb_Ring f is Ring )
assume A1:
f is bijective
; emb_Ring f is Ring
then A2:
rng f = X
by FUNCT_2:def 3;
A3:
dom f = [#] A
by FUNCT_2:def 1;
reconsider ZS = doubleLoopStr(# X,(addemb f),(multemb f),(f . (1. A)),(f . (0. A)) #) as non empty doubleLoopStr ;
A5:
for v, w being Element of ZS holds v + w = w + v
proof
let v,
w be
Element of
ZS;
v + w = w + v
reconsider v1 =
v,
w1 =
w as
Element of
X ;
reconsider x =
(f ") . v1,
y =
(f ") . w1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
v + w =
addemb (
f,
v1,
w1)
by Def2
.=
f . (x + y)
by A1, Def1
.=
f . (y + x)
.=
addemb (
f,
w1,
v1)
by A1, Def1
.=
w + v
by Def2
;
hence
v + w = w + v
;
verum
end;
A6:
emb_Ring f is Abelian
by A5;
for u, v, w being Element of ZS holds u + (v + w) = (u + v) + w
proof
let u,
v,
w be
Element of
ZS;
u + (v + w) = (u + v) + w
reconsider u1 =
u,
v1 =
v,
w1 =
w as
Element of
X ;
u + (v + w) =
addemb (
f,
u1,
((addemb f) . (v1,w1)))
by Def2
.=
addemb (
f,
u1,
(addemb (f,v1,w1)))
by Def2
.=
addemb (
f,
(addemb (f,u1,v1)),
w1)
by A1, Th4
.=
addemb (
f,
((addemb f) . (u1,v1)),
w1)
by Def2
.=
(u + v) + w
by Def2
;
hence
u + (v + w) = (u + v) + w
;
verum
end;
then A8:
emb_Ring f is add-associative
;
for v being Element of ZS holds v + (0. ZS) = v
proof
let v be
Element of
ZS;
v + (0. ZS) = v
reconsider v1 =
v as
Element of
X ;
reconsider x =
(f ") . v1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
v + (0. ZS) =
addemb (
f,
v1,
(f . (0. A)))
by Def2
.=
f . ( the addF of A . (((f ") . v1),((f ") . (f . (0. A)))))
by A1, Def1
.=
f . (x + (0. A))
by A1, A3, FUNCT_1:34
.=
v1
by A1, A2, FUNCT_1:35
;
hence
v + (0. ZS) = v
;
verum
end;
then A9:
emb_Ring f is right_zeroed
;
A10:
for v being Element of ZS holds v is right_complementable
proof
let v be
Element of
ZS;
v is right_complementable
reconsider v1 =
v as
Element of
X ;
reconsider x =
(f ") . v1 as
Element of
A by A2, A3, A1, FUNCT_1:32;
consider u being
Element of
ZS such that A11:
u = f . (- x)
;
reconsider u1 =
u as
Element of
X ;
v + u =
addemb (
f,
v1,
u1)
by Def2
.=
f . ( the addF of A . (((f ") . v1),((f ") . u1)))
by A1, Def1
.=
f . (x + (- x))
by A11, A3, A1, FUNCT_1:34
.=
0. ZS
by RLVECT_1:5
;
hence
v is
right_complementable
;
verum
end;
A12:
emb_Ring f is right_complementable
by A10;
A13:
for a, b, v being Element of ZS holds (a + b) * v = (a * v) + (b * v)
proof
let a,
b,
v be
Element of
ZS;
(a + b) * v = (a * v) + (b * v)
reconsider a1 =
a,
b1 =
b,
v1 =
v as
Element of
X ;
reconsider ab =
a + b as
Element of
ZS ;
reconsider ab1 =
a + b as
Element of
X ;
reconsider x =
(f ") . a1,
y =
(f ") . b1,
z =
(f ") . v1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
A14:
a + b =
addemb (
f,
a1,
b1)
by Def2
.=
f . (x + y)
by A1, Def1
;
A15:
(f ") . ab1 = x + y
by A14, A1, A3, FUNCT_1:34;
A16:
(a + b) * v =
multemb (
f,
ab1,
v1)
by Def4
.=
f . ((x + y) * z)
by A15, A1, Def3
.=
f . ((x * z) + (y * z))
by VECTSP_1:def 7
;
reconsider av1 =
a * v,
bv1 =
b * v as
Element of
X ;
A17:
a * v =
multemb (
f,
a1,
v1)
by Def4
.=
f . ( the multF of A . (((f ") . a1),((f ") . v1)))
by A1, Def3
;
A18:
b * v =
multemb (
f,
b1,
v1)
by Def4
.=
f . ( the multF of A . (((f ") . b1),((f ") . v1)))
by A1, Def3
;
reconsider za =
(f ") . av1,
zb =
(f ") . bv1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
A19:
za = x * z
by A3, A1, A17, FUNCT_1:34;
A20:
zb = y * z
by A3, A1, A18, FUNCT_1:34;
(a * v) + (b * v) =
addemb (
f,
av1,
bv1)
by Def2
.=
(a + b) * v
by A16, A19, A20, A1, Def1
;
hence
(a + b) * v = (a * v) + (b * v)
;
verum
end;
for a, b, v being Element of ZS holds
( v * (a + b) = (v * a) + (v * b) & (a + b) * v = (a * v) + (b * v) )
proof
let a,
b,
v be
Element of
ZS;
( v * (a + b) = (v * a) + (v * b) & (a + b) * v = (a * v) + (b * v) )
reconsider a1 =
a,
v1 =
v,
b1 =
b as
Element of
X ;
reconsider ab =
a + b as
Element of
ZS ;
reconsider ab1 =
a + b as
Element of
X ;
reconsider x =
(f ") . a1,
y =
(f ") . b1,
z =
(f ") . v1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
A21:
a + b =
addemb (
f,
a1,
b1)
by Def2
.=
f . (x + y)
by A1, Def1
;
A22:
(f ") . ab1 = x + y
by A21, A1, A3, FUNCT_1:34;
A23:
v * (a + b) =
multemb (
f,
v1,
ab1)
by Def4
.=
f . (z * (x + y))
by A22, A1, Def3
.=
f . ((z * x) + (z * y))
by VECTSP_1:def 7
;
reconsider va1 =
v * a,
vb1 =
v * b as
Element of
X ;
A24:
v * a =
multemb (
f,
v1,
a1)
by Def4
.=
f . ( the multF of A . (((f ") . v1),((f ") . a1)))
by A1, Def3
;
A25:
v * b =
multemb (
f,
v1,
b1)
by Def4
.=
f . ( the multF of A . (((f ") . v1),((f ") . b1)))
by A1, Def3
;
reconsider za =
(f ") . va1,
zb =
(f ") . vb1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
A26:
za = z * x
by A3, A1, A24, FUNCT_1:34;
A27:
zb = z * y
by A3, A1, A25, FUNCT_1:34;
(v * a) + (v * b) =
addemb (
f,
va1,
vb1)
by Def2
.=
v * (a + b)
by A23, A26, A27, A1, Def1
;
hence
(
v * (a + b) = (v * a) + (v * b) &
(a + b) * v = (a * v) + (b * v) )
by A13;
verum
end;
then A28:
emb_Ring f is distributive
;
for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
proof
let a,
b,
v be
Element of
ZS;
(a * b) * v = a * (b * v)
reconsider a1 =
a,
b1 =
b,
v1 =
v as
Element of
X ;
reconsider x =
(f ") . a1,
y =
(f ") . b1,
z =
(f ") . v1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
reconsider ab1 =
a * b,
bv1 =
b * v as
Element of
X ;
A29:
a * b =
multemb (
f,
a1,
b1)
by Def4
.=
f . (x * y)
by A1, Def3
;
A30:
b * v =
multemb (
f,
b1,
v1)
by Def4
.=
f . (y * z)
by A1, Def3
;
(a * b) * v =
multemb (
f,
ab1,
v1)
by Def4
.=
f . ( the multF of A . (((f ") . ab1),((f ") . v1)))
by A1, Def3
.=
f . ((x * y) * z)
by A1, A3, A29, FUNCT_1:34
.=
f . (x * (y * z))
by GROUP_1:def 3
.=
f . ( the multF of A . (((f ") . a1),((f ") . bv1)))
by A1, A3, A30, FUNCT_1:34
.=
multemb (
f,
a1,
bv1)
by A1, Def3
.=
a * (b * v)
by Def4
;
hence
(a * b) * v = a * (b * v)
;
verum
end;
then A31:
emb_Ring f is associative
;
for v being Element of ZS holds
( v * (1. ZS) = v & (1. ZS) * v = v )
proof
let v be
Element of
ZS;
( v * (1. ZS) = v & (1. ZS) * v = v )
reconsider v1 =
v,
1zs =
1. ZS as
Element of
X ;
reconsider y =
(f ") . v1,
z =
(f ") . 1zs as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
A32:
v * (1. ZS) =
multemb (
f,
v1,
1zs)
by Def4
.=
f . (y * z)
by A1, Def3
.=
f . (y * (1. A))
by A1, A3, FUNCT_1:34
.=
v1
by A1, A2, FUNCT_1:35
;
(1. ZS) * v =
multemb (
f,
1zs,
v1)
by Def4
.=
f . (z * y)
by A1, Def3
.=
f . ((1. A) * y)
by A1, A3, FUNCT_1:34
.=
v1
by A1, A2, FUNCT_1:35
;
hence
(
v * (1. ZS) = v &
(1. ZS) * v = v )
by A32;
verum
end;
then
emb_Ring f is well-unital
;
hence
emb_Ring f is Ring
by A31, A6, A8, A9, A12, A28; verum