let n be Nat; :: thesis: for C being non empty connected compact non horizontal non vertical Subset of () holds E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1)
let C be non empty connected compact non horizontal non vertical Subset of (); :: thesis: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1)
set f = Cage (C,n);
set G = Gauge (C,n);
consider j being Nat such that
A1: 1 <= j and
A2: j <= width (Gauge (C,n)) and
A3: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25;
A4: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set k = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n));
A6: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A7: ( (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) ) by ;
then A8: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) by PARTFUN1:def 6;
A9: now :: thesis: not (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n))
A10: 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2;
A11: 1 in dom (Cage (C,n)) by ;
assume (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; :: thesis: contradiction
then (Cage (C,n)) /. 1 = E-max (L~ (Cage (C,n))) by ;
then (Cage (C,n)) . 1 = E-max (L~ (Cage (C,n))) by ;
hence contradiction by A11, A10, FINSEQ_4:24; :: thesis: verum
end;
(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by ;
then A12: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * ((len (Gauge (C,n))),j) by JORDAN1H:44;
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by ;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by ;
then A13: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A14: 1 <= len (Gauge (C,n)) by ;
then A15: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by ;
( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by ;
then A16: [(len (Gauge (C,n))),((j -' 1) + 1)] in Indices (Gauge (C,n)) by ;
set p = E-max C;
A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A18: 1 <= ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;
then A19: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by ;
A20: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by ;
then consider ki, kj being Nat such that
A21: [ki,kj] in Indices (Gauge (C,n)) and
A22: (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by ;
A23: ( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by ;
A24: 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2;
then A25: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by ;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by ;
then A26: ki = len (Gauge (C,n)) by ;
A27: ( kj <= width (Gauge (C,n)) & 1 <= ki ) by ;
[(len (Gauge (C,n))),j] in Indices (GoB (Cage (C,n))) by ;
then |.((len (Gauge (C,n))) - ki).| + |.(j - kj).| = 1 by ;
then A28: 0 + |.(j - kj).| = 1 by ;
2 <= len (Cage (C,n)) by ;
then (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in E-most (L~ (Cage (C,n))) by ;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 >= ((Gauge (C,n)) * (ki,kj)) `2 by ;
then j >= kj by ;
then j = kj + 1 by ;
then kj = j - 1 ;
then A29: kj = j -' 1 by ;
then A30: 1 <= j -' 1 by ;
A31: j -' 1 <= width (Gauge (C,n)) by ;
(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),((j -' 1) + 1)) by ;
then A32: right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by ;
A33: now :: thesis: E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n)))
j -' 1 <= len (Gauge (C,n)) by ;
then A34: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 = E-bound C by ;
j <= len (Gauge (C,n)) by ;
then A35: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by ;
assume A36: not E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; :: thesis: contradiction
A37: 1 < len (Gauge (C,n)) by ;
then A38: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49;
A39: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:50;
then A40: ( ((Gauge (C,n)) * (1,j)) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 & ((Gauge (C,n)) * (1,(j -' 1))) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by ;
j -' 1 < j by ;
then j -' 1 < width (Gauge (C,n)) by ;
then LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) c= cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by ;
then not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) by ;
then A41: not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j))) by ;
(E-max C) `1 = E-bound C by EUCLID:52;
then A42: ( (E-max C) `2 > ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 or () `2 < ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by ;
per cases ) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 or () `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 ) by A1, A2, A5, A30, A31, A42, A40, GOBOARD5:1;
suppose A43: (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 ; :: thesis: contradiction
A44: ( 1 <= j -' 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by ;
cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) meets C by ;
then (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1))) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object such that
A45: c in (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1))) /\ C by XBOOLE_0:def 1;
reconsider c = c as Element of () by A45;
A46: ( 1 <= (len (Gauge (C,n))) -' 1 & ((len (Gauge (C,n))) -' 1) + 1 <= len (Gauge (C,n)) ) by ;
A47: c in cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by ;
then A48: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 <= c `1 by ;
A49: c in C by ;
then c `1 <= E-bound C by PSCOMP_1:24;
then c in E-most C by ;
then A50: c `2 <= () `2 by PSCOMP_1:47;
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 <= c `2 by ;
then ((Gauge (C,n)) * (1,(j -' 1))) `2 <= c `2 by ;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 <= c `2 by ;
hence contradiction by A43, A50, XXREAL_0:2; :: thesis: verum
end;
suppose A51: (E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 ; :: thesis: contradiction
east_halfline () meets L~ (Cage (C,n)) by ;
then consider r being object such that
A52: r in east_halfline () and
A53: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of () by A52;
r in () /\ (L~ (Cage (C,n))) by ;
then r `1 = E-bound (L~ (Cage (C,n))) by ;
then r in E-most (L~ (Cage (C,n))) by ;
then (E-max (L~ (Cage (C,n)))) `2 >= r `2 by PSCOMP_1:47;
hence contradiction by A3, A51, A52, TOPREAL1:def 11; :: thesis: verum
end;
end;
end;
GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by ;
hence E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by ; :: thesis: verum