let p be Point of (TOP-REAL 2); :: thesis: 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); :: thesis: L~ (Rotate (f,p)) = L~ f
per cases ( not p in rng f or p in rng f ) ;
suppose not p in rng f ; :: thesis: L~ (Rotate (f,p)) = L~ f
hence L~ (Rotate (f,p)) = L~ f by FINSEQ_6:def 2; :: thesis: verum
end;
suppose A1: p in rng f ; :: thesis: L~ (Rotate (f,p)) = L~ f
set 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 ) } :: according to XBOOLE_0:def 10 :: thesis: { (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 ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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) ; :: thesis: 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; :: thesis: verum
end;
suppose A12: i >= len (f :- p) ; :: thesis: 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; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A24: i < p .. f ; :: thesis: 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; :: thesis: verum
end;
end;
end;
len (Rotate (f,p)) = len f by Th14;
hence L~ (Rotate (f,p)) = L~ f by A2; :: thesis: verum
end;
end;