let j be Nat; for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds
(h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
let G be Matrix of (TOP-REAL 2); ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G implies (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } )
assume that
A1:
( G is V3() & G is Y_equal-in-column )
and
A2:
G is Y_increasing-in-line
and
A3:
j + 1 <= width G
; (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
len G <> 0
by A1, MATRIX_0:def 10;
then A4:
1 <= len G
by NAT_1:14;
A5:
j < width G
by A3, NAT_1:13;
thus
(h_strip (G,j)) /\ (h_strip (G,(j + 1))) c= { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
XBOOLE_0:def 10 { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= (h_strip (G,j)) /\ (h_strip (G,(j + 1)))proof
let x be
object ;
TARSKI:def 3 ( not x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) or x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } )
assume A6:
x in (h_strip (G,j)) /\ (h_strip (G,(j + 1)))
;
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
then A7:
x in h_strip (
G,
j)
by XBOOLE_0:def 4;
A8:
x in h_strip (
G,
(j + 1))
by A6, XBOOLE_0:def 4;
reconsider p =
x as
Point of
(TOP-REAL 2) by A6;
per cases
( ( j = 0 & j + 1 = width G ) or ( j = 0 & j + 1 <> width G ) or ( j <> 0 & j + 1 = width G ) or ( j <> 0 & j + 1 <> width G ) )
;
suppose that A9:
j = 0
and A10:
j + 1
= width G
;
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
h_strip (
G,
j)
= { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 }
by A1, A4, A9, Th7;
then consider r1,
s1 being
Real such that A11:
x = |[r1,s1]|
and A12:
s1 <= (G * (1,1)) `2
by A7;
h_strip (
G,
(width G))
= { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s }
by A1, A4, Th6;
then consider r2,
s2 being
Real such that A13:
x = |[r2,s2]|
and A14:
(G * (1,(j + 1))) `2 <= s2
by A8, A10;
s1 =
|[r2,s2]| `2
by A11, A13, EUCLID:52
.=
s2
by EUCLID:52
;
then
(G * (1,(j + 1))) `2 = s1
by A9, A12, A14, XXREAL_0:1;
then
(G * (1,(j + 1))) `2 = p `2
by A11, EUCLID:52;
hence
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
;
verum end; suppose that A15:
j = 0
and A16:
j + 1
<> width G
;
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
h_strip (
G,
j)
= { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 }
by A1, A4, A15, Th7;
then consider r1,
s1 being
Real such that A17:
x = |[r1,s1]|
and A18:
s1 <= (G * (1,1)) `2
by A7;
j + 1
< width G
by A3, A16, XXREAL_0:1;
then
h_strip (
G,
(j + 1))
= { |[r,s]| where r, s is Real : ( (G * (1,(0 + 1))) `2 <= s & s <= (G * (1,((0 + 1) + 1))) `2 ) }
by A1, A4, A15, Th5;
then consider r2,
s2 being
Real such that A19:
x = |[r2,s2]|
and A20:
(G * (1,1)) `2 <= s2
and
s2 <= (G * (1,(1 + 1))) `2
by A8;
s1 =
|[r2,s2]| `2
by A17, A19, EUCLID:52
.=
s2
by EUCLID:52
;
then
(G * (1,1)) `2 = s1
by A18, A20, XXREAL_0:1;
then
(G * (1,1)) `2 = p `2
by A17, EUCLID:52;
hence
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
by A15;
verum end; suppose that A21:
j <> 0
and A22:
j + 1
= width G
;
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } A23:
1
<= j
by A21, NAT_1:14;
h_strip (
G,
j)
= { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) }
by A1, A4, A23, Th5, A3, NAT_1:13;
then consider r1,
s1 being
Real such that A24:
x = |[r1,s1]|
and
(G * (1,j)) `2 <= s1
and A25:
s1 <= (G * (1,(j + 1))) `2
by A7;
h_strip (
G,
(width G))
= { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s }
by A1, A4, Th6;
then consider r2,
s2 being
Real such that A26:
x = |[r2,s2]|
and A27:
(G * (1,(j + 1))) `2 <= s2
by A8, A22;
s1 =
|[r2,s2]| `2
by A24, A26, EUCLID:52
.=
s2
by EUCLID:52
;
then
(G * (1,(j + 1))) `2 = s1
by A25, A27, XXREAL_0:1;
then
(G * (1,(j + 1))) `2 = p `2
by A24, EUCLID:52;
hence
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
;
verum end; suppose that A28:
j <> 0
and A29:
j + 1
<> width G
;
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } A30:
1
<= j
by A28, NAT_1:14;
h_strip (
G,
j)
= { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) }
by A1, A4, A30, Th5, A3, NAT_1:13;
then consider r1,
s1 being
Real such that A31:
x = |[r1,s1]|
and
(G * (1,j)) `2 <= s1
and A32:
s1 <= (G * (1,(j + 1))) `2
by A7;
A33:
1
<= j + 1
by NAT_1:11;
j + 1
< width G
by A3, A29, XXREAL_0:1;
then
h_strip (
G,
(j + 1))
= { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) }
by A1, A4, A33, Th5;
then consider r2,
s2 being
Real such that A34:
x = |[r2,s2]|
and A35:
(G * (1,(j + 1))) `2 <= s2
and
s2 <= (G * (1,((j + 1) + 1))) `2
by A8;
s1 =
|[r2,s2]| `2
by A31, A34, EUCLID:52
.=
s2
by EUCLID:52
;
then
(G * (1,(j + 1))) `2 = s1
by A32, A35, XXREAL_0:1;
then
(G * (1,(j + 1))) `2 = p `2
by A31, EUCLID:52;
hence
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
;
verum end; end;
end;
A36:
{ q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,j)
proof
let x be
object ;
TARSKI:def 3 ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,j) )
assume
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
;
x in h_strip (G,j)
then consider p being
Point of
(TOP-REAL 2) such that A37:
p = x
and A38:
p `2 = (G * (1,(j + 1))) `2
;
A39:
p = |[(p `1),(p `2)]|
by EUCLID:53;
per cases
( j = 0 or j >= 1 )
by NAT_1:14;
suppose A40:
j = 0
;
x in h_strip (G,j)then
h_strip (
G,
j)
= { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 }
by A1, A4, Th7;
hence
x in h_strip (
G,
j)
by A37, A38, A39, A40;
verum end; suppose A41:
j >= 1
;
x in h_strip (G,j)then A42:
h_strip (
G,
j)
= { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) }
by A1, A4, A5, Th5;
j < j + 1
by XREAL_1:29;
then
(G * (1,j)) `2 < p `2
by A2, A3, A4, A38, A41, Th4;
hence
x in h_strip (
G,
j)
by A37, A38, A39, A42;
verum end; end;
end;
{ q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,(j + 1))
proof
let x be
object ;
TARSKI:def 3 ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,(j + 1)) )
assume
x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
;
x in h_strip (G,(j + 1))
then consider p being
Point of
(TOP-REAL 2) such that A43:
p = x
and A44:
p `2 = (G * (1,(j + 1))) `2
;
A45:
p = |[(p `1),(p `2)]|
by EUCLID:53;
A46:
1
<= j + 1
by NAT_1:11;
per cases
( j + 1 = width G or j + 1 < width G )
by A3, XXREAL_0:1;
suppose A47:
j + 1
= width G
;
x in h_strip (G,(j + 1))then
h_strip (
G,
(j + 1))
= { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s }
by A1, A4, Th6;
hence
x in h_strip (
G,
(j + 1))
by A43, A44, A45, A47;
verum end; suppose A48:
j + 1
< width G
;
x in h_strip (G,(j + 1))then A49:
h_strip (
G,
(j + 1))
= { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) }
by A1, A4, A46, Th5;
A50:
j + 1
< (j + 1) + 1
by NAT_1:13;
(j + 1) + 1
<= width G
by A48, NAT_1:13;
then
p `2 < (G * (1,((j + 1) + 1))) `2
by A2, A4, A44, A46, A50, Th4;
hence
x in h_strip (
G,
(j + 1))
by A43, A44, A45, A49;
verum end; end;
end;
hence
{ q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= (h_strip (G,j)) /\ (h_strip (G,(j + 1)))
by A36, XBOOLE_1:19; verum