let p be Point of (TOP-REAL 2); for f being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate (f,p)) = L~ f
let f be circular FinSequence of (TOP-REAL 2); L~ (Rotate (f,p)) = L~ f
per cases
( not p in rng f or p in rng f )
;
suppose A1:
p in rng f
;
L~ (Rotate (f,p)) = L~ fset B =
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set A =
{ (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
A2:
{ (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
proof
A3:
p .. f <= len f
by A1, FINSEQ_4:21;
thus
{ (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
XBOOLE_0:def 10 { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } proof
A4:
1
<= p .. f
by A1, FINSEQ_4:21;
let x be
object ;
TARSKI:def 3 ( not x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } )
assume
x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
;
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
then consider i being
Nat such that A5:
x = LSeg (
(Rotate (f,p)),
i)
and A6:
1
<= i
and A7:
i + 1
<= len f
;
A8:
i < len f
by A7, NAT_1:13;
per cases
( i < len (f :- p) or i >= len (f :- p) )
;
suppose A9:
i < len (f :- p)
;
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } then
i < ((len f) - (p .. f)) + 1
by A1, FINSEQ_5:50;
then
i < ((len f) -' (p .. f)) + 1
by A3, XREAL_1:233;
then
i -' 1
< (len f) -' (p .. f)
by A6, NAT_D:54;
then
(i -' 1) + (p .. f) < len f
by NAT_D:53;
then A10:
((i -' 1) + (p .. f)) + 1
<= len f
by NAT_1:13;
1
+ 1
<= i + (p .. f)
by A6, A4, XREAL_1:7;
then
1
<= (i + (p .. f)) -' 1
by NAT_D:55;
then A11:
1
<= (i -' 1) + (p .. f)
by A6, NAT_D:38;
LSeg (
(Rotate (f,p)),
i)
= LSeg (
f,
((i -' 1) + (p .. f)))
by A1, A6, A9, Th24;
hence
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A5, A11, A10;
verum end; suppose A12:
i >= len (f :- p)
;
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } then
((len f) - (p .. f)) + 1
<= i
by A1, FINSEQ_5:50;
then
((len f) -' (p .. f)) + 1
<= i
by A3, XREAL_1:233;
then
(1 + (len f)) -' (p .. f) <= i
by A3, NAT_D:38;
then A13:
1
+ (len f) <= i + (p .. f)
by NAT_D:52;
then A14:
1
<= (i + (p .. f)) -' (len f)
by NAT_D:55;
(i + 1) + (p .. f) <= (len f) + (len f)
by A3, A7, XREAL_1:7;
then
(
len f <= (len f) + 1 &
((i + (p .. f)) + 1) -' (len f) <= len f )
by NAT_1:11, NAT_D:53;
then A15:
((i + (p .. f)) -' (len f)) + 1
<= len f
by A13, NAT_D:38, XXREAL_0:2;
LSeg (
(Rotate (f,p)),
i)
= LSeg (
f,
((i + (p .. f)) -' (len f)))
by A1, A8, A12, Th31;
hence
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A5, A14, A15;
verum end; end;
end;
let x be
object ;
TARSKI:def 3 ( not x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } )
assume
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
;
x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
then consider i being
Nat such that A16:
x = LSeg (
f,
i)
and A17:
1
<= i
and A18:
i + 1
<= len f
;
A19:
i < len f
by A18, NAT_1:13;
per cases
( p .. f <= i or i < p .. f )
;
suppose A20:
p .. f <= i
;
x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
i <= i + 1
by NAT_1:11;
then A21:
p .. f <= i + 1
by A20, XXREAL_0:2;
1
<= p .. f
by A1, FINSEQ_4:21;
then
i + 1
< (len f) + (p .. f)
by A19, XREAL_1:8;
then
(i + 1) -' (p .. f) < len f
by A21, NAT_D:54;
then
(i -' (p .. f)) + 1
< len f
by A20, NAT_D:38;
then A22:
((i -' (p .. f)) + 1) + 1
<= len f
by NAT_1:13;
1
+ (p .. f) <= i + 1
by A20, XREAL_1:6;
then
1
<= (i + 1) -' (p .. f)
by NAT_D:55;
then A23:
1
<= (i -' (p .. f)) + 1
by A20, NAT_D:38;
LSeg (
f,
i)
= LSeg (
(Rotate (f,p)),
((i -' (p .. f)) + 1))
by A1, A19, A20, Th25;
hence
x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A16, A23, A22;
verum end; suppose A24:
i < p .. f
;
x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } then
i + 1
<= p .. f
by NAT_1:13;
then
(i + 1) + (len f) <= (len f) + (p .. f)
by XREAL_1:6;
then A25:
((i + (len f)) + 1) -' (p .. f) <= len f
by NAT_D:53;
(
p .. f <= len f &
len f <= i + (len f) )
by A1, FINSEQ_4:21, NAT_1:11;
then A26:
((i + (len f)) -' (p .. f)) + 1
<= len f
by A25, NAT_D:38, XXREAL_0:2;
1
+ (p .. f) <= i + (len f)
by A3, A17, XREAL_1:7;
then A27:
1
<= (i + (len f)) -' (p .. f)
by NAT_D:55;
LSeg (
f,
i)
= LSeg (
(Rotate (f,p)),
((i + (len f)) -' (p .. f)))
by A1, A17, A24, Th32;
hence
x in { (LSeg ((Rotate (f,p)),i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A16, A27, A26;
verum end; end;
end;
len (Rotate (f,p)) = len f
by Th14;
hence
L~ (Rotate (f,p)) = L~ f
by A2;
verum end; end;