let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
let n be Nat; :: thesis: Lower_Seq (C,n) is_sequence_on Gauge (C,n)
consider j being Nat such that
A1: ( 1 <= j & j <= width (Gauge (C,n)) ) and
A2: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25;
set E1 = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1;
set i = len (Gauge (C,n));
A3: Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) by JORDAN1E:def 2
.= <*(E-max (L~ (Cage (C,n))))*> ^ ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by FINSEQ_5:def 2 ;
A4: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;
then A5: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) is_sequence_on Gauge (C,n) by JORDAN8:2;
A6: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1
proof
set en = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n));
let i1, j1, i2, j2 be Nat; :: thesis: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) implies |.(i2 - i1).| + |.(j2 - j1).| = 1 )
assume A7: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) ) ; :: thesis: |.(i2 - i1).| + |.(j2 - j1).| = 1
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by SPRECT_5:16;
then ( 1 <= ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 & ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) ) by NAT_1:11, NAT_1:13;
then A8: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by FINSEQ_3:25;
A9: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
A10: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:71;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:72, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:73, XXREAL_0:2;
then A11: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:74, XXREAL_0:2;
then A12: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by NAT_1:13;
A13: (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) > 0 by SPRECT_5:20, XREAL_1:50;
then A14: (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) >= 0 + 0 ;
A15: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by FINSEQ_4:21;
then A16: 1 < ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:13;
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A15, FINSEQ_6:90, SPRECT_2:43;
then A17: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_4:21;
now :: thesis: not (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
assume (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; :: thesis: contradiction
then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Cage (C,n)) by FINSEQ_6:179;
then len (Upper_Seq (C,n)) = len (Cage (C,n)) by JORDAN1E:8;
then (len (Cage (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1 by JORDAN1E:10;
hence contradiction by JORDAN1E:15; :: thesis: verum
end;
then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A17, XXREAL_0:1;
then ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;
then (1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:9;
then 1 <= len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A17, RFINSEQ:def 1;
then 1 in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by FINSEQ_3:25;
then ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1) by FINSEQ_5:27
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1) by A15, A9, A11, SPRECT_5:9
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + 1)
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + ((len (Cage (C,n))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + 1) by A13, XREAL_0:def 2
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))))
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) by A13, XREAL_0:def 2
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + (len (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + (len (Cage (C,n)))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A14, XREAL_0:def 2 ;
then A18: ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) by A9, A16, A12, FINSEQ_6:178;
( E-max (L~ (Cage (C,n))) = (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) & (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) ) by A15, FINSEQ_4:20, FINSEQ_5:38;
then |.(i1 - i2).| + |.(j1 - j2).| = 1 by A4, A7, A8, A18, GOBOARD1:def 9;
then |.(i1 - i2).| + |.(j2 - j1).| = 1 by UNIFORM1:11;
hence |.(i2 - i1).| + |.(j2 - j1).| = 1 by UNIFORM1:11; :: thesis: verum
end;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then 1 <= len (Gauge (C,n)) by XXREAL_0:2;
then [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A1, MATRIX_0:30;
hence Lower_Seq (C,n) is_sequence_on Gauge (C,n) by A5, A2, A6, A3, Th11; :: thesis: verum