let n be Nat; for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) 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 (TOP-REAL 2); 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 FINSEQ_4:19, FINSEQ_4:20;
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 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 A6, FINSEQ_3:31;
assume
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n))
;
contradictionthen
(Cage (C,n)) /. 1
= E-max (L~ (Cage (C,n)))
by A8, FINSEQ_6:def 1;
then
(Cage (C,n)) . 1
= E-max (L~ (Cage (C,n)))
by A11, PARTFUN1:def 6;
hence
contradiction
by A11, A10, FINSEQ_4:24;
verum end;
(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j)
by A3, A7, PARTFUN1:def 6;
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 A6, FINSEQ_4:21;
then
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n))
by A9, XXREAL_0:1;
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 A4, XXREAL_0:2;
then A15:
[(len (Gauge (C,n))),j] in Indices (Gauge (C,n))
by A1, A2, MATRIX_0:30;
( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge (C,n)) )
by A1, A2, XREAL_1:235;
then A16:
[(len (Gauge (C,n))),((j -' 1) + 1)] in Indices (Gauge (C,n))
by A14, MATRIX_0:30;
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 A13, FINSEQ_3:25;
A20:
((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n))
by A13, A18, FINSEQ_3:25;
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 A17, GOBOARD1:def 9;
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 A21, A22, JORDAN1H:44;
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 A8, A13, JORDAN1E:20;
then
((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1
by A3, A22, EUCLID:52;
then A26:
ki = len (Gauge (C,n))
by A21, A15, JORDAN1G:7;
A27:
( kj <= width (Gauge (C,n)) & 1 <= ki )
by A21, MATRIX_0:32;
[(len (Gauge (C,n))),j] in Indices (GoB (Cage (C,n)))
by A15, JORDAN1H:44;
then
|.((len (Gauge (C,n))) - ki).| + |.(j - kj).| = 1
by A6, A19, A12, A23, FINSEQ_4:20, GOBOARD5:12;
then A28:
0 + |.(j - kj).| = 1
by A26, ABSVALUE:2;
2 <= len (Cage (C,n))
by GOBOARD7:34, XXREAL_0:2;
then
(Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in E-most (L~ (Cage (C,n)))
by A25, A20, GOBOARD1:1, SPRECT_2:13;
then
((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 >= ((Gauge (C,n)) * (ki,kj)) `2
by A3, A22, PSCOMP_1:47;
then
j >= kj
by A1, A26, A27, GOBOARD5:4;
then
j = kj + 1
by A28, SEQM_3:41;
then
kj = j - 1
;
then A29:
kj = j -' 1
by A1, XREAL_1:233;
then A30:
1 <= j -' 1
by A21, MATRIX_0:32;
A31:
j -' 1 <= width (Gauge (C,n))
by A21, A29, MATRIX_0:32;
(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),((j -' 1) + 1))
by A1, A3, A8, XREAL_1:235;
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 A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13:28;
A33:
now 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 A31, JORDAN8:def 1;
then A34:
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 = E-bound C
by A30, JORDAN8:12;
j <= len (Gauge (C,n))
by A2, JORDAN8:def 1;
then A35:
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C
by A1, JORDAN8:12;
assume A36:
not
E-max C in right_cell (
(Cage (C,n)),
((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),
(Gauge (C,n)))
;
contradictionA37:
1
< len (Gauge (C,n))
by A4, XXREAL_0:2;
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 A1, A2, A30, A31, A38, GOBOARD5:1;
j -' 1
< j
by A30, NAT_D:51;
then
j -' 1
< width (Gauge (C,n))
by A2, XXREAL_0:2;
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 A30, A38, A39, GOBOARD5:19;
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 A32, A36;
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 A1, XREAL_1:235;
(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
(E-max C) `2 < ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 )
by A41, A34, A35, GOBOARD7:7;
per cases
( (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 or (E-max C) `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
;
contradictionA44:
( 1
<= j -' 1 &
(j -' 1) + 1
<= width (Gauge (C,n)) )
by A1, A2, A21, A29, MATRIX_0:32, XREAL_1:235;
cell (
(Gauge (C,n)),
((len (Gauge (C,n))) -' 1),
(j -' 1))
meets C
by A24, A13, A32, JORDAN9:31;
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
(TOP-REAL 2) by A45;
A46:
( 1
<= (len (Gauge (C,n))) -' 1 &
((len (Gauge (C,n))) -' 1) + 1
<= len (Gauge (C,n)) )
by A37, NAT_D:49, XREAL_1:235;
A47:
c in cell (
(Gauge (C,n)),
((len (Gauge (C,n))) -' 1),
(j -' 1))
by A45, XBOOLE_0:def 4;
then A48:
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 <= c `1
by A46, A44, JORDAN9:17;
A49:
c in C
by A45, XBOOLE_0:def 4;
then
c `1 <= E-bound C
by PSCOMP_1:24;
then
c in E-most C
by A34, A49, A48, SPRECT_2:13, XXREAL_0:1;
then A50:
c `2 <= (E-max C) `2
by PSCOMP_1:47;
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 <= c `2
by A47, A46, A44, JORDAN9:17;
then
((Gauge (C,n)) * (1,(j -' 1))) `2 <= c `2
by A30, A31, A38, A39, GOBOARD5:1;
then
((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 <= c `2
by A5, A30, A31, GOBOARD5:1;
hence
contradiction
by A43, A50, XXREAL_0:2;
verum end; suppose A51:
(E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2
;
contradiction
east_halfline (E-max C) meets L~ (Cage (C,n))
by JORDAN1A:52, SPRECT_1:14;
then consider r being
object such that A52:
r in east_halfline (E-max C)
and A53:
r in L~ (Cage (C,n))
by XBOOLE_0:3;
reconsider r =
r as
Element of
(TOP-REAL 2) by A52;
r in (east_halfline (E-max C)) /\ (L~ (Cage (C,n)))
by A52, A53, XBOOLE_0:def 4;
then
r `1 = E-bound (L~ (Cage (C,n)))
by JORDAN1A:83, PSCOMP_1:50;
then
r in E-most (L~ (Cage (C,n)))
by A53, SPRECT_2:13;
then
(E-max (L~ (Cage (C,n)))) `2 >= r `2
by PSCOMP_1:47;
hence
contradiction
by A3, A51, A52, TOPREAL1:def 11;
verum 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 A24, A13, A33, JORDAN1H:23;
hence
E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1)
by A6, Th5; verum