thus
not Polynom-Ring (n,L) is trivial
Polynom-Ring (n,L) is distributive proof
take
1_ (Polynom-Ring (n,L))
;
STRUCT_0:def 18 not 1_ (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L))
A1:
(
1_ (Polynom-Ring (n,L)) = 1_ (
n,
L) &
(0_ (n,L)) . (EmptyBag n) = 0. L )
by POLYNOM1:22, POLYNOM1:31;
(
0. L <> 1_ L &
0. (Polynom-Ring (n,L)) = 0_ (
n,
L) )
by POLYNOM1:def 11;
hence
not
1_ (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L))
by A1, POLYNOM1:25;
verum
end;
thus
Polynom-Ring (n,L) is distributive
verumproof
let x,
y,
z be
Element of
(Polynom-Ring (n,L));
VECTSP_1:def 7 ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider u =
x,
v =
y,
w =
z as
Polynomial of
n,
L by POLYNOM1:def 11;
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
(Polynom-Ring (n,L)) ;
A2:
(
u *' v = x9 * y9 &
u *' w = x9 * z9 )
by POLYNOM1:def 11;
y9 + z9 = v + w
by POLYNOM1:def 11;
hence x * (y + z) =
u *' (v + w)
by POLYNOM1:def 11
.=
(u *' v) + (u *' w)
by POLYNOM1:26
.=
(x * y) + (x * z)
by A2, POLYNOM1:def 11
;
(y + z) * x = (y * x) + (z * x)
A3:
(
v *' u = y9 * x9 &
w *' u = z9 * x9 )
by POLYNOM1:def 11;
y9 + z9 = v + w
by POLYNOM1:def 11;
hence (y + z) * x =
(v + w) *' u
by POLYNOM1:def 11
.=
(v *' u) + (w *' u)
by Th8
.=
(y * x) + (z * x)
by A3, POLYNOM1:def 11
;
verum
end;