let L be non empty non trivial right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; :: thesis: for p, q being Polynomial of L
for x being Element of L holds eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = (eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)
let p, q be Polynomial of L; :: thesis: for x being Element of L holds eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = (eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)
let x be Element of L; :: thesis: eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = (eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)
per cases
( ( len p <> 0 & len q <> 0 ) or len p = 0 or len q = 0 )
;
suppose
(
len p <> 0 &
len q <> 0 )
;
:: thesis: eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = (eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)then A1:
(
len p > 0 &
len q > 0 )
;
then A2:
(
len p >= 0 + 1 &
len q >= 0 + 1 )
by NAT_1:13;
then
(
(len p) - 1
>= 0 &
(len q) - 1
>= 0 )
by XREAL_1:21;
then A3:
(
(len p) - 1
= (len p) -' 1 &
(len q) - 1
= (len q) -' 1 )
by XREAL_0:def 2;
(len p) + (len q) >= 0 + (1 + 1)
by A2, XREAL_1:9;
then
((len p) + (len q)) - 2
>= 0
by XREAL_1:21;
then A4:
((len p) + (len q)) -' 2
= ((len p) + (len q)) - 2
by XREAL_0:def 2;
A5:
((len p) + (len q)) - (1 + 1) = ((len p) - 1) + ((len q) - 1)
;
thus eval ((Leading-Monomial p) *' (Leading-Monomial q)),
x =
((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2))
by A1, Lm3
.=
((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * (((power L) . x,((len p) -' 1)) * ((power L) . x,((len q) -' 1)))
by A3, A4, A5, POLYNOM2:2
.=
(p . ((len p) -' 1)) * ((q . ((len q) -' 1)) * (((power L) . x,((len p) -' 1)) * ((power L) . x,((len q) -' 1))))
by GROUP_1:def 4
.=
(p . ((len p) -' 1)) * (((power L) . x,((len p) -' 1)) * ((q . ((len q) -' 1)) * ((power L) . x,((len q) -' 1))))
by GROUP_1:def 4
.=
((p . ((len p) -' 1)) * ((power L) . x,((len p) -' 1))) * ((q . ((len q) -' 1)) * ((power L) . x,((len q) -' 1)))
by GROUP_1:def 4
.=
((p . ((len p) -' 1)) * ((power L) . x,((len p) -' 1))) * (eval (Leading-Monomial q),x)
by Th25
.=
(eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)
by Th25
;
:: thesis: verum end;