let L be domRing; :: thesis: for a being Element of L holds
( a | L is Unit of (Polynom-Ring L) iff a is Unit of L )
let a be Element of L; :: thesis: ( a | L is Unit of (Polynom-Ring L) iff a is Unit of L )
set R = Polynom-Ring L;
H1: 1. (Polynom-Ring L) = 1_. L by POLYNOM3:def 10;
reconsider p = a | L as Element of (Polynom-Ring L) by POLYNOM3:def 10;
A: now :: thesis: ( p is Unit of (Polynom-Ring L) implies a is Unit of L )
assume AS: p is Unit of (Polynom-Ring L) ; :: thesis: a is Unit of L
then a | L divides 1_. L by H1, GCD_1:def 2;
then consider q being Polynomial of L such that
H3: (a | L) *' q = 1_. L by T2;
reconsider qq = q as Element of (Polynom-Ring L) by POLYNOM3:def 10;
p <> 0. (Polynom-Ring L) by AS;
then H4: a | L <> 0_. L by POLYNOM3:def 10;
q <> 0_. L by H3, POLYNOM3:34;
then H6: (deg (a | L)) + (deg q) = deg (1_. L) by H3, H4, HURWITZ:23
.= 1 - 1 by POLYNOM4:4 ;
deg (a | L) is Element of NAT by H4, T8b;
then qq is constant by H6;
then consider b being Element of L such that
H5: qq = b | L by T11;
(a * b) | L = (1. L) | L by H3, H5, T4;
then a divides 1. L by T9;
hence a is Unit of L by GCD_1:def 2; :: thesis: verum
end;
now :: thesis: ( a is Unit of L implies p is Unit of (Polynom-Ring L) )
assume a is Unit of L ; :: thesis: p is Unit of (Polynom-Ring L)
then a divides 1. L by GCD_1:def 2;
then consider b being Element of L such that
H3: a * b = 1. L ;
(a | L) *' (b | L) = (1. L) | L by T4, H3
.= 1_. L ;
then a | L divides 1_. L by T2;
hence p is Unit of (Polynom-Ring L) by H1, GCD_1:def 2; :: thesis: verum
end;
hence ( a | L is Unit of (Polynom-Ring L) iff a is Unit of L ) by A; :: thesis: verum