let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being LeftIdeal of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being LeftIdeal of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being LeftIdeal of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let I be LeftIdeal of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let G be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) implies G -Ideal = I )

assume A1: G c= I ; :: thesis: ( ex f being Polynomial of n,L st

( f in I & not PolyRedRel (G,T) reduces f, 0_ (n,L) ) or G -Ideal = I )

PolyRedRel (G,T) reduces f, 0_ (n,L) ; :: thesis: G -Ideal = I

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being LeftIdeal of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being LeftIdeal of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being LeftIdeal of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let I be LeftIdeal of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds

G -Ideal = I

let G be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G c= I & ( for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) ) implies G -Ideal = I )

assume A1: G c= I ; :: thesis: ( ex f being Polynomial of n,L st

( f in I & not PolyRedRel (G,T) reduces f, 0_ (n,L) ) or G -Ideal = I )

A2: now :: thesis: for u being object st u in G -Ideal holds

u in I

assume A4:
for f being Polynomial of n,L st f in I holds u in I

let u be object ; :: thesis: ( u in G -Ideal implies u in I )

assume A3: u in G -Ideal ; :: thesis: u in I

G -Ideal c= I by A1, IDEAL_1:def 14;

hence u in I by A3; :: thesis: verum

end;assume A3: u in G -Ideal ; :: thesis: u in I

G -Ideal c= I by A1, IDEAL_1:def 14;

hence u in I by A3; :: thesis: verum

PolyRedRel (G,T) reduces f, 0_ (n,L) ; :: thesis: G -Ideal = I

now :: thesis: for u being object st u in I holds

u in G -Ideal

hence
G -Ideal = I
by A2, TARSKI:2; :: thesis: verumu in G -Ideal

let u be object ; :: thesis: ( u in I implies u in G -Ideal )

assume A5: u in I ; :: thesis: u in G -Ideal

then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;

reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;

PolyRedRel (G,T) reduces u9, 0_ (n,L) by A4, A5;

hence u in G -Ideal by POLYRED:60; :: thesis: verum

end;assume A5: u in I ; :: thesis: u in G -Ideal

then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;

reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;

PolyRedRel (G,T) reduces u9, 0_ (n,L) by A4, A5;

hence u in G -Ideal by POLYRED:60; :: thesis: verum