let i be Integer; :: thesis: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr

for a being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . (a |^ i) = i * (v . a) )

assume that

A1: K is having_valuation and

A2: a <> 0. K ; :: thesis: v . (a |^ i) = i * (v . a)

defpred S_{1}[ Nat] means v . (a |^ $1) = $1 * (v . a);

a |^ 0 = 1_ K by GROUP_1:def 7;

then A3: S_{1}[ 0 ]
by A1, Th17;

A4: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A3, A4);

for a being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . (a |^ i) = i * (v . a) )

assume that

A1: K is having_valuation and

A2: a <> 0. K ; :: thesis: v . (a |^ i) = i * (v . a)

defpred S

a |^ 0 = 1_ K by GROUP_1:def 7;

then A3: S

A4: for n being Nat st S

S

proof

A7:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

A6: v . a in REAL by A1, A2, Th18, XXREAL_0:14;

reconsider N = n as ExtReal ;

thus v . (a |^ (n + 1)) = v . ((a |^ n) * a) by Lm2

.= (n * (v . a)) + (v . a) by A5, A1, Def8

.= (n * (v . a)) + (1. * (v . a)) by XXREAL_3:81

.= (v . a) * (N + 1.) by A6, XXREAL_3:95

.= (n + 1) * (v . a) by XXREAL_3:def 2 ; :: thesis: verum

end;assume A5: S

A6: v . a in REAL by A1, A2, Th18, XXREAL_0:14;

reconsider N = n as ExtReal ;

thus v . (a |^ (n + 1)) = v . ((a |^ n) * a) by Lm2

.= (n * (v . a)) + (v . a) by A5, A1, Def8

.= (n * (v . a)) + (1. * (v . a)) by XXREAL_3:81

.= (v . a) * (N + 1.) by A6, XXREAL_3:95

.= (n + 1) * (v . a) by XXREAL_3:def 2 ; :: thesis: verum

per cases
( i >= 0 or i < 0 )
;

end;

suppose
i >= 0
; :: thesis: v . (a |^ i) = i * (v . a)

then reconsider j = i as Element of NAT by INT_1:3;

S_{1}[j]
by A7;

hence v . (a |^ i) = i * (v . a) ; :: thesis: verum

end;S

hence v . (a |^ i) = i * (v . a) ; :: thesis: verum

suppose A8:
i < 0
; :: thesis: v . (a |^ i) = i * (v . a)

then reconsider n1 = - i as Element of NAT by INT_1:3;

reconsider I = i as ExtReal ;

A9: v . (a |^ i) = v . (((power K) . (a,|.i.|)) ") by A8, Def5

.= v . ((a |^ n1) ") by A8, ABSVALUE:def 1 ;

v . ((a |^ n1) ") = - (v . (a |^ n1)) by A1, A2, Th21, Lm3

.= - (n1 * (v . a)) by A7

.= - ((- I) * (v . a)) by XXREAL_3:def 3

.= - (- (i * (v . a))) by XXREAL_3:92 ;

hence v . (a |^ i) = i * (v . a) by A9; :: thesis: verum

end;reconsider I = i as ExtReal ;

A9: v . (a |^ i) = v . (((power K) . (a,|.i.|)) ") by A8, Def5

.= v . ((a |^ n1) ") by A8, ABSVALUE:def 1 ;

v . ((a |^ n1) ") = - (v . (a |^ n1)) by A1, A2, Th21, Lm3

.= - (n1 * (v . a)) by A7

.= - ((- I) * (v . a)) by XXREAL_3:def 3

.= - (- (i * (v . a))) by XXREAL_3:92 ;

hence v . (a |^ i) = i * (v . a) by A9; :: thesis: verum