thus
not Polynom-Ring n,L is trivial
:: thesis: Polynom-Ring n,L is distributive proof
take u =
1_ (Polynom-Ring n,L);
:: according to STRUCT_0:def 19 :: thesis: not u = 0. (Polynom-Ring n,L)
A1:
0. L <> 1_ L
by POLYNOM1:27;
A2:
0. (Polynom-Ring n,L) = 0_ n,
L
by POLYNOM1:def 27;
A3:
1_ (Polynom-Ring n,L) = 1_ n,
L
by POLYNOM1:90;
(0_ n,L) . (EmptyBag n) = 0. L
by POLYNOM1:81;
hence
not
u = 0. (Polynom-Ring n,L)
by A1, A2, A3, POLYNOM1:84;
:: thesis: verum
end;
thus
Polynom-Ring n,L is distributive
:: thesis: verumproof
let x,
y,
z be
Element of
(Polynom-Ring n,L);
:: according to VECTSP_1:def 18 :: thesis: ( 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 27;
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
(Polynom-Ring n,L) ;
A4:
y' + z' = v + w
by POLYNOM1:def 27;
A5:
u *' v = x' * y'
by POLYNOM1:def 27;
A6:
u *' w = x' * z'
by POLYNOM1:def 27;
thus x * (y + z) =
u *' (v + w)
by A4, POLYNOM1:def 27
.=
(u *' v) + (u *' w)
by POLYNOM1:85
.=
(x * y) + (x * z)
by A5, A6, POLYNOM1:def 27
;
:: thesis: (y + z) * x = (y * x) + (z * x)
A7:
y' + z' = v + w
by POLYNOM1:def 27;
A8:
v *' u = y' * x'
by POLYNOM1:def 27;
A9:
w *' u = z' * x'
by POLYNOM1:def 27;
thus (y + z) * x =
(v + w) *' u
by A7, POLYNOM1:def 27
.=
(v *' u) + (w *' u)
by Th8
.=
(y * x) + (z * x)
by A8, A9, POLYNOM1:def 27
;
:: thesis: verum
end;