let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is nodic & PairF f is Simple & f . 1 <> f . (len f) implies f is s.n.c. )
assume that
A1: f is nodic and
A2: PairF f is Simple and
A3: f . 1 <> f . (len f) ; :: thesis: f is s.n.c.
reconsider f1 = f as FinSequence of the carrier of (PGraph the carrier of (TOP-REAL 2)) ;
A4: (len f) -' 1 <= len f by NAT_D:44;
per cases ( (len f) -' 1 > 2 or (len f) -' 1 <= 2 ) ;
suppose A5: (len f) -' 1 > 2 ; :: thesis: f is s.n.c.
then A6: (len f) -' 1 > 1 by XXREAL_0:2;
then A7: 1 < len f by NAT_D:44;
len f >= 1 by A6, NAT_D:44;
then A8: f1 is_oriented_vertex_seq_of PairF f by Th7;
A9: 1 + 1 < len f by A5, NAT_D:44;
A10: (len f) -' 1 = (len f) - 1 by A6, NAT_D:39;
then A11: ((len f) -' 1) + 1 = len f ;
now :: thesis: not LSeg (f,1) meets LSeg (f,((len f) -' 1))
assume A12: LSeg (f,1) meets LSeg (f,((len f) -' 1)) ; :: thesis: contradiction
now :: thesis: ( ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} & ( f . 1 = f . ((len f) -' 1) or f . 1 = f . (((len f) -' 1) + 1) ) & contradiction ) or ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . (1 + 1))} & ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) & contradiction ) or ( LSeg (f,1) = LSeg (f,((len f) -' 1)) & contradiction ) )
per cases ( ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} & ( f . 1 = f . ((len f) -' 1) or f . 1 = f . (((len f) -' 1) + 1) ) ) or ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . (1 + 1))} & ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) ) or LSeg (f,1) = LSeg (f,((len f) -' 1)) ) by A1, A12;
case ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} & ( f . 1 = f . ((len f) -' 1) or f . 1 = f . (((len f) -' 1) + 1) ) ) ; :: thesis: contradiction
hence contradiction by A2, A3, A4, A6, A8, A10, Th1; :: thesis: verum
end;
case A13: ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . (1 + 1))} & ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) ) ; :: thesis: contradiction
now :: thesis: ( ( f . (1 + 1) = f . ((len f) -' 1) & contradiction ) or ( f . (1 + 1) = f . (((len f) -' 1) + 1) & contradiction ) )
per cases ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) by A13;
case f . (1 + 1) = f . ((len f) -' 1) ; :: thesis: contradiction
hence contradiction by A2, A4, A5, A8, Th1; :: thesis: verum
end;
case f . (1 + 1) = f . (((len f) -' 1) + 1) ; :: thesis: contradiction
hence contradiction by A2, A8, A9, A10, Th1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case LSeg (f,1) = LSeg (f,((len f) -' 1)) ; :: thesis: contradiction
then LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,((len f) -' 1)) by A9, TOPREAL1:def 3;
then A14: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by A6, A10, TOPREAL1:def 3;
A15: 1 + 1 < ((len f) -' 1) + 1 by A6, XREAL_1:6;
(len f) -' 1 < len f by A11, NAT_1:13;
then A16: f /. ((len f) -' 1) = f . ((len f) -' 1) by A6, FINSEQ_4:15;
1 < len f by A6, NAT_D:44;
then A17: f /. 1 = f . 1 by FINSEQ_4:15;
A18: ( f /. (1 + 1) = f . (1 + 1) & f /. (((len f) -' 1) + 1) = f . (((len f) -' 1) + 1) ) by A7, A9, A10, FINSEQ_4:15;
now :: thesis: ( ( f . 1 = f . ((len f) -' 1) & f . (1 + 1) = f . (((len f) -' 1) + 1) & contradiction ) or ( f . 1 = f . (((len f) -' 1) + 1) & f . (1 + 1) = f . ((len f) -' 1) & contradiction ) )
per cases ( ( f . 1 = f . ((len f) -' 1) & f . (1 + 1) = f . (((len f) -' 1) + 1) ) or ( f . 1 = f . (((len f) -' 1) + 1) & f . (1 + 1) = f . ((len f) -' 1) ) ) by A14, A17, A16, A18, SPPOL_1:8;
case ( f . 1 = f . ((len f) -' 1) & f . (1 + 1) = f . (((len f) -' 1) + 1) ) ; :: thesis: contradiction
hence contradiction by A2, A8, A10, A15, Th1; :: thesis: verum
end;
case ( f . 1 = f . (((len f) -' 1) + 1) & f . (1 + 1) = f . ((len f) -' 1) ) ; :: thesis: contradiction
hence contradiction by A3, A10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence f is s.n.c. by A1, A2, Th13, Th14; :: thesis: verum
end;
suppose A19: (len f) -' 1 <= 2 ; :: thesis: f is s.n.c.
for i, j being Nat st i + 1 < j holds
LSeg (f,i) misses LSeg (f,j)
proof
let i, j be Nat; :: thesis: ( i + 1 < j implies LSeg (f,i) misses LSeg (f,j) )
assume A20: i + 1 < j ; :: thesis: LSeg (f,i) misses LSeg (f,j)
per cases ( ( 1 <= i & j + 1 <= len f ) or 1 > i or j + 1 > len f ) ;
suppose A21: ( 1 <= i & j + 1 <= len f ) ; :: thesis: LSeg (f,i) misses LSeg (f,j)
then 1 < i + 1 by NAT_1:13;
then 1 + 1 < (i + 1) + 1 by XREAL_1:8;
then A22: (1 + 1) + 1 <= (i + 1) + 1 by NAT_1:13;
(i + 1) + 1 < j + 1 by A20, XREAL_1:6;
then (i + 1) + 1 < len f by A21, XXREAL_0:2;
then (1 + 1) + 1 < len f by A22, XXREAL_0:2;
then A23: ((1 + 1) + 1) - 1 < (len f) - 1 by XREAL_1:9;
then 1 < (len f) - 1 by XXREAL_0:2;
hence LSeg (f,i) misses LSeg (f,j) by A19, A23, NAT_D:39; :: thesis: verum
end;
suppose A24: ( 1 > i or j + 1 > len f ) ; :: thesis: LSeg (f,i) misses LSeg (f,j)
now :: thesis: ( ( 1 > i & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) or ( j + 1 > len f & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) )
per cases ( 1 > i or j + 1 > len f ) by A24;
case 1 > i ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}
then LSeg (f,i) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum
end;
case j + 1 > len f ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}
then LSeg (f,j) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum
end;
end;
end;
hence LSeg (f,i) misses LSeg (f,j) ; :: thesis: verum
end;
end;
end;
hence f is s.n.c. by TOPREAL1:def 7; :: thesis: verum
end;
end;