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

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

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

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let m be non-zero Monomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies Low ((m *' p),T,i) = m *' (Low (p,T,i)) )

set l = Low (p,T,i);

set lm = Low ((m *' p),T,i);

assume A1: i <= card (Support p) ; :: thesis: Low ((m *' p),T,i) = m *' (Low (p,T,i))

then A2: i <= card (Support (m *' p)) by Th10;

A3: Support (m *' (Low (p,T,i))) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low (p,T,i)) ) } by TERMORD:30;

.= dom (Low ((m *' p),T,i)) by FUNCT_2:def 1 ;

hence Low ((m *' p),T,i) = m *' (Low (p,T,i)) by A28, FUNCT_1:2; :: thesis: verum

for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

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

for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L

for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L

for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let m be non-zero Monomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds

Low ((m *' p),T,i) = m *' (Low (p,T,i))

let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies Low ((m *' p),T,i) = m *' (Low (p,T,i)) )

set l = Low (p,T,i);

set lm = Low ((m *' p),T,i);

assume A1: i <= card (Support p) ; :: thesis: Low ((m *' p),T,i) = m *' (Low (p,T,i))

then A2: i <= card (Support (m *' p)) by Th10;

A3: Support (m *' (Low (p,T,i))) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low (p,T,i)) ) } by TERMORD:30;

A4: now :: thesis: for u being object st u in Support (m *' (Low (p,T,i))) holds

u in Support (Low ((m *' p),T,i))

A16:
Support (m *' p) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) }
by TERMORD:30;u in Support (Low ((m *' p),T,i))

m <> 0_ (n,L)
by POLYNOM7:def 1;

then Support m <> {} by POLYNOM7:1;

then A5: Support m = {(term m)} by POLYNOM7:7;

then term m in Support m by TARSKI:def 1;

then A6: m . (term m) <> 0. L by POLYNOM1:def 4;

let u be object ; :: thesis: ( u in Support (m *' (Low (p,T,i))) implies u in Support (Low ((m *' p),T,i)) )

assume A7: u in Support (m *' (Low (p,T,i))) ; :: thesis: u in Support (Low ((m *' p),T,i))

then reconsider u9 = u as Element of Bags n ;

u in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low (p,T,i)) ) } by A3, A7;

then consider s, t being Element of Bags n such that

A8: u9 = s + t and

A9: s in Support m and

A10: t in Support (Low (p,T,i)) ;

A11: (Low (p,T,i)) . t <> 0. L by A10, POLYNOM1:def 4;

A12: term m = s by A9, A5, TARSKI:def 1;

then (m *' p) . u9 = (m . (term m)) * (p . t) by A8, POLYRED:7

.= (m . (term m)) * ((Low (p,T,i)) . t) by A1, A10, Th31 ;

then (m *' p) . u9 <> 0. L by A11, A6, VECTSP_2:def 1;

then A13: u9 in Support (m *' p) by POLYNOM1:def 4;

end;then Support m <> {} by POLYNOM7:1;

then A5: Support m = {(term m)} by POLYNOM7:7;

then term m in Support m by TARSKI:def 1;

then A6: m . (term m) <> 0. L by POLYNOM1:def 4;

let u be object ; :: thesis: ( u in Support (m *' (Low (p,T,i))) implies u in Support (Low ((m *' p),T,i)) )

assume A7: u in Support (m *' (Low (p,T,i))) ; :: thesis: u in Support (Low ((m *' p),T,i))

then reconsider u9 = u as Element of Bags n ;

u in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low (p,T,i)) ) } by A3, A7;

then consider s, t being Element of Bags n such that

A8: u9 = s + t and

A9: s in Support m and

A10: t in Support (Low (p,T,i)) ;

A11: (Low (p,T,i)) . t <> 0. L by A10, POLYNOM1:def 4;

A12: term m = s by A9, A5, TARSKI:def 1;

then (m *' p) . u9 = (m . (term m)) * (p . t) by A8, POLYRED:7

.= (m . (term m)) * ((Low (p,T,i)) . t) by A1, A10, Th31 ;

then (m *' p) . u9 <> 0. L by A11, A6, VECTSP_2:def 1;

then A13: u9 in Support (m *' p) by POLYNOM1:def 4;

now :: thesis: s + t in Support (Low ((m *' p),T,i))

hence
u in Support (Low ((m *' p),T,i))
by A8; :: thesis: verumassume
not s + t in Support (Low ((m *' p),T,i))
; :: thesis: contradiction

then A14: s + t in Support (Up ((m *' p),T,i)) by A2, A8, A13, Th28;

hence contradiction by TERMORD:def 3; :: thesis: verum

end;then A14: s + t in Support (Up ((m *' p),T,i)) by A2, A8, A13, Th28;

now :: thesis: for t9 being bag of n st t9 in Support (Low (p,T,i)) holds

t9 < t,T

then
t < t,T
by A10;t9 < t,T

let t9 be bag of n; :: thesis: ( t9 in Support (Low (p,T,i)) implies t9 < t,T )

assume t9 in Support (Low (p,T,i)) ; :: thesis: t9 < t,T

then s + t9 in Support (Low ((m *' p),T,i)) by A1, A12, Th40;

then A15: s + t9 < s + t,T by A2, A14, Th29;

not t <= t9,T by A15, TERMORD:5, Th2;

hence t9 < t,T by TERMORD:5; :: thesis: verum

end;assume t9 in Support (Low (p,T,i)) ; :: thesis: t9 < t,T

then s + t9 in Support (Low ((m *' p),T,i)) by A1, A12, Th40;

then A15: s + t9 < s + t,T by A2, A14, Th29;

not t <= t9,T by A15, TERMORD:5, Th2;

hence t9 < t,T by TERMORD:5; :: thesis: verum

hence contradiction by TERMORD:def 3; :: thesis: verum

now :: thesis: for u being object st u in Support (Low ((m *' p),T,i)) holds

u in Support (m *' (Low (p,T,i)))

then A27:
Support (m *' (Low (p,T,i))) = Support (Low ((m *' p),T,i))
by A4, TARSKI:2;u in Support (m *' (Low (p,T,i)))

let u be object ; :: thesis: ( u in Support (Low ((m *' p),T,i)) implies u in Support (m *' (Low (p,T,i))) )

assume A17: u in Support (Low ((m *' p),T,i)) ; :: thesis: u in Support (m *' (Low (p,T,i)))

then reconsider u9 = u as Element of Bags n ;

Support (Low ((m *' p),T,i)) c= Support (m *' p) by A2, Th26;

then u9 in Support (m *' p) by A17;

then A18: u9 in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A16;

m <> 0_ (n,L) by POLYNOM7:def 1;

then Support m <> {} by POLYNOM7:1;

then A19: Support m = {(term m)} by POLYNOM7:7;

then term m in Support m by TARSKI:def 1;

then A20: m . (term m) <> 0. L by POLYNOM1:def 4;

consider s, t being Element of Bags n such that

A21: u = s + t and

A22: s in Support m and

A23: t in Support p by A18;

A24: p . t <> 0. L by A23, POLYNOM1:def 4;

A25: term m = s by A22, A19, TARSKI:def 1;

then A26: t in Support (Low (p,T,i)) by A1, A17, A21, Th40;

(m *' (Low (p,T,i))) . ((term m) + t) = (m . (term m)) * ((Low (p,T,i)) . t) by POLYRED:7

.= (m . (term m)) * (p . t) by A1, A26, Th31 ;

then (m *' (Low (p,T,i))) . u9 <> 0. L by A21, A20, A25, A24, VECTSP_2:def 1;

hence u in Support (m *' (Low (p,T,i))) by POLYNOM1:def 4; :: thesis: verum

end;assume A17: u in Support (Low ((m *' p),T,i)) ; :: thesis: u in Support (m *' (Low (p,T,i)))

then reconsider u9 = u as Element of Bags n ;

Support (Low ((m *' p),T,i)) c= Support (m *' p) by A2, Th26;

then u9 in Support (m *' p) by A17;

then A18: u9 in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A16;

m <> 0_ (n,L) by POLYNOM7:def 1;

then Support m <> {} by POLYNOM7:1;

then A19: Support m = {(term m)} by POLYNOM7:7;

then term m in Support m by TARSKI:def 1;

then A20: m . (term m) <> 0. L by POLYNOM1:def 4;

consider s, t being Element of Bags n such that

A21: u = s + t and

A22: s in Support m and

A23: t in Support p by A18;

A24: p . t <> 0. L by A23, POLYNOM1:def 4;

A25: term m = s by A22, A19, TARSKI:def 1;

then A26: t in Support (Low (p,T,i)) by A1, A17, A21, Th40;

(m *' (Low (p,T,i))) . ((term m) + t) = (m . (term m)) * ((Low (p,T,i)) . t) by POLYRED:7

.= (m . (term m)) * (p . t) by A1, A26, Th31 ;

then (m *' (Low (p,T,i))) . u9 <> 0. L by A21, A20, A25, A24, VECTSP_2:def 1;

hence u in Support (m *' (Low (p,T,i))) by POLYNOM1:def 4; :: thesis: verum

A28: now :: thesis: for x being object st x in dom (m *' (Low (p,T,i))) holds

(m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x

dom (m *' (Low (p,T,i))) =
Bags n
by FUNCT_2:def 1
(m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x

let x be object ; :: thesis: ( x in dom (m *' (Low (p,T,i))) implies (m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x )

assume x in dom (m *' (Low (p,T,i))) ; :: thesis: (m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x

then reconsider b = x as Element of Bags n ;

end;assume x in dom (m *' (Low (p,T,i))) ; :: thesis: (m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x

then reconsider b = x as Element of Bags n ;

now :: thesis: ( ( b in Support (m *' (Low (p,T,i))) & (m *' (Low (p,T,i))) . b = (Low ((m *' p),T,i)) . b ) or ( not b in Support (m *' (Low (p,T,i))) & (m *' (Low (p,T,i))) . b = (Low ((m *' p),T,i)) . b ) )end;

hence
(m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x
; :: thesis: verumper cases
( b in Support (m *' (Low (p,T,i))) or not b in Support (m *' (Low (p,T,i))) )
;

end;

case A29:
b in Support (m *' (Low (p,T,i)))
; :: thesis: (m *' (Low (p,T,i))) . b = (Low ((m *' p),T,i)) . b

then A30:
b in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low (p,T,i)) ) }
by A3;

A31: b in Support (Low ((m *' p),T,i)) by A4, A29;

consider s, t being Element of Bags n such that

A32: b = s + t and

A33: s in Support m and

A34: t in Support (Low (p,T,i)) by A30;

Support m = {(term m)} by A33, POLYNOM7:7;

then A35: term m = s by A33, TARSKI:def 1;

hence (m *' (Low (p,T,i))) . b = (m . (term m)) * ((Low (p,T,i)) . t) by A32, POLYRED:7

.= (m . (term m)) * (p . t) by A1, A34, Th31

.= (m *' p) . b by A32, A35, POLYRED:7

.= (Low ((m *' p),T,i)) . b by A2, A31, Th31 ;

:: thesis: verum

end;A31: b in Support (Low ((m *' p),T,i)) by A4, A29;

consider s, t being Element of Bags n such that

A32: b = s + t and

A33: s in Support m and

A34: t in Support (Low (p,T,i)) by A30;

Support m = {(term m)} by A33, POLYNOM7:7;

then A35: term m = s by A33, TARSKI:def 1;

hence (m *' (Low (p,T,i))) . b = (m . (term m)) * ((Low (p,T,i)) . t) by A32, POLYRED:7

.= (m . (term m)) * (p . t) by A1, A34, Th31

.= (m *' p) . b by A32, A35, POLYRED:7

.= (Low ((m *' p),T,i)) . b by A2, A31, Th31 ;

:: thesis: verum

.= dom (Low ((m *' p),T,i)) by FUNCT_2:def 1 ;

hence Low ((m *' p),T,i) = m *' (Low (p,T,i)) by A28, FUNCT_1:2; :: thesis: verum