let n be Ordinal; for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let O be connected TermOrder of n; for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let p be Polynomial of n,L; Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
A1:
now for u being object st u in Support (Red (p,O)) holds
u in (Support p) \ {(HT (p,O))}let u be
object ;
( u in Support (Red (p,O)) implies u in (Support p) \ {(HT (p,O))} )assume A2:
u in Support (Red (p,O))
;
u in (Support p) \ {(HT (p,O))}then reconsider u9 =
u as
Element of
Bags n ;
reconsider u9 =
u9 as
bag of
n ;
A3:
(p - (HM (p,O))) . u9 <> 0. L
by A2, POLYNOM1:def 4;
A4:
not
u9 = HT (
p,
O)
by A2, Lm15;
(p + (- (HM (p,O)))) . u9 =
(p . u9) + ((- (HM (p,O))) . u9)
by POLYNOM1:15
.=
(p . u9) + (- ((HM (p,O)) . u9))
by POLYNOM1:17
;
then (p + (- (HM (p,O)))) . u9 =
(p . u9) + (- (0. L))
by A4, Th19
.=
(p . u9) + (0. L)
by RLVECT_1:12
.=
p . u9
by RLVECT_1:4
;
then
p . u9 <> 0. L
by A3, POLYNOM1:def 7;
then A5:
u9 in Support p
by POLYNOM1:def 4;
not
u9 in {(HT (p,O))}
by A4, TARSKI:def 1;
hence
u in (Support p) \ {(HT (p,O))}
by A5, XBOOLE_0:def 5;
verum end;
now for u being object st u in (Support p) \ {(HT (p,O))} holds
u in Support (Red (p,O))let u be
object ;
( u in (Support p) \ {(HT (p,O))} implies u in Support (Red (p,O)) )assume A6:
u in (Support p) \ {(HT (p,O))}
;
u in Support (Red (p,O))then reconsider u9 =
u as
Element of
Bags n ;
reconsider u9 =
u9 as
bag of
n ;
not
u in {(HT (p,O))}
by A6, XBOOLE_0:def 5;
then A7:
u9 <> HT (
p,
O)
by TARSKI:def 1;
u in Support p
by A6, XBOOLE_0:def 5;
hence
u in Support (Red (p,O))
by A7, Lm16;
verum end;
hence
Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
by A1, TARSKI:2; verum