let n, i be Element of NAT ; :: thesis: for q being Element of REAL n

for p being Point of (TOP-REAL n) st i in Seg n & q = p holds

|.(p /. i).| <= |.q.|

let q be Element of REAL n; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n & q = p holds

|.(p /. i).| <= |.q.|

let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n & q = p implies |.(p /. i).| <= |.q.| )

assume that

A1: i in Seg n and

A2: q = p ; :: thesis: |.(p /. i).| <= |.q.|

reconsider p2 = (p /. i) ^2 , q2 = (q /. i) ^2 as Element of REAL by XREAL_0:def 1;

A3: Sum ((0* n) +* (i,p2)) = (p /. i) ^2 by A1, JORDAN2B:10;

len (0* n) = n by CARD_1:def 7;

then len ((0* n) +* (i,p2)) = n by FUNCT_7:97;

then reconsider w1 = (0* n) +* (i,p2) as Element of n -tuples_on REAL by FINSEQ_2:92;

A4: len w1 = n by CARD_1:def 7;

reconsider w2 = sqr q as Element of n -tuples_on REAL ;

A5: Sum (sqr q) >= 0 by RVSUM_1:86;

A6: len q = n by CARD_1:def 7;

for j being Nat st j in Seg n holds

w1 . j <= w2 . j

then ( 0 <= (p /. i) ^2 & (p /. i) ^2 <= (sqrt (Sum (sqr q))) ^2 ) by A5, A3, SQUARE_1:def 2, XREAL_1:63;

then sqrt ((p /. i) ^2) <= sqrt ((sqrt (Sum (sqr q))) ^2) by SQUARE_1:26;

then |.|.(p /. i).|.| <= sqrt ((sqrt (Sum (sqr q))) ^2) by COMPLEX1:72;

then ( 0 <= |.q.| & |.(p /. i).| <= |.(sqrt (Sum (sqr q))).| ) by COMPLEX1:72;

hence |.(p /. i).| <= |.q.| by ABSVALUE:def 1; :: thesis: verum

for p being Point of (TOP-REAL n) st i in Seg n & q = p holds

|.(p /. i).| <= |.q.|

let q be Element of REAL n; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n & q = p holds

|.(p /. i).| <= |.q.|

let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n & q = p implies |.(p /. i).| <= |.q.| )

assume that

A1: i in Seg n and

A2: q = p ; :: thesis: |.(p /. i).| <= |.q.|

reconsider p2 = (p /. i) ^2 , q2 = (q /. i) ^2 as Element of REAL by XREAL_0:def 1;

A3: Sum ((0* n) +* (i,p2)) = (p /. i) ^2 by A1, JORDAN2B:10;

len (0* n) = n by CARD_1:def 7;

then len ((0* n) +* (i,p2)) = n by FUNCT_7:97;

then reconsider w1 = (0* n) +* (i,p2) as Element of n -tuples_on REAL by FINSEQ_2:92;

A4: len w1 = n by CARD_1:def 7;

reconsider w2 = sqr q as Element of n -tuples_on REAL ;

A5: Sum (sqr q) >= 0 by RVSUM_1:86;

A6: len q = n by CARD_1:def 7;

for j being Nat st j in Seg n holds

w1 . j <= w2 . j

proof

then
Sum w1 <= Sum w2
by RVSUM_1:82;
let j be Nat; :: thesis: ( j in Seg n implies w1 . j <= w2 . j )

assume A7: j in Seg n ; :: thesis: w1 . j <= w2 . j

set r1 = w1 . j;

set r2 = w2 . j;

end;assume A7: j in Seg n ; :: thesis: w1 . j <= w2 . j

set r1 = w1 . j;

set r2 = w2 . j;

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

end;

suppose A8:
j = i
; :: thesis: w1 . j <= w2 . j

then
j in dom q
by A1, A6, FINSEQ_1:def 3;

then A9: q /. j = q . j by PARTFUN1:def 6;

A10: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

i in dom w1 by A1, A4, FINSEQ_1:def 3;

then w1 . j = w1 /. i by A8, PARTFUN1:def 6

.= q2 by A2, A1, A10, FUNCT_7:36 ;

hence w1 . j <= w2 . j by A8, A9, VALUED_1:11; :: thesis: verum

end;then A9: q /. j = q . j by PARTFUN1:def 6;

A10: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

i in dom w1 by A1, A4, FINSEQ_1:def 3;

then w1 . j = w1 /. i by A8, PARTFUN1:def 6

.= q2 by A2, A1, A10, FUNCT_7:36 ;

hence w1 . j <= w2 . j by A8, A9, VALUED_1:11; :: thesis: verum

suppose A11:
j <> i
; :: thesis: w1 . j <= w2 . j

A12: dom (0* n) =
Seg (len (0* n))
by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom q = Seg n by A6, FINSEQ_1:def 3;

then q /. j = q . j by A7, PARTFUN1:def 6;

then A13: w2 . j = (q /. j) ^2 by VALUED_1:11;

j in dom w1 by A4, A7, FINSEQ_1:def 3;

then w1 . j = w1 /. j by PARTFUN1:def 6

.= (0* n) /. j by A7, A11, A12, FUNCT_7:37

.= (n |-> 0) . j by A7, A12, PARTFUN1:def 6

.= 0 ;

hence w1 . j <= w2 . j by A13, XREAL_1:63; :: thesis: verum

end;.= Seg n by CARD_1:def 7 ;

dom q = Seg n by A6, FINSEQ_1:def 3;

then q /. j = q . j by A7, PARTFUN1:def 6;

then A13: w2 . j = (q /. j) ^2 by VALUED_1:11;

j in dom w1 by A4, A7, FINSEQ_1:def 3;

then w1 . j = w1 /. j by PARTFUN1:def 6

.= (0* n) /. j by A7, A11, A12, FUNCT_7:37

.= (n |-> 0) . j by A7, A12, PARTFUN1:def 6

.= 0 ;

hence w1 . j <= w2 . j by A13, XREAL_1:63; :: thesis: verum

then ( 0 <= (p /. i) ^2 & (p /. i) ^2 <= (sqrt (Sum (sqr q))) ^2 ) by A5, A3, SQUARE_1:def 2, XREAL_1:63;

then sqrt ((p /. i) ^2) <= sqrt ((sqrt (Sum (sqr q))) ^2) by SQUARE_1:26;

then |.|.(p /. i).|.| <= sqrt ((sqrt (Sum (sqr q))) ^2) by COMPLEX1:72;

then ( 0 <= |.q.| & |.(p /. i).| <= |.(sqrt (Sum (sqr q))).| ) by COMPLEX1:72;

hence |.(p /. i).| <= |.q.| by ABSVALUE:def 1; :: thesis: verum