let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for a being Element of the carrier of (Polynom-Ring F)
for q being Element of (Polynom-Ring p) st a = q holds
- a = - q
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of the carrier of (Polynom-Ring F)
for q being Element of (Polynom-Ring p) st a = q holds
- a = - q
let a be Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of (Polynom-Ring p) st a = q holds
- a = - q
let q be Element of (Polynom-Ring p); :: thesis: ( a = q implies - a = - q )
reconsider x = - q as Element of (Polynom-Ring F) by Lm8;
A1: the addF of (Polynom-Ring p) = the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p) by RING_4:def 8;
A2: the ZeroF of (Polynom-Ring p) = 0_. F by RING_4:def 8;
assume A3: a = q ; :: thesis: - a = - q
[a,x] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by A3, ZFMISC_1:def 2;
then a + x = q + (- q) by A3, A1, FUNCT_1:49
.= 0. (Polynom-Ring p) by RLVECT_1:5
.= 0. (Polynom-Ring F) by A2, POLYNOM3:def 10 ;
then a = - x by RLVECT_1:6;
hence - a = - q ; :: thesis: verum