:: PENCIL_2 semantic presentation
begin
definition
let D be set ;
let p be FinSequence of D;
let i, j be Nat;
func Del (p,i,j) -> FinSequence of D equals :: PENCIL_2:def 1
(p | (i -' 1)) ^ (p /^ j);
coherence
(p | (i -' 1)) ^ (p /^ j) is FinSequence of D ;
end;
:: deftheorem defines Del PENCIL_2:def_1_:_
for D being set
for p being FinSequence of D
for i, j being Nat holds Del (p,i,j) = (p | (i -' 1)) ^ (p /^ j);
theorem Th1: :: PENCIL_2:1
for D being set
for p being FinSequence of D
for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p
proof
let D be set ; ::_thesis: for p being FinSequence of D
for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p
let p be FinSequence of D; ::_thesis: for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p
let i, j be Element of NAT ; ::_thesis: rng (Del (p,i,j)) c= rng p
A1: rng (p /^ j) c= rng p
proof
percases ( D is empty or not D is empty ) ;
supposeA2: D is empty ; ::_thesis: rng (p /^ j) c= rng p
then A3: ( j > len p implies rng (p /^ j) c= rng p ) ;
( j <= len p implies rng (p /^ j) c= rng p ) by A2;
hence rng (p /^ j) c= rng p by A3; ::_thesis: verum
end;
suppose not D is empty ; ::_thesis: rng (p /^ j) c= rng p
then reconsider E = D as non empty set ;
reconsider r = p as FinSequence of E ;
rng (r /^ j) c= rng r by FINSEQ_5:33;
hence rng (p /^ j) c= rng p ; ::_thesis: verum
end;
end;
end;
rng (p | (i -' 1)) = rng (p | (Seg (i -' 1))) by FINSEQ_1:def_15;
then A4: rng (p | (i -' 1)) c= rng p by RELAT_1:70;
rng ((p | (i -' 1)) ^ (p /^ j)) = (rng (p | (i -' 1))) \/ (rng (p /^ j)) by FINSEQ_1:31;
hence rng (Del (p,i,j)) c= rng p by A4, A1, XBOOLE_1:8; ::_thesis: verum
end;
theorem Th2: :: PENCIL_2:2
for D being set
for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p holds
len (Del (p,i,j)) = (((len p) - j) + i) - 1
proof
let D be set ; ::_thesis: for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p holds
len (Del (p,i,j)) = (((len p) - j) + i) - 1
let p be FinSequence of D; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p holds
len (Del (p,i,j)) = (((len p) - j) + i) - 1
let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p implies len (Del (p,i,j)) = (((len p) - j) + i) - 1 )
assume that
A1: i in dom p and
A2: j in dom p ; ::_thesis: len (Del (p,i,j)) = (((len p) - j) + i) - 1
A3: i <= len p by A1, FINSEQ_3:25;
1 <= i by A1, FINSEQ_3:25;
then A4: i - 1 >= 1 - 1 by XREAL_1:9;
A5: i -' 1 <= i by NAT_D:35;
A6: j <= len p by A2, FINSEQ_3:25;
thus len (Del (p,i,j)) = (len (p | (i -' 1))) + (len (p /^ j)) by FINSEQ_1:22
.= (i -' 1) + (len (p /^ j)) by A3, A5, FINSEQ_1:59, XXREAL_0:2
.= (i -' 1) + ((len p) - j) by A6, RFINSEQ:def_1
.= (i - 1) + ((len p) - j) by A4, XREAL_0:def_2
.= (((len p) - j) + i) - 1 ; ::_thesis: verum
end;
theorem Th3: :: PENCIL_2:3
for D being set
for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )
proof
let D be set ; ::_thesis: for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )
let p be FinSequence of D; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )
let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & len (Del (p,i,j)) = 0 implies ( i = 1 & j = len p ) )
assume that
A1: i in dom p and
A2: j in dom p and
A3: len (Del (p,i,j)) = 0 ; ::_thesis: ( i = 1 & j = len p )
A4: 1 <= i by A1, FINSEQ_3:25;
j <= len p by A2, FINSEQ_3:25;
then A5: (len p) - j >= 0 by XREAL_1:48;
A6: (((len p) - j) + i) - 1 = 0 by A1, A2, A3, Th2;
then (len p) - j = 1 - i ;
then 1 >= i by A5, XREAL_1:49;
hence i = 1 by A4, XXREAL_0:1; ::_thesis: j = len p
hence j = len p by A6; ::_thesis: verum
end;
theorem Th4: :: PENCIL_2:4
for D being set
for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds
(Del (p,i,j)) . k = p . k
proof
let D be set ; ::_thesis: for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds
(Del (p,i,j)) . k = p . k
let p be FinSequence of D; ::_thesis: for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds
(Del (p,i,j)) . k = p . k
let i, j, k be Element of NAT ; ::_thesis: ( i in dom p & 1 <= k & k <= i - 1 implies (Del (p,i,j)) . k = p . k )
assume that
A1: i in dom p and
A2: 1 <= k and
A3: k <= i - 1 ; ::_thesis: (Del (p,i,j)) . k = p . k
A4: i <= len p by A1, FINSEQ_3:25;
A5: k <= i -' 1 by A3, XREAL_0:def_2;
A6: i -' 1 <= i by NAT_D:35;
then len (p | (i -' 1)) = i -' 1 by A4, FINSEQ_1:59, XXREAL_0:2;
then A7: k in dom (p | (i -' 1)) by A2, A5, FINSEQ_3:25;
i -' 1 <= len p by A4, A6, XXREAL_0:2;
then k <= len p by A5, XXREAL_0:2;
then A8: k in dom p by A2, FINSEQ_3:25;
thus (Del (p,i,j)) . k = (p | (i -' 1)) . k by A7, FINSEQ_1:def_7
.= (p | (i -' 1)) /. k by A7, PARTFUN1:def_6
.= p /. k by A7, FINSEQ_4:70
.= p . k by A8, PARTFUN1:def_6 ; ::_thesis: verum
end;
theorem Th5: :: PENCIL_2:5
for p, q being FinSequence
for k being Element of NAT st (len p) + 1 <= k holds
(p ^ q) . k = q . (k - (len p))
proof
let p, q be FinSequence; ::_thesis: for k being Element of NAT st (len p) + 1 <= k holds
(p ^ q) . k = q . (k - (len p))
let k be Element of NAT ; ::_thesis: ( (len p) + 1 <= k implies (p ^ q) . k = q . (k - (len p)) )
assume A1: (len p) + 1 <= k ; ::_thesis: (p ^ q) . k = q . (k - (len p))
percases ( k <= (len p) + (len q) or not k <= (len p) + (len q) ) ;
suppose k <= (len p) + (len q) ; ::_thesis: (p ^ q) . k = q . (k - (len p))
hence (p ^ q) . k = q . (k - (len p)) by A1, FINSEQ_1:23; ::_thesis: verum
end;
supposeA2: not k <= (len p) + (len q) ; ::_thesis: (p ^ q) . k = q . (k - (len p))
then k - (len p) > len q by XREAL_1:20;
then A3: not k - (len p) in dom q by FINSEQ_3:25;
not k <= len (p ^ q) by A2, FINSEQ_1:22;
then not k in dom (p ^ q) by FINSEQ_3:25;
hence (p ^ q) . k = {} by FUNCT_1:def_2
.= q . (k - (len p)) by A3, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
theorem Th6: :: PENCIL_2:6
for D being set
for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
proof
let D be set ; ::_thesis: for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
let p be FinSequence of D; ::_thesis: for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
let i, j, k be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 implies (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) )
assume that
A1: i in dom p and
A2: j in dom p and
A3: i <= j and
A4: i <= k and
A5: k <= (((len p) - j) + i) - 1 ; ::_thesis: (Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
A6: i -' 1 <= i by NAT_D:35;
i -' 1 <= i by NAT_D:35;
then k >= i -' 1 by A4, XXREAL_0:2;
then k - (i -' 1) >= (i -' 1) - (i -' 1) by XREAL_1:9;
then A7: k - (i -' 1) = k -' (i -' 1) by XREAL_0:def_2;
A8: 1 <= i by A1, FINSEQ_3:25;
then A9: (i -' 1) + 1 <= k by A4, XREAL_1:235;
i - 1 >= 1 - 1 by A8, XREAL_1:9;
then A10: i -' 1 = i - 1 by XREAL_0:def_2;
j - i >= i - i by A3, XREAL_1:9;
then A11: j -' i = j - i by XREAL_0:def_2;
A12: j <= len p by A2, FINSEQ_3:25;
then A13: len (p /^ j) = (len p) - j by RFINSEQ:def_1;
k <= ((len p) - j) + (i - 1) by A5;
then A14: k - (i -' 1) <= (len p) - j by A10, XREAL_1:20;
1 <= k - (i -' 1) by A9, XREAL_1:19;
then A15: k - (i -' 1) in dom (p /^ j) by A7, A13, A14, FINSEQ_3:25;
i <= len p by A1, FINSEQ_3:25;
then len (p | (i -' 1)) = i -' 1 by A6, FINSEQ_1:59, XXREAL_0:2;
hence (Del (p,i,j)) . k = (p /^ j) . (k - (i -' 1)) by A9, Th5
.= p . (j + (k + (1 - i))) by A12, A10, A15, RFINSEQ:def_1
.= p . (((j -' i) + k) + 1) by A11 ;
::_thesis: verum
end;
scheme :: PENCIL_2:sch 1
FinSeqOneToOne{ F1() -> set , F2() -> set , F3() -> set , F4() -> FinSequence of F3(), P1[ set , set ] } :
ex g being one-to-one FinSequence of F3() st
( F1() = g . 1 & F2() = g . (len g) & rng g c= rng F4() & ( for j being Element of NAT st 1 <= j & j < len g holds
P1[g . j,g . (j + 1)] ) )
provided
A1: ( F1() = F4() . 1 & F2() = F4() . (len F4()) ) and
A2: for i being Element of NAT
for d1, d2 being set st 1 <= i & i < len F4() & d1 = F4() . i & d2 = F4() . (i + 1) holds
P1[d1,d2]
proof
defpred S1[ Nat] means ex f being FinSequence of F3() st
( len f = $1 & F1() = f . 1 & F2() = f . (len f) & rng f c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len f holds
P1[f . i,f . (i + 1)] ) );
for i being Element of NAT st 1 <= i & i < len F4() holds
P1[F4() . i,F4() . (i + 1)] by A2;
then A3: ex k being Nat st S1[k] by A1;
consider k being Nat such that
A4: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A3);
consider g being FinSequence of F3() such that
A5: len g = k and
A6: F1() = g . 1 and
A7: F2() = g . (len g) and
A8: rng g c= rng F4() and
A9: for i being Element of NAT st 1 <= i & i < len g holds
P1[g . i,g . (i + 1)] by A4;
now__::_thesis:_g_is_one-to-one
assume not g is one-to-one ; ::_thesis: contradiction
then consider x, y being set such that
A10: x in dom g and
A11: y in dom g and
A12: g . x = g . y and
A13: x <> y by FUNCT_1:def_4;
reconsider x = x, y = y as Element of NAT by A10, A11;
percases ( x < y or y < x ) by A13, XXREAL_0:1;
supposeA14: x < y ; ::_thesis: contradiction
set d = Del (g,(x + 1),y);
A15: 1 <= y by A11, FINSEQ_3:25;
A16: x + 1 >= 1 by NAT_1:11;
A17: y <= len g by A11, FINSEQ_3:25;
then A18: x < len g by A14, XXREAL_0:2;
then x + 1 <= len g by NAT_1:13;
then A19: x + 1 in dom g by A16, FINSEQ_3:25;
A20: x + 1 <= y by A14, NAT_1:13;
then A21: y - (x + 1) >= 0 by XREAL_1:48;
A22: ( rng (Del (g,(x + 1),y)) c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] ) )
proof
rng (Del (g,(x + 1),y)) c= rng g by Th1;
hence rng (Del (g,(x + 1),y)) c= rng F4() by A8, XBOOLE_1:1; ::_thesis: for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (Del (g,(x + 1),y)) implies P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] )
assume that
A23: 1 <= i and
A24: i < len (Del (g,(x + 1),y)) ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
percases ( i < x or i = x or i > x ) by XXREAL_0:1;
supposeA25: i < x ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
then i + 1 <= (x + 1) - 1 by NAT_1:13;
then A26: (Del (g,(x + 1),y)) . (i + 1) = g . (i + 1) by A19, Th4, NAT_1:11;
i <= (x + 1) - 1 by A25;
then A27: (Del (g,(x + 1),y)) . i = g . i by A19, A23, Th4;
i < len g by A18, A25, XXREAL_0:2;
hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A23, A27, A26; ::_thesis: verum
end;
supposeA28: i = x ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
now__::_thesis:_not_y_=_len_g
assume y = len g ; ::_thesis: contradiction
then x < (((len g) - (len g)) + (x + 1)) - 1 by A11, A19, A24, A28, Th2;
hence contradiction ; ::_thesis: verum
end;
then A29: y < len g by A17, XXREAL_0:1;
then A30: 0 < (len g) - y by XREAL_1:50;
then 0 < (len g) -' y by XREAL_0:def_2;
then 0 + 1 <= (len g) -' y by NAT_1:13;
then 1 - 1 <= ((len g) -' y) - 1 by XREAL_1:9;
then 0 <= ((len g) - y) - 1 by A30, XREAL_0:def_2;
then (i + 1) + 0 <= (i + 1) + (((len g) - y) - 1) by XREAL_1:7;
then (i + 1) + 0 <= ((i + 1) + ((len g) - y)) - 1 ;
then A31: (Del (g,(x + 1),y)) . (i + 1) = g . (((y -' (x + 1)) + (i + 1)) + 1) by A11, A20, A19, A28, Th6
.= g . (y + 1) by A20, A28, XREAL_1:235 ;
i <= (x + 1) - 1 by A28;
then (Del (g,(x + 1),y)) . i = g . y by A12, A19, A23, A28, Th4;
hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A15, A29, A31; ::_thesis: verum
end;
suppose i > x ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
then A32: x + 1 <= i by NAT_1:13;
A33: (len g) - y >= 0 by A17, XREAL_1:48;
i < (((len g) - y) + (x + 1)) - 1 by A11, A19, A24, Th2;
then A34: i < (((len g) -' y) + (x + 1)) - 1 by A33, XREAL_0:def_2;
then i + 1 <= ((len g) -' y) + x by NAT_1:13;
then i + 1 <= ((((len g) - y) + x) + 1) - 1 by A33, XREAL_0:def_2;
then A35: i + 1 <= (((len g) - y) + (x + 1)) - 1 ;
i < ((((len g) -' y) + x) + 1) - 1 by A34;
then i < ((len g) - y) + x by A33, XREAL_0:def_2;
then i - x < (((len g) - y) + x) - x by XREAL_1:9;
then (i - x) + y < ((len g) - y) + y by XREAL_1:8;
then (((y - x) - 1) + i) + 1 < len g ;
then A36: ((y -' (x + 1)) + i) + 1 < len g by A21, XREAL_0:def_2;
i <= i + 1 by NAT_1:11;
then x + 1 <= i + 1 by A32, XXREAL_0:2;
then A37: (Del (g,(x + 1),y)) . (i + 1) = g . (((y -' (x + 1)) + (i + 1)) + 1) by A11, A20, A19, A35, Th6
.= g . ((((y -' (x + 1)) + i) + 1) + 1) ;
i <= (((len g) - y) + (x + 1)) - 1 by A11, A19, A24, Th2;
then (Del (g,(x + 1),y)) . i = g . (((y -' (x + 1)) + i) + 1) by A11, A20, A19, A32, Th6;
hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A37, A36, NAT_1:11; ::_thesis: verum
end;
end;
end;
A38: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))
proof
percases ( len (Del (g,(x + 1),y)) <= x or len (Del (g,(x + 1),y)) > x ) ;
supposeA39: len (Del (g,(x + 1),y)) <= x ; ::_thesis: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))
now__::_thesis:_not_len_(Del_(g,(x_+_1),y))_=_0
assume len (Del (g,(x + 1),y)) = 0 ; ::_thesis: contradiction
then x + 1 = 0 + 1 by A11, A19, Th3;
hence contradiction by A10, FINSEQ_3:24; ::_thesis: verum
end;
then A40: 0 + 1 <= len (Del (g,(x + 1),y)) by NAT_1:13;
len (Del (g,(x + 1),y)) <= (x + 1) - 1 by A39;
then A41: (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) = g . (len (Del (g,(x + 1),y))) by A19, A40, Th4;
(((len g) - y) + (x + 1)) - 1 <= x by A11, A19, A39, Th2;
then ((((len g) - y) + x) + 1) - 1 <= x ;
then (len g) - y <= 0 by XREAL_1:29;
then len g <= y by XREAL_1:50;
then A42: len g = y by A17, XXREAL_0:1;
then x <= (((len g) - y) + (x + 1)) - 1 ;
hence F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) by A7, A11, A12, A19, A42, A41, Th2; ::_thesis: verum
end;
suppose len (Del (g,(x + 1),y)) > x ; ::_thesis: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))
then A43: x + 1 <= len (Del (g,(x + 1),y)) by NAT_1:13;
len (Del (g,(x + 1),y)) = (((len g) - y) + (x + 1)) - 1 by A11, A19, Th2;
hence (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) = g . (((y -' (x + 1)) + ((((len g) - y) + (x + 1)) - 1)) + 1) by A11, A20, A19, A43, Th6
.= g . (((y - (x + 1)) + ((x + 1) + (((len g) - y) - 1))) + 1) by A20, XREAL_1:233
.= F2() by A7 ;
::_thesis: verum
end;
end;
end;
1 <= (x + 1) - 1 by A10, FINSEQ_3:25;
then A44: F1() = (Del (g,(x + 1),y)) . 1 by A6, A19, Th4;
0 < - (- (y - x)) by A14, XREAL_1:50;
then - (y - x) < 0 ;
then (len g) + (- (y - x)) < (len g) + 0 by XREAL_1:8;
then (((len g) - y) + (x + 1)) - 1 < len g ;
then len (Del (g,(x + 1),y)) < len g by A11, A19, Th2;
hence contradiction by A4, A5, A44, A38, A22; ::_thesis: verum
end;
supposeA45: y < x ; ::_thesis: contradiction
set d = Del (g,(y + 1),x);
A46: 1 <= x by A10, FINSEQ_3:25;
A47: y + 1 >= 1 by NAT_1:11;
A48: x <= len g by A10, FINSEQ_3:25;
then A49: y < len g by A45, XXREAL_0:2;
then y + 1 <= len g by NAT_1:13;
then A50: y + 1 in dom g by A47, FINSEQ_3:25;
A51: y + 1 <= x by A45, NAT_1:13;
then A52: x - (y + 1) >= 0 by XREAL_1:48;
A53: ( rng (Del (g,(y + 1),x)) c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] ) )
proof
rng (Del (g,(y + 1),x)) c= rng g by Th1;
hence rng (Del (g,(y + 1),x)) c= rng F4() by A8, XBOOLE_1:1; ::_thesis: for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (Del (g,(y + 1),x)) implies P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] )
assume that
A54: 1 <= i and
A55: i < len (Del (g,(y + 1),x)) ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
percases ( i < y or i = y or i > y ) by XXREAL_0:1;
supposeA56: i < y ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
then i + 1 <= (y + 1) - 1 by NAT_1:13;
then A57: (Del (g,(y + 1),x)) . (i + 1) = g . (i + 1) by A50, Th4, NAT_1:11;
i <= (y + 1) - 1 by A56;
then A58: (Del (g,(y + 1),x)) . i = g . i by A50, A54, Th4;
i < len g by A49, A56, XXREAL_0:2;
hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A54, A58, A57; ::_thesis: verum
end;
supposeA59: i = y ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
now__::_thesis:_not_x_=_len_g
assume x = len g ; ::_thesis: contradiction
then y < (((len g) - (len g)) + (y + 1)) - 1 by A10, A50, A55, A59, Th2;
hence contradiction ; ::_thesis: verum
end;
then A60: x < len g by A48, XXREAL_0:1;
then A61: 0 < (len g) - x by XREAL_1:50;
then 0 < (len g) -' x by XREAL_0:def_2;
then 0 + 1 <= (len g) -' x by NAT_1:13;
then 1 - 1 <= ((len g) -' x) - 1 by XREAL_1:9;
then 0 <= ((len g) - x) - 1 by A61, XREAL_0:def_2;
then (i + 1) + 0 <= (i + 1) + (((len g) - x) - 1) by XREAL_1:7;
then (i + 1) + 0 <= ((i + 1) + ((len g) - x)) - 1 ;
then A62: (Del (g,(y + 1),x)) . (i + 1) = g . (((x -' (y + 1)) + (i + 1)) + 1) by A10, A51, A50, A59, Th6
.= g . (x + 1) by A51, A59, XREAL_1:235 ;
i <= (y + 1) - 1 by A59;
then (Del (g,(y + 1),x)) . i = g . x by A12, A50, A54, A59, Th4;
hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A46, A60, A62; ::_thesis: verum
end;
suppose i > y ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
then A63: y + 1 <= i by NAT_1:13;
A64: (len g) - x >= 0 by A48, XREAL_1:48;
i < (((len g) - x) + (y + 1)) - 1 by A10, A50, A55, Th2;
then A65: i < (((len g) -' x) + (y + 1)) - 1 by A64, XREAL_0:def_2;
then i + 1 <= ((len g) -' x) + y by NAT_1:13;
then i + 1 <= ((((len g) - x) + y) + 1) - 1 by A64, XREAL_0:def_2;
then A66: i + 1 <= (((len g) - x) + (y + 1)) - 1 ;
i < ((((len g) -' x) + y) + 1) - 1 by A65;
then i < ((len g) - x) + y by A64, XREAL_0:def_2;
then i - y < (((len g) - x) + y) - y by XREAL_1:9;
then (i - y) + x < ((len g) - x) + x by XREAL_1:8;
then (((x - y) - 1) + i) + 1 < len g ;
then A67: ((x -' (y + 1)) + i) + 1 < len g by A52, XREAL_0:def_2;
i <= i + 1 by NAT_1:11;
then y + 1 <= i + 1 by A63, XXREAL_0:2;
then A68: (Del (g,(y + 1),x)) . (i + 1) = g . (((x -' (y + 1)) + (i + 1)) + 1) by A10, A51, A50, A66, Th6
.= g . ((((x -' (y + 1)) + i) + 1) + 1) ;
i <= (((len g) - x) + (y + 1)) - 1 by A10, A50, A55, Th2;
then (Del (g,(y + 1),x)) . i = g . (((x -' (y + 1)) + i) + 1) by A10, A51, A50, A63, Th6;
hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A68, A67, NAT_1:11; ::_thesis: verum
end;
end;
end;
A69: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))
proof
percases ( len (Del (g,(y + 1),x)) <= y or len (Del (g,(y + 1),x)) > y ) ;
supposeA70: len (Del (g,(y + 1),x)) <= y ; ::_thesis: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))
now__::_thesis:_not_len_(Del_(g,(y_+_1),x))_=_0
assume len (Del (g,(y + 1),x)) = 0 ; ::_thesis: contradiction
then y + 1 = 0 + 1 by A10, A50, Th3;
hence contradiction by A11, FINSEQ_3:24; ::_thesis: verum
end;
then A71: 0 + 1 <= len (Del (g,(y + 1),x)) by NAT_1:13;
len (Del (g,(y + 1),x)) <= (y + 1) - 1 by A70;
then A72: (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) = g . (len (Del (g,(y + 1),x))) by A50, A71, Th4;
(((len g) - x) + (y + 1)) - 1 <= y by A10, A50, A70, Th2;
then ((((len g) - x) + y) + 1) - 1 <= y ;
then (len g) - x <= 0 by XREAL_1:29;
then len g <= x by XREAL_1:50;
then A73: len g = x by A48, XXREAL_0:1;
then y <= (((len g) - x) + (y + 1)) - 1 ;
hence F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) by A7, A10, A12, A50, A73, A72, Th2; ::_thesis: verum
end;
suppose len (Del (g,(y + 1),x)) > y ; ::_thesis: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))
then A74: y + 1 <= len (Del (g,(y + 1),x)) by NAT_1:13;
len (Del (g,(y + 1),x)) = (((len g) - x) + (y + 1)) - 1 by A10, A50, Th2;
hence (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) = g . (((x -' (y + 1)) + ((((len g) - x) + (y + 1)) - 1)) + 1) by A10, A51, A50, A74, Th6
.= g . (((x - (y + 1)) + ((y + 1) + (((len g) - x) - 1))) + 1) by A51, XREAL_1:233
.= F2() by A7 ;
::_thesis: verum
end;
end;
end;
1 <= (y + 1) - 1 by A11, FINSEQ_3:25;
then A75: F1() = (Del (g,(y + 1),x)) . 1 by A6, A50, Th4;
0 < - (- (x - y)) by A45, XREAL_1:50;
then - (x - y) < 0 ;
then (len g) + (- (x - y)) < (len g) + 0 by XREAL_1:8;
then (((len g) - x) + (y + 1)) - 1 < len g ;
then len (Del (g,(y + 1),x)) < len g by A10, A50, Th2;
hence contradiction by A4, A5, A75, A69, A53; ::_thesis: verum
end;
end;
end;
hence ex g being one-to-one FinSequence of F3() st
( F1() = g . 1 & F2() = g . (len g) & rng g c= rng F4() & ( for j being Element of NAT st 1 <= j & j < len g holds
P1[g . j,g . (j + 1)] ) ) by A6, A7, A8, A9; ::_thesis: verum
end;
begin
theorem Th7: :: PENCIL_2:7
for I being non empty set
for A being 1-sorted-yielding ManySortedSet of I
for L being ManySortedSubset of Carrier A
for i being Element of I
for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A
proof
let I be non empty set ; ::_thesis: for A being 1-sorted-yielding ManySortedSet of I
for L being ManySortedSubset of Carrier A
for i being Element of I
for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A
let A be 1-sorted-yielding ManySortedSet of I; ::_thesis: for L being ManySortedSubset of Carrier A
for i being Element of I
for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A
let L be ManySortedSubset of Carrier A; ::_thesis: for i being Element of I
for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A
let i be Element of I; ::_thesis: for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A
let S be Subset of (A . i); ::_thesis: L +* (i,S) is ManySortedSubset of Carrier A
A1: L c= Carrier A by PBOOLE:def_18;
A2: dom L = I by PARTFUN1:def_2;
L +* (i,S) c= Carrier A
proof
let a be set ; :: according to PBOOLE:def_2 ::_thesis: ( not a in I or (L +* (i,S)) . a c= (Carrier A) . a )
assume a in I ; ::_thesis: (L +* (i,S)) . a c= (Carrier A) . a
then reconsider b = a as Element of I ;
percases ( a = i or a <> i ) ;
supposeA3: a = i ; ::_thesis: (L +* (i,S)) . a c= (Carrier A) . a
then (L +* (i,S)) . b = S by A2, FUNCT_7:31;
then (L +* (i,S)) . b c= the carrier of (A . b) by A3;
hence (L +* (i,S)) . a c= (Carrier A) . a by YELLOW_6:2; ::_thesis: verum
end;
suppose a <> i ; ::_thesis: (L +* (i,S)) . a c= (Carrier A) . a
then (L +* (i,S)) . a = L . b by FUNCT_7:32;
hence (L +* (i,S)) . a c= (Carrier A) . a by A1, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
hence L +* (i,S) is ManySortedSubset of Carrier A by PBOOLE:def_18; ::_thesis: verum
end;
definition
let I be non empty set ;
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I;
mode Segre-Coset of A -> Subset of (Segre_Product A) means :Def2: :: PENCIL_2:def 2
ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( it = product L & L . (indx L) = [#] (A . (indx L)) );
existence
ex b1 being Subset of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b1 = product L & L . (indx L) = [#] (A . (indx L)) )
proof
set L = the non trivial-yielding Segre-like ManySortedSubset of Carrier A;
reconsider C = the non trivial-yielding Segre-like ManySortedSubset of Carrier A +* ((indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A),([#] (A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A)))) as ManySortedSubset of Carrier A by Th7;
A1: dom (Carrier A) = I by PARTFUN1:def_2;
dom A = I by PARTFUN1:def_2;
then A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) in rng A by FUNCT_1:3;
then A2: not A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) is trivial by PENCIL_1:def_17;
then reconsider C = C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:27;
C c= Carrier A by PBOOLE:def_18;
then A3: for a being set st a in I holds
C . a c= (Carrier A) . a by PBOOLE:def_2;
dom C = I by PARTFUN1:def_2;
then reconsider P = product C as Subset of (Segre_Product A) by A1, A3, CARD_3:27;
take P ; ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( P = product L & L . (indx L) = [#] (A . (indx L)) )
dom the non trivial-yielding Segre-like ManySortedSubset of Carrier A = I by PARTFUN1:def_2;
then A4: C . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) = [#] (A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A)) by FUNCT_7:31;
then indx C = indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A by A2, PENCIL_1:def_21;
hence ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( P = product L & L . (indx L) = [#] (A . (indx L)) ) by A4; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Segre-Coset PENCIL_2:def_2_:_
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for b3 being Subset of (Segre_Product A) holds
( b3 is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b3 = product L & L . (indx L) = [#] (A . (indx L)) ) );
theorem Th8: :: PENCIL_2:8
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds
B1 = B2
proof
let I be non empty set ; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds
B1 = B2
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds
B1 = B2
let B1, B2 be Segre-Coset of A; ::_thesis: ( 2 c= card (B1 /\ B2) implies B1 = B2 )
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A1: B1 = product L1 and
A2: L1 . (indx L1) = [#] (A . (indx L1)) by Def2;
consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3: B2 = product L2 and
A4: L2 . (indx L2) = [#] (A . (indx L2)) by Def2;
assume A5: 2 c= card (B1 /\ B2) ; ::_thesis: B1 = B2
then A6: indx L1 = indx L2 by A1, A3, PENCIL_1:26;
A7: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
L1_._i_=_L2_._i
let i be set ; ::_thesis: ( i in I implies L1 . b1 = L2 . b1 )
assume i in I ; ::_thesis: L1 . b1 = L2 . b1
percases ( i <> indx L1 or i = indx L1 ) ;
suppose i <> indx L1 ; ::_thesis: L1 . b1 = L2 . b1
hence L1 . i = L2 . i by A5, A1, A3, PENCIL_1:26; ::_thesis: verum
end;
suppose i = indx L1 ; ::_thesis: L1 . b1 = L2 . b1
hence L1 . i = L2 . i by A2, A4, A6; ::_thesis: verum
end;
end;
end;
A8: dom L2 = I by PARTFUN1:def_2;
dom L1 = I by PARTFUN1:def_2;
hence B1 = B2 by A1, A3, A8, A7, FUNCT_1:2; ::_thesis: verum
end;
definition
let S be TopStruct ;
let X, Y be Subset of S;
predX,Y are_joinable means :Def3: :: PENCIL_2:def 3
ex f being FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) );
end;
:: deftheorem Def3 defines are_joinable PENCIL_2:def_3_:_
for S being TopStruct
for X, Y being Subset of S holds
( X,Y are_joinable iff ex f being FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) ) );
theorem :: PENCIL_2:9
for S being TopStruct
for X, Y being Subset of S st X,Y are_joinable holds
ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
proof
defpred S1[ set , set ] means 2 c= card ($1 /\ $2);
let S be TopStruct ; ::_thesis: for X, Y being Subset of S st X,Y are_joinable holds
ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
let X, Y be Subset of S; ::_thesis: ( X,Y are_joinable implies ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) ) )
assume X,Y are_joinable ; ::_thesis: ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
then consider f being FinSequence of bool the carrier of S such that
A1: ( X = f . 1 & Y = f . (len f) ) and
A2: for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) and
A3: for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by Def3;
A4: for i being Element of NAT
for d1, d2 being set st 1 <= i & i < len f & d1 = f . i & d2 = f . (i + 1) holds
S1[d1,d2] by A3;
consider g being one-to-one FinSequence of bool the carrier of S such that
A5: ( X = g . 1 & Y = g . (len g) ) and
A6: rng g c= rng f and
A7: for i being Element of NAT st 1 <= i & i < len g holds
S1[g . i,g . (i + 1)] from PENCIL_2:sch_1(A1, A4);
take g ; ::_thesis: ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1))) ) )
thus ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1))) ) ) by A2, A5, A6, A7; ::_thesis: verum
end;
theorem Th10: :: PENCIL_2:10
for S being TopStruct
for X being Subset of S st X is closed_under_lines & X is strong holds
X,X are_joinable
proof
let S be TopStruct ; ::_thesis: for X being Subset of S st X is closed_under_lines & X is strong holds
X,X are_joinable
let X be Subset of S; ::_thesis: ( X is closed_under_lines & X is strong implies X,X are_joinable )
assume A1: ( X is closed_under_lines & X is strong ) ; ::_thesis: X,X are_joinable
reconsider f = <*X*> as FinSequence of bool the carrier of S ;
take f ; :: according to PENCIL_2:def_3 ::_thesis: ( X = f . 1 & X = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
thus X = f . 1 by FINSEQ_1:40; ::_thesis: ( X = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
len f = 1 by FINSEQ_1:40;
hence X = f . (len f) by FINSEQ_1:40; ::_thesis: ( ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
thus for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1)))
proof
let W be Subset of S; ::_thesis: ( W in rng f implies ( W is closed_under_lines & W is strong ) )
assume W in rng f ; ::_thesis: ( W is closed_under_lines & W is strong )
then W in {X} by FINSEQ_1:38;
hence ( W is closed_under_lines & W is strong ) by A1, TARSKI:def_1; ::_thesis: verum
end;
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies 2 c= card ((f . i) /\ (f . (i + 1))) )
assume that
A2: 1 <= i and
A3: i < len f ; ::_thesis: 2 c= card ((f . i) /\ (f . (i + 1)))
thus 2 c= card ((f . i) /\ (f . (i + 1))) by A2, A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th11: :: PENCIL_2:11
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds
for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds
for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds
for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )
let X, Y be Subset of (Segre_Product A); ::_thesis: ( not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable implies for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) ) )
assume that
A1: ( not X is trivial & X is closed_under_lines & X is strong ) and
A2: ( not Y is trivial & Y is closed_under_lines & Y is strong ) and
A3: X,Y are_joinable ; ::_thesis: for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )
set B = bool the carrier of (Segre_Product A);
consider f being FinSequence of bool the carrier of (Segre_Product A) such that
A4: X = f . 1 and
A5: Y = f . (len f) and
A6: for W being Subset of (Segre_Product A) st W in rng f holds
( W is closed_under_lines & W is strong ) and
A7: for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by A3, Def3;
len f in dom f by A2, A5, FUNCT_1:def_2;
then A8: 1 <= len f by FINSEQ_3:25;
consider B0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A9: X = product B0 and
for C being Subset of (A . (indx B0)) st C = B0 . (indx B0) holds
( C is strong & C is closed_under_lines ) by A1, PENCIL_1:29;
let X1, Y1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( X = product X1 & Y = product Y1 implies ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) ) )
assume that
A10: X = product X1 and
A11: Y = product Y1 ; ::_thesis: ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )
defpred S1[ Element of NAT ] means for H being non trivial-yielding Segre-like ManySortedSubset of Carrier A st f . $1 = product H holds
( indx X1 = indx H & ( for i being set st i <> indx X1 holds
X1 . i = H . i ) );
A12: B0 = X1 by A10, A9, PUA2MSS1:2;
A13: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] )
assume that
A14: 1 <= j and
A15: j < len f ; ::_thesis: ( not S1[j] or S1[j + 1] )
j in dom f by A14, A15, FINSEQ_3:25;
then A16: f . j in rng f by FUNCT_1:3;
A17: 1 <= j + 1 by NAT_1:11;
j + 1 <= len f by A15, NAT_1:13;
then j + 1 in dom f by A17, FINSEQ_3:25;
then f . (j + 1) in rng f by FUNCT_1:3;
then reconsider fj = f . j, fj1 = f . (j + 1) as Subset of (Segre_Product A) by A16;
A18: card (fj /\ fj1) c= card fj by CARD_1:11, XBOOLE_1:17;
A19: 2 c= card (fj /\ fj1) by A7, A14, A15;
2 c= card (fj /\ fj1) by A7, A14, A15;
then 2 c= card fj by A18, XBOOLE_1:1;
then ( not fj is trivial & fj is closed_under_lines & fj is strong ) by A6, A16, PENCIL_1:4;
then consider B1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A20: fj = product B1 and
for C being Subset of (A . (indx B1)) st C = B1 . (indx B1) holds
( C is strong & C is closed_under_lines ) by PENCIL_1:29;
assume A21: S1[j] ; ::_thesis: S1[j + 1]
then A22: indx B0 = indx B1 by A12, A20;
now__::_thesis:_for_H_being_non_trivial-yielding_Segre-like_ManySortedSubset_of_Carrier_A_st_f_._(j_+_1)_=_product_H_holds_
(_indx_X1_=_indx_H_&_(_for_i_being_set_st_i_<>_indx_X1_holds_
X1_._i_=_H_._i_)_)
let H be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( f . (j + 1) = product H implies ( indx X1 = indx H & ( for i being set st i <> indx X1 holds
X1 . i = H . i ) ) )
assume A23: f . (j + 1) = product H ; ::_thesis: ( indx X1 = indx H & ( for i being set st i <> indx X1 holds
X1 . i = H . i ) )
hence indx X1 = indx H by A12, A20, A22, A19, PENCIL_1:26; ::_thesis: for i being set st i <> indx X1 holds
X1 . i = H . i
thus for i being set st i <> indx X1 holds
X1 . i = H . i ::_thesis: verum
proof
let i be set ; ::_thesis: ( i <> indx X1 implies X1 . i = H . i )
assume A24: i <> indx X1 ; ::_thesis: X1 . i = H . i
then A25: i <> indx B1 by A21, A20;
thus X1 . i = B1 . i by A21, A20, A24
.= H . i by A20, A19, A23, A25, PENCIL_1:26 ; ::_thesis: verum
end;
end;
hence S1[j + 1] ; ::_thesis: verum
end;
A26: S1[1] by A10, A4, PUA2MSS1:2;
for i being Element of NAT st 1 <= i & i <= len f holds
S1[i] from INT_1:sch_7(A26, A13);
hence ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) ) by A11, A5, A8; ::_thesis: verum
end;
begin
theorem :: PENCIL_2:12
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st f is bijective holds
f " is bijective
proof
let S be 1-sorted ; ::_thesis: for T being non empty 1-sorted
for f being Function of S,T st f is bijective holds
f " is bijective
let T be non empty 1-sorted ; ::_thesis: for f being Function of S,T st f is bijective holds
f " is bijective
let f be Function of S,T; ::_thesis: ( f is bijective implies f " is bijective )
assume A1: f is bijective ; ::_thesis: f " is bijective
then A2: rng f = [#] T by FUNCT_2:def_3;
then rng (f ") = [#] S by A1, TOPS_2:49;
then A3: f " is onto by FUNCT_2:def_3;
f " is one-to-one by A1, A2, TOPS_2:50;
hence f " is bijective by A3; ::_thesis: verum
end;
definition
let S, T be TopStruct ;
let f be Function of S,T;
attrf is isomorphic means :Def4: :: PENCIL_2:def 4
( f is bijective & f is open & f " is bijective & f " is open );
end;
:: deftheorem Def4 defines isomorphic PENCIL_2:def_4_:_
for S, T being TopStruct
for f being Function of S,T holds
( f is isomorphic iff ( f is bijective & f is open & f " is bijective & f " is open ) );
registration
let S be non empty TopStruct ;
cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty total quasi_total isomorphic for Element of bool [: the carrier of S, the carrier of S:];
existence
ex b1 being Function of S,S st b1 is isomorphic
proof
take f = id S; ::_thesis: f is isomorphic
f " = id S by TOPGRP_1:2;
hence f is isomorphic by Def4; ::_thesis: verum
end;
end;
definition
let S be non empty TopStruct ;
mode Collineation of S is isomorphic Function of S,S;
end;
definition
let S be non empty non void TopStruct ;
let f be Collineation of S;
let l be Block of S;
:: original: .:
redefine funcf .: l -> Block of S;
coherence
f .: l is Block of S
proof
l in the topology of S ;
then reconsider L = l as Subset of S ;
A1: L is open by PRE_TOPC:def_2;
f is open by Def4;
then f .: L is open by A1, T_0TOPSP:def_2;
hence f .: l is Block of S by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
definition
let S be non empty non void TopStruct ;
let f be Collineation of S;
let l be Block of S;
:: original: "
redefine funcf " l -> Block of S;
coherence
f " l is Block of S
proof
l in the topology of S ;
then reconsider L = l as Subset of S ;
A1: L is open by PRE_TOPC:def_2;
A2: f is bijective by Def4;
f " = f " by A2, TOPS_2:def_4;
then A3: (f ") .: L = f " L by A2, FUNCT_1:85;
f " is open by Def4;
then (f ") .: L is open by A1, T_0TOPSP:def_2;
hence f " l is Block of S by A3, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
theorem Th13: :: PENCIL_2:13
for S being non empty TopStruct
for f being Collineation of S holds f " is Collineation of S
proof
let S be non empty TopStruct ; ::_thesis: for f being Collineation of S holds f " is Collineation of S
let f be Collineation of S; ::_thesis: f " is Collineation of S
A1: ( f " is bijective & f " is open ) by Def4;
A2: f is bijective by Def4;
then A3: rng f = [#] S by FUNCT_2:def_3;
then (f ") " = f by A2, TOPS_2:51;
then A4: (f ") " is open by Def4;
(f ") " is bijective by A2, A3, TOPS_2:51;
hence f " is Collineation of S by A1, A4, Def4; ::_thesis: verum
end;
theorem Th14: :: PENCIL_2:14
for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f .: X is trivial
proof
let S be non empty TopStruct ; ::_thesis: for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f .: X is trivial
let f be Collineation of S; ::_thesis: for X being Subset of S st not X is trivial holds
not f .: X is trivial
let X be Subset of S; ::_thesis: ( not X is trivial implies not f .: X is trivial )
assume not X is trivial ; ::_thesis: not f .: X is trivial
then 2 c= card X by PENCIL_1:4;
then consider x, y being set such that
A1: x in X and
A2: y in X and
A3: x <> y by PENCIL_1:2;
A4: dom f = the carrier of S by FUNCT_2:def_1;
then A5: f . x in f .: X by A1, FUNCT_1:def_6;
A6: f . y in f .: X by A4, A2, FUNCT_1:def_6;
f is bijective by Def4;
then f . x <> f . y by A4, A1, A2, A3, FUNCT_1:def_4;
then 2 c= card (f .: X) by A5, A6, PENCIL_1:2;
hence not f .: X is trivial by PENCIL_1:4; ::_thesis: verum
end;
theorem :: PENCIL_2:15
for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f " X is trivial
proof
let S be non empty TopStruct ; ::_thesis: for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f " X is trivial
let f be Collineation of S; ::_thesis: for X being Subset of S st not X is trivial holds
not f " X is trivial
let X be Subset of S; ::_thesis: ( not X is trivial implies not f " X is trivial )
assume not X is trivial ; ::_thesis: not f " X is trivial
then 2 c= card X by PENCIL_1:4;
then consider x, y being set such that
A1: x in X and
A2: y in X and
A3: x <> y by PENCIL_1:2;
f is bijective by Def4;
then A4: rng f = the carrier of S by FUNCT_2:def_3;
then consider fx being set such that
A5: fx in dom f and
A6: f . fx = x by A1, FUNCT_1:def_3;
consider fy being set such that
A7: fy in dom f and
A8: f . fy = y by A4, A2, FUNCT_1:def_3;
A9: fy in f " X by A2, A7, A8, FUNCT_1:def_7;
fx in f " X by A1, A5, A6, FUNCT_1:def_7;
then 2 c= card (f " X) by A3, A6, A8, A9, PENCIL_1:2;
hence not f " X is trivial by PENCIL_1:4; ::_thesis: verum
end;
theorem Th16: :: PENCIL_2:16
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is strong holds
f .: X is strong
proof
let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S
for X being Subset of S st X is strong holds
f .: X is strong
let f be Collineation of S; ::_thesis: for X being Subset of S st X is strong holds
f .: X is strong
let X be Subset of S; ::_thesis: ( X is strong implies f .: X is strong )
assume A1: X is strong ; ::_thesis: f .: X is strong
thus f .: X is strong ::_thesis: verum
proof
let a, b be Point of S; :: according to PENCIL_1:def_3 ::_thesis: ( not a in f .: X or not b in f .: X or a,b are_collinear )
assume that
A2: a in f .: X and
A3: b in f .: X ; ::_thesis: a,b are_collinear
thus a,b are_collinear ::_thesis: verum
proof
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: a,b are_collinear
hence a,b are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
supposeA4: a <> b ; ::_thesis: a,b are_collinear
consider B being set such that
A5: B in dom f and
A6: B in X and
A7: b = f . B by A3, FUNCT_1:def_6;
consider A being set such that
A8: A in dom f and
A9: A in X and
A10: a = f . A by A2, FUNCT_1:def_6;
reconsider A = A, B = B as Point of S by A8, A5;
A,B are_collinear by A1, A9, A6, PENCIL_1:def_3;
then consider l being Block of S such that
A11: {A,B} c= l by A4, A10, A7, PENCIL_1:def_1;
B in l by A11, ZFMISC_1:32;
then A12: b in f .: l by A5, A7, FUNCT_1:def_6;
A in l by A11, ZFMISC_1:32;
then a in f .: l by A8, A10, FUNCT_1:def_6;
then {a,b} c= f .: l by A12, ZFMISC_1:32;
hence a,b are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: PENCIL_2:17
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is strong holds
f " X is strong
proof
let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S
for X being Subset of S st X is strong holds
f " X is strong
let f be Collineation of S; ::_thesis: for X being Subset of S st X is strong holds
f " X is strong
reconsider g = f " as Collineation of S by Th13;
let X be Subset of S; ::_thesis: ( X is strong implies f " X is strong )
assume X is strong ; ::_thesis: f " X is strong
then A1: g .: X is strong by Th16;
A2: f is bijective by Def4;
then rng f = [#] S by FUNCT_2:def_3;
hence f " X is strong by A2, A1, TOPS_2:55; ::_thesis: verum
end;
theorem Th18: :: PENCIL_2:18
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f .: X is closed_under_lines
proof
let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f .: X is closed_under_lines
let f be Collineation of S; ::_thesis: for X being Subset of S st X is closed_under_lines holds
f .: X is closed_under_lines
let X be Subset of S; ::_thesis: ( X is closed_under_lines implies f .: X is closed_under_lines )
assume A1: X is closed_under_lines ; ::_thesis: f .: X is closed_under_lines
thus f .: X is closed_under_lines ::_thesis: verum
proof
let l be Block of S; :: according to PENCIL_1:def_2 ::_thesis: ( not 2 c= card (l /\ (f .: X)) or l c= f .: X )
assume 2 c= card (l /\ (f .: X)) ; ::_thesis: l c= f .: X
then consider a, b being set such that
A2: a in l /\ (f .: X) and
A3: b in l /\ (f .: X) and
A4: a <> b by PENCIL_1:2;
b in f .: X by A3, XBOOLE_0:def_4;
then consider B being set such that
A5: B in dom f and
A6: B in X and
A7: b = f . B by FUNCT_1:def_6;
b in l by A3, XBOOLE_0:def_4;
then B in f " l by A5, A7, FUNCT_1:def_7;
then A8: B in (f " l) /\ X by A6, XBOOLE_0:def_4;
a in f .: X by A2, XBOOLE_0:def_4;
then consider A being set such that
A9: A in dom f and
A10: A in X and
A11: a = f . A by FUNCT_1:def_6;
a in l by A2, XBOOLE_0:def_4;
then A in f " l by A9, A11, FUNCT_1:def_7;
then A in (f " l) /\ X by A10, XBOOLE_0:def_4;
then 2 c= card ((f " l) /\ X) by A4, A11, A7, A8, PENCIL_1:2;
then f " l c= X by A1, PENCIL_1:def_2;
then A12: f .: (f " l) c= f .: X by RELAT_1:123;
f is bijective by Def4;
then A13: rng f = the carrier of S by FUNCT_2:def_3;
l in the topology of S ;
hence l c= f .: X by A13, A12, FUNCT_1:77; ::_thesis: verum
end;
end;
theorem :: PENCIL_2:19
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f " X is closed_under_lines
proof
let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f " X is closed_under_lines
let f be Collineation of S; ::_thesis: for X being Subset of S st X is closed_under_lines holds
f " X is closed_under_lines
reconsider g = f " as Collineation of S by Th13;
let X be Subset of S; ::_thesis: ( X is closed_under_lines implies f " X is closed_under_lines )
assume X is closed_under_lines ; ::_thesis: f " X is closed_under_lines
then A1: g .: X is closed_under_lines by Th18;
A2: f is bijective by Def4;
then rng f = [#] S by FUNCT_2:def_3;
hence f " X is closed_under_lines by A2, A1, TOPS_2:55; ::_thesis: verum
end;
theorem Th20: :: PENCIL_2:20
for S being non empty non void TopStruct
for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable
proof
let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable
let f be Collineation of S; ::_thesis: for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable
let X, Y be Subset of S; ::_thesis: ( not X is trivial & not Y is trivial & X,Y are_joinable implies f .: X,f .: Y are_joinable )
assume that
A1: not X is trivial and
A2: not Y is trivial and
A3: X,Y are_joinable ; ::_thesis: f .: X,f .: Y are_joinable
consider g being FinSequence of bool the carrier of S such that
A4: X = g . 1 and
A5: Y = g . (len g) and
A6: for W being Subset of S st W in rng g holds
( W is closed_under_lines & W is strong ) and
A7: for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1))) by A3, Def3;
deffunc H1( set ) -> Element of bool the carrier of S = f .: (g . $1);
consider p being FinSequence such that
A8: ( len p = len g & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
A9: dom g = Seg (len g) by FINSEQ_1:def_3;
A10: dom p = Seg (len p) by FINSEQ_1:def_3;
rng p c= bool the carrier of S
proof
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in rng p or o in bool the carrier of S )
assume o in rng p ; ::_thesis: o in bool the carrier of S
then consider i being set such that
A11: i in dom p and
A12: o = p . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A11;
g . i in rng g by A8, A10, A9, A11, FUNCT_1:3;
then reconsider gi = g . i as Subset of S ;
p . i = f .: gi by A8, A11;
hence o in bool the carrier of S by A12; ::_thesis: verum
end;
then reconsider p = p as FinSequence of bool the carrier of S by FINSEQ_1:def_4;
take p ; :: according to PENCIL_2:def_3 ::_thesis: ( f .: X = p . 1 & f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )
1 in dom g by A1, A4, FUNCT_1:def_2;
hence f .: X = p . 1 by A4, A8, A10, A9; ::_thesis: ( f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )
len g in dom g by A2, A5, FUNCT_1:def_2;
hence f .: Y = p . (len p) by A5, A8, A10, A9; ::_thesis: ( ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )
thus for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ::_thesis: for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1)))
proof
let W be Subset of S; ::_thesis: ( W in rng p implies ( W is closed_under_lines & W is strong ) )
assume W in rng p ; ::_thesis: ( W is closed_under_lines & W is strong )
then consider i being set such that
A13: i in dom p and
A14: W = p . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A13;
g . i in rng g by A8, A10, A9, A13, FUNCT_1:3;
then reconsider gi = g . i as Subset of S ;
gi in rng g by A8, A10, A9, A13, FUNCT_1:3;
then A15: ( gi is strong & gi is closed_under_lines ) by A6;
p . i = f .: gi by A8, A13;
hence ( W is closed_under_lines & W is strong ) by A14, A15, Th16, Th18; ::_thesis: verum
end;
A16: f is bijective by Def4;
thus for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len p implies 2 c= card ((p . i) /\ (p . (i + 1))) )
assume that
A17: 1 <= i and
A18: i < len p ; ::_thesis: 2 c= card ((p . i) /\ (p . (i + 1)))
A19: (g . i) /\ (g . (i + 1)) c= g . i by XBOOLE_1:17;
i in dom g by A8, A17, A18, FINSEQ_3:25;
then g . i in rng g by FUNCT_1:3;
then reconsider gg = (g . i) /\ (g . (i + 1)) as Subset of S by A19, XBOOLE_1:1;
2 c= card ((g . i) /\ (g . (i + 1))) by A7, A8, A17, A18;
then not gg is trivial by PENCIL_1:4;
then not f .: gg is trivial by Th14;
then A20: not (f .: (g . i)) /\ (f .: (g . (i + 1))) is trivial by A16, FUNCT_1:62;
A21: i + 1 <= len p by A18, NAT_1:13;
1 <= i + 1 by A17, NAT_1:13;
then i + 1 in dom p by A21, FINSEQ_3:25;
then A22: p . (i + 1) = f .: (g . (i + 1)) by A8;
i in dom g by A8, A17, A18, FINSEQ_3:25;
then p . i = f .: (g . i) by A8, A10, A9;
hence 2 c= card ((p . i) /\ (p . (i + 1))) by A22, A20, PENCIL_1:4; ::_thesis: verum
end;
end;
theorem :: PENCIL_2:21
for S being non empty non void TopStruct
for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f " X,f " Y are_joinable
proof
let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f " X,f " Y are_joinable
let f be Collineation of S; ::_thesis: for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f " X,f " Y are_joinable
let X, Y be Subset of S; ::_thesis: ( not X is trivial & not Y is trivial & X,Y are_joinable implies f " X,f " Y are_joinable )
reconsider g = f " as Collineation of S by Th13;
assume that
A1: not X is trivial and
A2: not Y is trivial and
A3: X,Y are_joinable ; ::_thesis: f " X,f " Y are_joinable
A4: f is bijective by Def4;
then A5: rng f = [#] S by FUNCT_2:def_3;
then A6: f " Y = g .: Y by A4, TOPS_2:55;
f " X = g .: X by A4, A5, TOPS_2:55;
hence f " X,f " Y are_joinable by A6, A1, A2, A3, Th20; ::_thesis: verum
end;
theorem Th22: :: PENCIL_2:22
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A
let W be Subset of (Segre_Product A); ::_thesis: ( not W is trivial & W is strong & W is closed_under_lines implies union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A )
assume A2: ( not W is trivial & W is strong & W is closed_under_lines ) ; ::_thesis: union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A
consider K being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3: W = product K and
A4: for S being Subset of (A . (indx K)) st S = K . (indx K) holds
( S is strong & S is closed_under_lines ) by A2, PENCIL_1:29;
set O = [#] (A . (indx K));
set B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ;
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } c= the carrier of (Segre_Product A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } or a in the carrier of (Segre_Product A) )
assume a in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; ::_thesis: a in the carrier of (Segre_Product A)
then consider y being set such that
A5: a in y and
A6: y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by TARSKI:def_4;
ex Y being Subset of (Segre_Product A) st
( y = Y & not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) by A6;
hence a in the carrier of (Segre_Product A) by A5; ::_thesis: verum
end;
then reconsider C = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } as Subset of (Segre_Product A) ;
dom A = I by PARTFUN1:def_2;
then A . (indx K) in rng A by FUNCT_1:3;
then A7: not A . (indx K) is trivial by PENCIL_1:def_17;
then reconsider L = K +* ((indx K),([#] (A . (indx K)))) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th7, PENCIL_1:27;
dom K = I by PARTFUN1:def_2;
then L . (indx K) = [#] (A . (indx K)) by FUNCT_7:31;
then A8: indx K = indx L by A7, PENCIL_1:def_21;
A9: product L c= C
proof
K c= Carrier A by PBOOLE:def_18;
then K . (indx K) c= (Carrier A) . (indx K) by PBOOLE:def_2;
then reconsider S = K . (indx K) as Subset of (A . (indx K)) by YELLOW_6:2;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in product L or y in C )
A10: dom K = I by PARTFUN1:def_2;
A11: A . (indx K) is strongly_connected by A1;
assume y in product L ; ::_thesis: y in C
then consider z being Function such that
A12: z = y and
A13: dom z = dom L and
A14: for a being set st a in dom L holds
z . a in L . a by CARD_3:def_5;
A15: dom L = I by PARTFUN1:def_2;
then reconsider z = z as ManySortedSet of I by A13, PARTFUN1:def_2, RELAT_1:def_18;
z . (indx K) in L . (indx K) by A14, A15;
then reconsider zi = z . (indx K) as Point of (A . (indx K)) by A10, FUNCT_7:31;
( not S is trivial & S is strong & S is closed_under_lines ) by A4, PENCIL_1:def_21;
then consider f being FinSequence of bool the carrier of (A . (indx K)) such that
A16: S = f . 1 and
A17: zi in f . (len f) and
A18: for Z being Subset of (A . (indx K)) st Z in rng f holds
( Z is closed_under_lines & Z is strong ) and
A19: for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by A11, PENCIL_1:def_11;
A20: len f in dom f by A17, FUNCT_1:def_2;
then 1 in dom f by FINSEQ_5:6, RELAT_1:38;
then A21: 1 in Seg (len f) by FINSEQ_1:def_3;
A22: not f . (len f) is trivial
proof
reconsider l1 = (len f) - 1 as Element of NAT by A20, FINSEQ_3:26;
A23: 1 <= len f by A20, FINSEQ_3:25;
percases ( len f = 1 or len f > 1 ) by A23, XXREAL_0:1;
suppose len f = 1 ; ::_thesis: not f . (len f) is trivial
hence not f . (len f) is trivial by A16, PENCIL_1:def_21; ::_thesis: verum
end;
suppose len f > 1 ; ::_thesis: not f . (len f) is trivial
then 1 + 1 <= len f by NAT_1:13;
then A24: 2 - 1 <= l1 by XREAL_1:9;
A25: card ((f . l1) /\ (f . (l1 + 1))) c= card (f . (l1 + 1)) by CARD_1:11, XBOOLE_1:17;
l1 < (len f) - 0 by XREAL_1:15;
then 2 c= card ((f . l1) /\ (f . (l1 + 1))) by A19, A24;
then 2 c= card (f . (l1 + 1)) by A25, XBOOLE_1:1;
hence not f . (len f) is trivial by PENCIL_1:4; ::_thesis: verum
end;
end;
end;
then reconsider ff = f . (len f) as non trivial set ;
L . (indx K) = [#] (A . (indx K)) by A10, FUNCT_7:31;
then indx K = indx L by A7, PENCIL_1:def_21;
then reconsider EL = L +* ((indx K),ff) as non trivial-yielding Segre-like ManySortedSet of I by PENCIL_1:27;
A26: dom z = dom (L +* ((indx K),(f . (len f)))) by A13, FUNCT_7:30;
deffunc H1( set ) -> set = product (L +* ((indx K),(f . $1)));
consider g being FinSequence such that
A27: ( len g = len f & ( for k being Nat st k in dom g holds
g . k = H1(k) ) ) from FINSEQ_1:sch_2();
A28: rng g c= bool the carrier of (Segre_Product A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in bool the carrier of (Segre_Product A) )
A29: dom (Carrier A) = I by PARTFUN1:def_2;
assume a in rng g ; ::_thesis: a in bool the carrier of (Segre_Product A)
then consider k being set such that
A30: k in dom g and
A31: a = g . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A30;
A32: k in Seg (len f) by A27, A30, FINSEQ_1:def_3;
A33: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
(L_+*_((indx_K),(f_._k)))_._o_c=_(Carrier_A)_._o
let o be set ; ::_thesis: ( o in I implies (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1 )
assume A34: o in I ; ::_thesis: (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1
A35: k in dom f by A32, FINSEQ_1:def_3;
percases ( o <> indx K or o = indx K ) ;
supposeA36: o <> indx K ; ::_thesis: (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1
then (L +* ((indx K),(f . k))) . o = L . o by FUNCT_7:32;
then A37: (L +* ((indx K),(f . k))) . o = K . o by A36, FUNCT_7:32;
K c= Carrier A by PBOOLE:def_18;
hence (L +* ((indx K),(f . k))) . o c= (Carrier A) . o by A34, A37, PBOOLE:def_2; ::_thesis: verum
end;
supposeA38: o = indx K ; ::_thesis: (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1
then (L +* ((indx K),(f . k))) . o = f . k by A15, FUNCT_7:31;
then (L +* ((indx K),(f . k))) . o in rng f by A35, FUNCT_1:3;
then (L +* ((indx K),(f . k))) . o c= the carrier of (A . (indx K)) ;
hence (L +* ((indx K),(f . k))) . o c= (Carrier A) . o by A38, YELLOW_6:2; ::_thesis: verum
end;
end;
end;
dom (L +* ((indx K),(f . k))) = I by PARTFUN1:def_2;
then product (L +* ((indx K),(f . k))) c= product (Carrier A) by A29, A33, CARD_3:27;
then a c= product (Carrier A) by A27, A30, A31;
hence a in bool the carrier of (Segre_Product A) ; ::_thesis: verum
end;
A39: dom g = Seg (len f) by A27, FINSEQ_1:def_3;
reconsider g = g as FinSequence of bool the carrier of (Segre_Product A) by A28, FINSEQ_1:def_4;
len f in dom g by A20, A27, FINSEQ_3:29;
then A40: g . (len f) in rng g by FUNCT_1:3;
then reconsider Yb = g . (len f) as Subset of (Segre_Product A) ;
A41: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
(L_+*_((indx_K),(f_._1)))_._o_=_K_._o
let o be set ; ::_thesis: ( o in I implies (L +* ((indx K),(f . 1))) . b1 = K . b1 )
assume o in I ; ::_thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1
percases ( o <> indx K or o = indx K ) ;
supposeA42: o <> indx K ; ::_thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1
then (L +* ((indx K),(f . 1))) . o = L . o by FUNCT_7:32;
hence (L +* ((indx K),(f . 1))) . o = K . o by A42, FUNCT_7:32; ::_thesis: verum
end;
suppose o = indx K ; ::_thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1
hence (L +* ((indx K),(f . 1))) . o = K . o by A15, A16, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
A43: for V being Subset of (Segre_Product A) st V in rng g holds
( V is closed_under_lines & V is strong )
proof
let V be Subset of (Segre_Product A); ::_thesis: ( V in rng g implies ( V is closed_under_lines & V is strong ) )
assume V in rng g ; ::_thesis: ( V is closed_under_lines & V is strong )
then consider n1 being set such that
A44: n1 in dom g and
A45: V = g . n1 by FUNCT_1:def_3;
reconsider n = n1 as Element of NAT by A44;
n in Seg (len f) by A27, A44, FINSEQ_1:def_3;
then A46: n in dom f by FINSEQ_1:def_3;
not f . n is trivial
proof
A47: n <= len f by A46, FINSEQ_3:25;
percases ( ( 1 <= n & n = len f ) or ( 1 <= n & n < len f ) ) by A46, A47, FINSEQ_3:25, XXREAL_0:1;
suppose ( 1 <= n & n = len f ) ; ::_thesis: not f . n is trivial
hence not f . n is trivial by A22; ::_thesis: verum
end;
supposeA48: ( 1 <= n & n < len f ) ; ::_thesis: not f . n is trivial
A49: card ((f . n) /\ (f . (n + 1))) c= card (f . n) by CARD_1:11, XBOOLE_1:17;
2 c= card ((f . n) /\ (f . (n + 1))) by A19, A48;
then 2 c= card (f . n) by A49, XBOOLE_1:1;
hence not f . n is trivial by PENCIL_1:4; ::_thesis: verum
end;
end;
end;
then reconsider fn = f . n as non trivial set ;
A50: L +* ((indx K),(f . n)) c= Carrier A
proof
let o be set ; :: according to PBOOLE:def_2 ::_thesis: ( not o in I or (L +* ((indx K),(f . n))) . o c= (Carrier A) . o )
assume A51: o in I ; ::_thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o
percases ( o <> indx K or o = indx K ) ;
supposeA52: o <> indx K ; ::_thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o
A53: L c= Carrier A by PBOOLE:def_18;
(L +* ((indx K),(f . n))) . o = L . o by A52, FUNCT_7:32;
hence (L +* ((indx K),(f . n))) . o c= (Carrier A) . o by A51, A53, PBOOLE:def_2; ::_thesis: verum
end;
supposeA54: o = indx K ; ::_thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o
then (L +* ((indx K),(f . n))) . o = f . n by A15, FUNCT_7:31;
then (L +* ((indx K),(f . n))) . o in rng f by A46, FUNCT_1:3;
then (L +* ((indx K),(f . n))) . o c= the carrier of (A . (indx K)) ;
hence (L +* ((indx K),(f . n))) . o c= (Carrier A) . o by A54, YELLOW_6:2; ::_thesis: verum
end;
end;
end;
L . (indx K) = [#] (A . (indx K)) by A10, FUNCT_7:31;
then indx K = indx L by A7, PENCIL_1:def_21;
then reconsider LI = L +* ((indx K),fn) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A50, PBOOLE:def_18, PENCIL_1:27;
reconsider LI = LI as non trivial-yielding Segre-like ManySortedSubset of Carrier A ;
A55: LI . (indx K) = fn by A15, FUNCT_7:31;
then A56: indx LI = indx K by PENCIL_1:def_21;
A57: now__::_thesis:_for_D_being_Subset_of_(A_._(indx_LI))_st_D_=_LI_._(indx_LI)_holds_
(_D_is_strong_&_D_is_closed_under_lines_)
let D be Subset of (A . (indx LI)); ::_thesis: ( D = LI . (indx LI) implies ( D is strong & D is closed_under_lines ) )
assume D = LI . (indx LI) ; ::_thesis: ( D is strong & D is closed_under_lines )
then D in rng f by A46, A55, A56, FUNCT_1:3;
hence ( D is strong & D is closed_under_lines ) by A18, A56; ::_thesis: verum
end;
g . n = product (L +* ((indx K),(f . n))) by A27, A44;
hence ( V is closed_under_lines & V is strong ) by A45, A57, PENCIL_1:29; ::_thesis: verum
end;
A58: len f in Seg (len f) by A20, FINSEQ_1:def_3;
then Yb = product EL by A27, A39;
then A59: ( not Yb is trivial & Yb is strong & Yb is closed_under_lines ) by A40, A43;
A60: for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1)))
proof
consider l1 being set such that
A61: l1 in product L by XBOOLE_0:def_1;
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len g implies 2 c= card ((g . i) /\ (g . (i + 1))) )
assume that
A62: 1 <= i and
A63: i < len g ; ::_thesis: 2 c= card ((g . i) /\ (g . (i + 1)))
i in Seg (len f) by A27, A62, A63, FINSEQ_1:1;
then A64: g . i = product (L +* ((indx K),(f . i))) by A27, A39;
2 c= card ((f . i) /\ (f . (i + 1))) by A19, A27, A62, A63;
then consider a, b being set such that
A65: a in (f . i) /\ (f . (i + 1)) and
A66: b in (f . i) /\ (f . (i + 1)) and
A67: a <> b by PENCIL_1:2;
consider l being Function such that
l = l1 and
A68: dom l = dom L and
A69: for o being set st o in dom L holds
l . o in L . o by A61, CARD_3:def_5;
reconsider l = l as ManySortedSet of I by A15, A68, PARTFUN1:def_2, RELAT_1:def_18;
set l1 = l +* ((indx K),a);
set l2 = l +* ((indx K),b);
A70: i + 1 <= len g by A63, NAT_1:13;
A71: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._i)))_holds_
(l_+*_((indx_K),a))_._o_in_(L_+*_((indx_K),(f_._i)))_._o
let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1 )
assume o in dom (L +* ((indx K),(f . i))) ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1
then A72: o in I ;
then A73: o in dom l by PARTFUN1:def_2;
percases ( o = indx K or o <> indx K ) ;
supposeA74: o = indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1
then (l +* ((indx K),a)) . o = a by A73, FUNCT_7:31;
then (l +* ((indx K),a)) . o in f . i by A65, XBOOLE_0:def_4;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by A15, A74, FUNCT_7:31; ::_thesis: verum
end;
supposeA75: o <> indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1
then A76: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A72;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by A75, A76, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
1 <= i + 1 by A62, NAT_1:13;
then i + 1 in Seg (len f) by A27, A70, FINSEQ_1:1;
then A77: g . (i + 1) = product (L +* ((indx K),(f . (i + 1)))) by A27, A39;
A78: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._i)))_holds_
(l_+*_((indx_K),b))_._o_in_(L_+*_((indx_K),(f_._i)))_._o
let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1 )
assume o in dom (L +* ((indx K),(f . i))) ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1
then A79: o in I ;
then A80: o in dom l by PARTFUN1:def_2;
percases ( o = indx K or o <> indx K ) ;
supposeA81: o = indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1
then (l +* ((indx K),b)) . o = b by A80, FUNCT_7:31;
then (l +* ((indx K),b)) . o in f . i by A66, XBOOLE_0:def_4;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by A15, A81, FUNCT_7:31; ::_thesis: verum
end;
supposeA82: o <> indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1
then A83: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A79;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by A82, A83, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
A84: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._(i_+_1))))_holds_
(l_+*_((indx_K),a))_._o_in_(L_+*_((indx_K),(f_._(i_+_1))))_._o
let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 )
assume o in dom (L +* ((indx K),(f . (i + 1)))) ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A85: o in I ;
then A86: o in dom l by PARTFUN1:def_2;
percases ( o = indx K or o <> indx K ) ;
supposeA87: o = indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then (l +* ((indx K),a)) . o = a by A86, FUNCT_7:31;
then (l +* ((indx K),a)) . o in f . (i + 1) by A65, XBOOLE_0:def_4;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A15, A87, FUNCT_7:31; ::_thesis: verum
end;
supposeA88: o <> indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A89: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A85;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A88, A89, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom (l +* ((indx K),a)) = I by PARTFUN1:def_2
.= dom (L +* ((indx K),(f . (i + 1)))) by PARTFUN1:def_2 ;
then A90: l +* ((indx K),a) in product (L +* ((indx K),(f . (i + 1)))) by A84, CARD_3:9;
A91: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._(i_+_1))))_holds_
(l_+*_((indx_K),b))_._o_in_(L_+*_((indx_K),(f_._(i_+_1))))_._o
let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 )
assume o in dom (L +* ((indx K),(f . (i + 1)))) ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A92: o in I ;
then A93: o in dom l by PARTFUN1:def_2;
percases ( o = indx K or o <> indx K ) ;
supposeA94: o = indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then (l +* ((indx K),b)) . o = b by A93, FUNCT_7:31;
then (l +* ((indx K),b)) . o in f . (i + 1) by A66, XBOOLE_0:def_4;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A15, A94, FUNCT_7:31; ::_thesis: verum
end;
supposeA95: o <> indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A96: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A92;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A95, A96, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom (l +* ((indx K),b)) = I by PARTFUN1:def_2
.= dom (L +* ((indx K),(f . (i + 1)))) by PARTFUN1:def_2 ;
then A97: l +* ((indx K),b) in product (L +* ((indx K),(f . (i + 1)))) by A91, CARD_3:9;
dom (l +* ((indx K),b)) = I by PARTFUN1:def_2
.= dom (L +* ((indx K),(f . i))) by PARTFUN1:def_2 ;
then l +* ((indx K),b) in product (L +* ((indx K),(f . i))) by A78, CARD_3:9;
then A98: l +* ((indx K),b) in (g . i) /\ (g . (i + 1)) by A64, A77, A97, XBOOLE_0:def_4;
(l +* ((indx K),a)) . (indx K) = a by A15, A68, FUNCT_7:31;
then A99: l +* ((indx K),a) <> l +* ((indx K),b) by A15, A67, A68, FUNCT_7:31;
dom (l +* ((indx K),a)) = I by PARTFUN1:def_2
.= dom (L +* ((indx K),(f . i))) by PARTFUN1:def_2 ;
then l +* ((indx K),a) in product (L +* ((indx K),(f . i))) by A71, CARD_3:9;
then l +* ((indx K),a) in (g . i) /\ (g . (i + 1)) by A64, A77, A90, XBOOLE_0:def_4;
hence 2 c= card ((g . i) /\ (g . (i + 1))) by A99, A98, PENCIL_1:2; ::_thesis: verum
end;
A100: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._(len_f))))_holds_
z_._o_in_(L_+*_((indx_K),(f_._(len_f))))_._o
let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . (len f)))) implies z . b1 in (L +* ((indx K),(f . (len f)))) . b1 )
assume o in dom (L +* ((indx K),(f . (len f)))) ; ::_thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1
then A101: o in I ;
percases ( o = indx K or o <> indx K ) ;
suppose o = indx K ; ::_thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1
hence z . o in (L +* ((indx K),(f . (len f)))) . o by A15, A17, FUNCT_7:31; ::_thesis: verum
end;
supposeA102: o <> indx K ; ::_thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1
z . o in L . o by A14, A15, A101;
hence z . o in (L +* ((indx K),(f . (len f)))) . o by A102, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom (L +* ((indx K),(f . 1))) = I by PARTFUN1:def_2;
then L +* ((indx K),(f . 1)) = K by A10, A41, FUNCT_1:2;
then W = g . 1 by A3, A27, A39, A21;
then W,Yb are_joinable by A27, A43, A60, Def3;
then A103: Yb in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by A59;
Yb = product (L +* ((indx K),(f . (len f)))) by A27, A39, A58;
then y in Yb by A12, A26, A100, CARD_3:9;
hence y in C by A103, TARSKI:def_4; ::_thesis: verum
end;
dom K = I by PARTFUN1:def_2;
then A104: L . (indx L) = [#] (A . (indx L)) by A8, FUNCT_7:31;
C c= product L
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in product L )
assume c in C ; ::_thesis: c in product L
then consider y being set such that
A105: c in y and
A106: y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by TARSKI:def_4;
consider Y being Subset of (Segre_Product A) such that
A107: y = Y and
A108: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and
A109: W,Y are_joinable by A106;
reconsider c1 = c as ManySortedSet of I by A105, A107, PENCIL_1:14;
consider M being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A110: Y = product M and
for S being Subset of (A . (indx M)) st S = M . (indx M) holds
( S is strong & S is closed_under_lines ) by A108, PENCIL_1:29;
A111: dom M = I by PARTFUN1:def_2
.= dom L by PARTFUN1:def_2 ;
A112: dom K = I by PARTFUN1:def_2
.= dom L by PARTFUN1:def_2 ;
A113: for a being set st a in dom L holds
c1 . a in L . a
proof
let a be set ; ::_thesis: ( a in dom L implies c1 . a in L . a )
assume A114: a in dom L ; ::_thesis: c1 . a in L . a
then reconsider a1 = a as Element of I ;
percases ( a = indx K or a <> indx K ) ;
supposeA115: a = indx K ; ::_thesis: c1 . a in L . a
M c= Carrier A by PBOOLE:def_18;
then M . a1 c= (Carrier A) . a1 by PBOOLE:def_2;
then A116: M . a1 c= the carrier of (A . a1) by YELLOW_6:2;
c1 . a in M . a by A105, A107, A110, A111, A114, CARD_3:9;
then c1 . a in [#] (A . (indx K)) by A115, A116;
hence c1 . a in L . a by A112, A114, A115, FUNCT_7:31; ::_thesis: verum
end;
supposeA117: a <> indx K ; ::_thesis: c1 . a in L . a
c1 . a in M . a by A105, A107, A110, A111, A114, CARD_3:9;
then c1 . a in K . a by A2, A3, A108, A109, A110, A117, Th11;
hence c1 . a in L . a by A117, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom c1 = I by PARTFUN1:def_2
.= dom L by PARTFUN1:def_2 ;
hence c in product L by A113, CARD_3:9; ::_thesis: verum
end;
then C = product L by A9, XBOOLE_0:def_10;
hence union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A by A104, Def2; ::_thesis: verum
end;
theorem Th23: :: PENCIL_2:23
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )
let B be set ; ::_thesis: ( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )
thus ( B is Segre-Coset of A implies ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) ::_thesis: ( ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) implies B is Segre-Coset of A )
proof
assume B is Segre-Coset of A ; ::_thesis: ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } )
then reconsider BB = B as Segre-Coset of A ;
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A2: BB = product L and
A3: L . (indx L) = [#] (A . (indx L)) by Def2;
set K1 = the Block of (A . (indx L));
consider V being set such that
A4: V in product L by XBOOLE_0:def_1;
the Block of (A . (indx L)) in the topology of (A . (indx L)) ;
then reconsider K = the Block of (A . (indx L)) as Subset of (A . (indx L)) ;
A5: ex g being Function st
( g = V & dom g = dom L & ( for i being set st i in dom L holds
g . i in L . i ) ) by A4, CARD_3:def_5;
A6: dom L = I by PARTFUN1:def_2;
then reconsider V = V as ManySortedSet of I by A5, PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in I holds
V . i is Element of (Carrier A) . i
proof
let i be set ; ::_thesis: ( i in I implies V . i is Element of (Carrier A) . i )
assume A7: i in I ; ::_thesis: V . i is Element of (Carrier A) . i
L c= Carrier A by PBOOLE:def_18;
then A8: L . i c= (Carrier A) . i by A7, PBOOLE:def_2;
V . i in L . i by A6, A5, A7;
hence V . i is Element of (Carrier A) . i by A8; ::_thesis: verum
end;
then reconsider V = V as Element of Carrier A by PBOOLE:def_14;
reconsider VV = {V} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider X = VV +* ((indx L),K) as ManySortedSubset of Carrier A by Th7;
2 c= card K by PENCIL_1:def_6;
then A9: not K is trivial by PENCIL_1:4;
then reconsider X = X as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10;
dom VV = I by PARTFUN1:def_2;
then A10: X . (indx L) = K by FUNCT_7:31;
then indx X = indx L by A9, PENCIL_1:def_21;
then reconsider pX = product X as Block of (Segre_Product A) by A10, PENCIL_1:24;
A11: for i being set st i in I holds
X . i c= L . i
proof
let i be set ; ::_thesis: ( i in I implies X . i c= L . i )
assume A12: i in I ; ::_thesis: X . i c= L . i
percases ( i <> indx L or i = indx L ) ;
suppose i <> indx L ; ::_thesis: X . i c= L . i
then X . i = VV . i by FUNCT_7:32;
then A13: X . i = {(V . i)} by A12, PZFMISC1:def_1;
V . i in L . i by A6, A5, A12;
hence X . i c= L . i by A13, ZFMISC_1:31; ::_thesis: verum
end;
suppose i = indx L ; ::_thesis: X . i c= L . i
hence X . i c= L . i by A3, A10; ::_thesis: verum
end;
end;
end;
pX in the topology of (Segre_Product A) ;
then reconsider psX = pX as Subset of (Segre_Product A) ;
take psX ; ::_thesis: ( not psX is trivial & psX is strong & psX is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } )
thus A14: ( not psX is trivial & psX is strong & psX is closed_under_lines ) by PENCIL_1:20, PENCIL_1:21; ::_thesis: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) }
then reconsider Z = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } as Segre-Coset of A by A1, Th22;
psX,psX are_joinable by A14, Th10;
then A15: psX in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } by A14;
A16: psX c= Z
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in psX or a in Z )
assume a in psX ; ::_thesis: a in Z
hence a in Z by A15, TARSKI:def_4; ::_thesis: verum
end;
dom X = I by PARTFUN1:def_2;
then psX c= B by A2, A6, A11, CARD_3:27;
then psX c= B /\ Z by A16, XBOOLE_1:19;
then A17: card psX c= card (B /\ Z) by CARD_1:11;
2 c= card pX by PENCIL_1:def_6;
then BB = Z by A17, Th8, XBOOLE_1:1;
hence B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } ; ::_thesis: verum
end;
given W being Subset of (Segre_Product A) such that A18: ( not W is trivial & W is strong & W is closed_under_lines ) and
A19: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; ::_thesis: B is Segre-Coset of A
thus B is Segre-Coset of A by A1, A18, A19, Th22; ::_thesis: verum
end;
theorem Th24: :: PENCIL_2:24
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let B be Segre-Coset of A; ::_thesis: for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
consider W being Subset of (Segre_Product A) such that
A2: ( not W is trivial & W is strong & W is closed_under_lines ) and
A3: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by A1, Th23;
let f be Collineation of (Segre_Product A); ::_thesis: f .: B is Segre-Coset of A
reconsider g = f " as Collineation of (Segre_Product A) by Th13;
A4: dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1;
A5: dom g = the carrier of (Segre_Product A) by FUNCT_2:def_1;
A6: f is bijective by Def4;
then A7: rng f = the carrier of (Segre_Product A) by FUNCT_2:def_3;
A8: rng f = [#] (Segre_Product A) by A6, FUNCT_2:def_3;
A9: f .: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
proof
A10: W c= f " (f .: W) by A4, FUNCT_1:76;
f " (f .: W) c= W by A6, FUNCT_1:82;
then A11: f " (f .: W) = W by A10, XBOOLE_0:def_10;
thus f .: B c= union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } :: according to XBOOLE_0:def_10 ::_thesis: union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } c= f .: B
proof
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in f .: B or o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } )
assume o in f .: B ; ::_thesis: o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
then consider u being set such that
A12: u in dom f and
A13: u in B and
A14: o = f . u by FUNCT_1:def_6;
consider y being set such that
A15: u in y and
A16: y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by A3, A13, TARSKI:def_4;
consider Y being Subset of (Segre_Product A) such that
A17: y = Y and
A18: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and
A19: W,Y are_joinable by A16;
A20: f .: W,f .: Y are_joinable by A2, A18, A19, Th20;
( not f .: Y is trivial & f .: Y is strong & f .: Y is closed_under_lines ) by A18, Th14, Th16, Th18;
then A21: f .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & f .: W,Z are_joinable ) } by A20;
o in f .: Y by A12, A14, A15, A17, FUNCT_1:def_6;
hence o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } by A21, TARSKI:def_4; ::_thesis: verum
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } or o in f .: B )
assume o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } ; ::_thesis: o in f .: B
then consider u being set such that
A22: o in u and
A23: u in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } by TARSKI:def_4;
consider Y being Subset of (Segre_Product A) such that
A24: u = Y and
A25: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and
A26: f .: W,Y are_joinable by A23;
A27: ( not g .: Y is trivial & g .: Y is strong & g .: Y is closed_under_lines ) by A25, Th14, Th16, Th18;
( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A2, Th14, Th16, Th18;
then g .: (f .: W),g .: Y are_joinable by A25, A26, Th20;
then W,g .: Y are_joinable by A6, A8, A11, TOPS_2:55;
then A28: g .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & W,Z are_joinable ) } by A27;
g . o in g .: Y by A5, A22, A24, FUNCT_1:def_6;
then A29: g . o in B by A3, A28, TARSKI:def_4;
o = f . ((f ") . o) by A6, A7, A22, A24, FUNCT_1:35;
then o = f . (g . o) by A6, TOPS_2:def_4;
hence o in f .: B by A4, A29, FUNCT_1:def_6; ::_thesis: verum
end;
( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A2, Th14, Th16, Th18;
hence f .: B is Segre-Coset of A by A1, A9, Th23; ::_thesis: verum
end;
theorem :: PENCIL_2:25
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A
let B be Segre-Coset of A; ::_thesis: for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A
let f be Collineation of (Segre_Product A); ::_thesis: f " B is Segre-Coset of A
reconsider g = f " as Collineation of (Segre_Product A) by Th13;
A2: f is bijective by Def4;
then rng f = [#] (Segre_Product A) by FUNCT_2:def_3;
then f " B = g .: B by A2, TOPS_2:55;
hence f " B is Segre-Coset of A by A1, Th24; ::_thesis: verum
end;