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

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