set f1 = <*|[0,0]|,|[0,1]|,|[1,1]|*>;
set f2 = <*|[1,0]|,|[0,0]|*>;
A1: len <*|[0,0]|,|[0,1]|,|[1,1]|*> = 3 by FINSEQ_1:45;
A2: len <*|[1,0]|,|[0,0]|*> = 2 by FINSEQ_1:44;
then A3: len (<*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*>) = 3 + 2 by A1, FINSEQ_1:22;
reconsider f = <*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*> as non empty FinSequence of (TOP-REAL 2) ;
take f ; :: thesis: ( f is V8() & f is special & f is unfolded & f is circular & f is s.c.c. & f is standard )
A4: 1 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25;
then A5: f /. 1 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 1 by FINSEQ_4:68
.= |[0,0]| by FINSEQ_4:18 ;
A6: 2 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25;
then A7: f /. 2 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 2 by FINSEQ_4:68
.= |[0,1]| by FINSEQ_4:18 ;
A8: dom <*|[0,0]|,|[0,1]|,|[1,1]|*> c= dom f by FINSEQ_1:26;
then A9: f . 1 = f /. 1 by A4, PARTFUN1:def 6;
f . 2 = f /. 2 by A6, A8, PARTFUN1:def 6;
then f . 1 <> f . 2 by A5, A7, A9, SPPOL_2:1;
hence f is V8() by A4, A6, A8; :: thesis: ( f is special & f is unfolded & f is circular & f is s.c.c. & f is standard )
3 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25;
then A10: f /. 3 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 3 by FINSEQ_4:68
.= |[1,1]| by FINSEQ_4:18 ;
1 in dom <*|[1,0]|,|[0,0]|*> by A2, FINSEQ_3:25;
then A11: f /. (3 + 1) = <*|[1,0]|,|[0,0]|*> /. 1 by A1, FINSEQ_4:69
.= |[1,0]| by FINSEQ_4:17 ;
2 in dom <*|[1,0]|,|[0,0]|*> by A2, FINSEQ_3:25;
then A12: f /. (3 + 2) = <*|[1,0]|,|[0,0]|*> /. 2 by A1, FINSEQ_4:69
.= |[0,0]| by FINSEQ_4:17 ;
1 + 1 = 2 ;
then A13: LSeg (f,1) = LSeg (|[0,0]|,|[0,1]|) by A3, A5, A7, TOPREAL1:def 3;
2 + 1 = 3 ;
then A14: LSeg (f,2) = LSeg (|[0,1]|,|[1,1]|) by A3, A7, A10, TOPREAL1:def 3;
A15: LSeg (f,3) = LSeg (|[1,1]|,|[1,0]|) by A3, A10, A11, TOPREAL1:def 3;
4 + 1 = 5 ;
then A16: LSeg (f,4) = LSeg (|[1,0]|,|[0,0]|) by A3, A11, A12, TOPREAL1:def 3;
thus f is special :: thesis: ( f is unfolded & f is circular & f is s.c.c. & f is standard )
proof
let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
assume 1 <= i ; :: thesis: ( not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
then 1 + 1 <= i + 1 by XREAL_1:6;
then A17: 1 < i + 1 by XXREAL_0:2;
assume i + 1 <= len f ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
then A18: not not i + 1 = 0 & ... & not i + 1 = 5 by A3;
per cases ( i = 1 or i = 2 or i = 3 or i = 4 ) by A17, A18;
suppose A19: i = 1 ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 1) `1 = 0 by A5, EUCLID:52
.= (f /. (1 + 1)) `1 by A7, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A19; :: thesis: verum
end;
suppose A20: i = 2 ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 2) `2 = 1 by A7, EUCLID:52
.= (f /. (2 + 1)) `2 by A10, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A20; :: thesis: verum
end;
suppose A21: i = 3 ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 3) `1 = 1 by A10, EUCLID:52
.= (f /. (3 + 1)) `1 by A11, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A21; :: thesis: verum
end;
suppose A22: i = 4 ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 4) `2 = 0 by A11, EUCLID:52
.= (f /. (4 + 1)) `2 by A12, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A22; :: thesis: verum
end;
end;
end;
thus f is unfolded :: thesis: ( f is circular & f is s.c.c. & f is standard )
proof
let i be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
assume 1 <= i ; :: thesis: ( not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
then 1 + 2 <= i + 2 by XREAL_1:6;
then A23: 2 < i + 2 by XXREAL_0:2;
assume i + 2 <= len f ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
then A24: not not i + 2 = 0 & ... & not i + 2 = 5 by A3;
per cases ( i = 1 or i = 2 or i = 3 ) by A23, A24;
suppose i = 1 ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A5, A7, A14, TOPREAL1:15, TOPREAL1:def 3; :: thesis: verum
end;
suppose i = 2 ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A7, A10, A15, TOPREAL1:18, TOPREAL1:def 3; :: thesis: verum
end;
suppose i = 3 ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A10, A11, A16, TOPREAL1:16, TOPREAL1:def 3; :: thesis: verum
end;
end;
end;
thus f /. 1 = f /. (len f) by A1, A2, A5, A12, FINSEQ_1:22; :: according to FINSEQ_6:def 1 :: thesis: ( f is s.c.c. & f is standard )
thus f is s.c.c. :: thesis: f is standard
proof
let i, j be Nat; :: according to GOBOARD5:def 4 :: thesis: ( i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) implies LSeg (f,i) misses LSeg (f,j) )
assume that
A25: i + 1 < j and
A26: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; :: thesis: LSeg (f,i) misses LSeg (f,j)
A27: i + 1 >= 1 by NAT_1:11;
j + 1 <= 5 by A3, A26, NAT_1:13;
then A28: not not j + 1 = 0 & ... & not j + 1 = 5 ;
A29: (i + 1) + 1 = i + (1 + 1) ;
then A30: i + 2 <= j by A25, NAT_1:13;
A31: i + 2 <> 0 + 1 by A29;
A32: now :: thesis: ( ( j = 2 & i = 0 ) or ( j = 3 & ( i = 0 or i = 1 ) ) or ( j = 4 & ( i = 0 or i = 2 ) ) )
per cases ( j = 2 or j = 3 or j = 4 ) by A25, A27, A28;
case j = 2 ; :: thesis: i = 0
then not not i + 2 = 0 & ... & not i + 2 = 2 by A30;
hence i = 0 by A25; :: thesis: verum
end;
case j = 3 ; :: thesis: ( i = 0 or i = 1 )
then not not i + 2 = 0 & ... & not i + 2 = 3 by A30;
hence ( i = 0 or i = 1 ) by A25; :: thesis: verum
end;
case A33: j = 4 ; :: thesis: ( i = 0 or i = 2 )
then not not i + 2 = 0 & ... & not i + 2 = 4 by A30;
hence ( i = 0 or i = 2 ) by A3, A26, A31, A33; :: thesis: verum
end;
end;
end;
per cases ( i = 0 or ( i = 1 & j = 3 ) or ( i = 2 & j = 4 ) ) by A32;
suppose i = 0 ; :: thesis: LSeg (f,i) misses LSeg (f,j)
then LSeg (f,i) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
suppose ( i = 1 & j = 3 ) ; :: thesis: LSeg (f,i) misses LSeg (f,j)
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by A13, A15, TOPREAL1:20; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
suppose ( i = 2 & j = 4 ) ; :: thesis: LSeg (f,i) misses LSeg (f,j)
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by A14, A16, TOPREAL1:19; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
end;
end;
set Xf1 = <*zz,zz,jj*>;
set Xf2 = <*jj,zz*>;
reconsider Xf = <*zz,zz,jj*> ^ <*jj,zz*> as FinSequence of REAL ;
A34: len <*zz,zz,jj*> = 3 by FINSEQ_1:45;
A35: len <*jj,zz*> = 2 by FINSEQ_1:44;
then A36: len Xf = 3 + 2 by A34, FINSEQ_1:22;
1 in dom <*zz,zz,jj*> by A34, FINSEQ_3:25;
then A37: Xf . 1 = <*zz,zz,jj*> . 1 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:45 ;
2 in dom <*zz,zz,jj*> by A34, FINSEQ_3:25;
then A38: Xf . 2 = <*zz,zz,jj*> . 2 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:45 ;
3 in dom <*zz,zz,jj*> by A34, FINSEQ_3:25;
then A39: Xf . 3 = <*zz,zz,jj*> . 3 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:45 ;
1 in dom <*jj,zz*> by A35, FINSEQ_3:25;
then A40: Xf . (3 + 1) = <*jj,zz*> . 1 by A34, FINSEQ_1:def 7
.= 1 by FINSEQ_1:44 ;
2 in dom <*jj,zz*> by A35, FINSEQ_3:25;
then A41: Xf . (3 + 2) = <*jj,zz*> . 2 by A34, FINSEQ_1:def 7
.= 0 by FINSEQ_1:44 ;
now :: thesis: for n being Nat st n in dom Xf holds
Xf . n = (f /. n) `1
let n be Nat; :: thesis: ( n in dom Xf implies Xf . b1 = (f /. b1) `1 )
assume A42: n in dom Xf ; :: thesis: Xf . b1 = (f /. b1) `1
then A43: n <> 0 by FINSEQ_3:25;
n <= 5 by A36, A42, FINSEQ_3:25;
then not not n = 0 & ... & not n = 5 ;
per cases then ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A43;
suppose n = 1 ; :: thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A5, A37, EUCLID:52; :: thesis: verum
end;
suppose n = 2 ; :: thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A7, A38, EUCLID:52; :: thesis: verum
end;
suppose n = 3 ; :: thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A10, A39, EUCLID:52; :: thesis: verum
end;
suppose n = 4 ; :: thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A11, A40, EUCLID:52; :: thesis: verum
end;
suppose n = 5 ; :: thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A12, A41, EUCLID:52; :: thesis: verum
end;
end;
end;
then A44: Xf = X_axis f by A3, A36, GOBOARD1:def 1;
A45: rng <*zz,zz,jj*> = {0,0,1} by FINSEQ_2:128
.= {0,1} by ENUMSET1:30 ;
rng <*jj,zz*> = {0,1} by FINSEQ_2:127;
then A46: rng Xf = {0,1} \/ {0,1} by A45, FINSEQ_1:31
.= {0,1} ;
then A47: rng <*zz,jj*> = rng Xf by FINSEQ_2:127;
A48: len <*zz,jj*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A46, CARD_2:57 ;
<*zz,jj*> is increasing
proof
let n, m be Nat; :: according to SEQM_3:def 1 :: thesis: ( not n in K79(<*zz,jj*>) or not m in K79(<*zz,jj*>) or m <= n or not <*zz,jj*> . m <= <*zz,jj*> . n )
len <*zz,jj*> = 2 by FINSEQ_1:44;
then A49: dom <*zz,jj*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
assume that
A50: n in dom <*zz,jj*> and
A51: m in dom <*zz,jj*> ; :: thesis: ( m <= n or not <*zz,jj*> . m <= <*zz,jj*> . n )
A52: ( n = 1 or n = 2 ) by A49, A50, TARSKI:def 2;
A53: ( m = 1 or m = 2 ) by A49, A51, TARSKI:def 2;
assume A54: n < m ; :: thesis: not <*zz,jj*> . m <= <*zz,jj*> . n
then A55: <*0,jj*> . n = 0 by A52, A53, FINSEQ_1:44;
<*0,jj*> . m = 1 by A52, A53, A54, FINSEQ_1:44;
hence <*zz,jj*> . n < <*zz,jj*> . m by A55; :: thesis: verum
end;
then A56: <*0,jj*> = Incr (X_axis f) by A44, A47, A48, SEQ_4:def 21;
set Yf1 = <*zz,jj,jj*>;
set Yf2 = <*zz,zz*>;
reconsider Yf = <*zz,jj,jj*> ^ <*zz,zz*> as FinSequence of REAL ;
A57: len <*zz,jj,jj*> = 3 by FINSEQ_1:45;
A58: len <*zz,zz*> = 2 by FINSEQ_1:44;
then A59: len Yf = 3 + 2 by A57, FINSEQ_1:22;
1 in dom <*zz,jj,jj*> by A57, FINSEQ_3:25;
then A60: Yf . 1 = <*zz,jj,jj*> . 1 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:45 ;
2 in dom <*zz,jj,jj*> by A57, FINSEQ_3:25;
then A61: Yf . 2 = <*zz,jj,jj*> . 2 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:45 ;
3 in dom <*zz,jj,jj*> by A57, FINSEQ_3:25;
then A62: Yf . 3 = <*zz,jj,jj*> . 3 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:45 ;
1 in dom <*zz,zz*> by A58, FINSEQ_3:25;
then A63: Yf . (3 + 1) = <*zz,zz*> . 1 by A57, FINSEQ_1:def 7
.= 0 by FINSEQ_1:44 ;
2 in dom <*zz,zz*> by A58, FINSEQ_3:25;
then A64: Yf . (3 + 2) = <*zz,zz*> . 2 by A57, FINSEQ_1:def 7
.= 0 by FINSEQ_1:44 ;
now :: thesis: for n being Nat st n in dom Yf holds
Yf . n = (f /. n) `2
let n be Nat; :: thesis: ( n in dom Yf implies Yf . b1 = (f /. b1) `2 )
assume A65: n in dom Yf ; :: thesis: Yf . b1 = (f /. b1) `2
then A66: n <> 0 by FINSEQ_3:25;
n <= 5 by A59, A65, FINSEQ_3:25;
then not not n = 0 & ... & not n = 5 ;
per cases then ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A66;
suppose n = 1 ; :: thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A5, A60, EUCLID:52; :: thesis: verum
end;
suppose n = 2 ; :: thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A7, A61, EUCLID:52; :: thesis: verum
end;
suppose n = 3 ; :: thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A10, A62, EUCLID:52; :: thesis: verum
end;
suppose n = 4 ; :: thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A11, A63, EUCLID:52; :: thesis: verum
end;
suppose n = 5 ; :: thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A12, A64, EUCLID:52; :: thesis: verum
end;
end;
end;
then A67: Yf = Y_axis f by A3, A59, GOBOARD1:def 2;
A68: rng <*zz,jj,jj*> = {0,1,1} by FINSEQ_2:128
.= {1,1,0} by ENUMSET1:59
.= {0,1} by ENUMSET1:30 ;
rng <*zz,zz*> = {0,0} by FINSEQ_2:127
.= {0} by ENUMSET1:29 ;
then A69: rng Yf = {0,1} \/ {0} by A68, FINSEQ_1:31
.= {0,0,1} by ENUMSET1:2
.= {0,1} by ENUMSET1:30 ;
then A70: rng <*0,jj*> = rng Yf by FINSEQ_2:127;
A71: len <*0,jj*> = 2 by FINSEQ_1:44
.= card (rng Yf) by A69, CARD_2:57 ;
<*(In (0,REAL)),jj*> is increasing
proof
let n, m be Nat; :: according to SEQM_3:def 1 :: thesis: ( not n in K79(<*(In (0,REAL)),jj*>) or not m in K79(<*(In (0,REAL)),jj*>) or m <= n or not <*(In (0,REAL)),jj*> . m <= <*(In (0,REAL)),jj*> . n )
len <*0,jj*> = 2 by FINSEQ_1:44;
then A72: dom <*0,jj*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
assume that
A73: n in dom <*(In (0,REAL)),jj*> and
A74: m in dom <*(In (0,REAL)),jj*> ; :: thesis: ( m <= n or not <*(In (0,REAL)),jj*> . m <= <*(In (0,REAL)),jj*> . n )
A75: ( n = 1 or n = 2 ) by A72, A73, TARSKI:def 2;
A76: ( m = 1 or m = 2 ) by A72, A74, TARSKI:def 2;
assume A77: n < m ; :: thesis: not <*(In (0,REAL)),jj*> . m <= <*(In (0,REAL)),jj*> . n
then A78: <*0,jj*> . n = 0 by A75, A76, FINSEQ_1:44;
<*0,jj*> . m = 1 by A75, A76, A77, FINSEQ_1:44;
hence <*(In (0,REAL)),jj*> . n < <*(In (0,REAL)),jj*> . m by A78; :: thesis: verum
end;
then A79: <*0,jj*> = Incr (Y_axis f) by A67, A70, A71, SEQ_4:def 21;
set M = (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|);
A80: len ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_0:47
.= len (Incr (X_axis f)) by A56, FINSEQ_1:44 ;
A81: width ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_0:47
.= len (Incr (Y_axis f)) by A79, FINSEQ_1:44 ;
for n, m being Nat st [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) holds
((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
proof
let n, m be Nat; :: thesis: ( [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) implies ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| )
assume [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) ; :: thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:2, MATRIX_0:47;
then A82: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
A83: <*0,jj*> . 1 = 0 by FINSEQ_1:44;
A84: <*0,jj*> . 2 = 1 by FINSEQ_1:44;
per cases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A82, ENUMSET1:def 2;
suppose A85: [n,m] = [1,1] ; :: thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A86: n = 1 by XTUPLE_0:1;
m = 1 by A85, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A83, A86, MATRIX_0:50; :: thesis: verum
end;
suppose A87: [n,m] = [1,2] ; :: thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A88: n = 1 by XTUPLE_0:1;
m = 2 by A87, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A83, A84, A88, MATRIX_0:50; :: thesis: verum
end;
suppose A89: [n,m] = [2,1] ; :: thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A90: n = 2 by XTUPLE_0:1;
m = 1 by A89, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A83, A84, A90, MATRIX_0:50; :: thesis: verum
end;
suppose A91: [n,m] = [2,2] ; :: thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A92: n = 2 by XTUPLE_0:1;
m = 2 by A91, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A84, A92, MATRIX_0:50; :: thesis: verum
end;
end;
end;
then A93: (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|) = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A80, A81, GOBOARD2:def 1
.= GoB f by GOBOARD2:def 2 ;
then A94: f /. 1 = (GoB f) * (1,1) by A5, MATRIX_0:50;
A95: f /. 2 = (GoB f) * (1,2) by A7, A93, MATRIX_0:50;
A96: f /. 3 = (GoB f) * (2,2) by A10, A93, MATRIX_0:50;
A97: f /. 4 = (GoB f) * (2,1) by A11, A93, MATRIX_0:50;
thus for k being Nat st k in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) :: according to GOBOARD1:def 9,GOBOARD5:def 5 :: thesis: for b1 being set holds
( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being set holds
( not [b2,b3] in Indices (GoB f) or not [b4,b5] in Indices (GoB f) or not f /. b1 = (GoB f) * (b2,b3) or not f /. (b1 + 1) = (GoB f) * (b4,b5) or |.(b2 - b4).| + |.(b3 - b5).| = 1 ) )
proof
let k be Nat; :: thesis: ( k in dom f implies ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )
assume A98: k in dom f ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
then A99: k <= 5 by A3, FINSEQ_3:25;
A100: k <> 0 by A98, FINSEQ_3:25;
not not k = 0 & ... & not k = 5 by A99;
per cases then ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 ) by A100;
suppose A101: k = 1 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 1 ; :: thesis: ex j being Nat st
( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) )
take 1 ; :: thesis: ( [1,1] in Indices (GoB f) & f /. k = (GoB f) * (1,1) )
thus [1,1] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis: f /. k = (GoB f) * (1,1)
thus f /. k = (GoB f) * (1,1) by A5, A93, A101, MATRIX_0:50; :: thesis: verum
end;
suppose A102: k = 2 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 1 ; :: thesis: ex j being Nat st
( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) )
take 2 ; :: thesis: ( [1,2] in Indices (GoB f) & f /. k = (GoB f) * (1,2) )
thus [1,2] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis: f /. k = (GoB f) * (1,2)
thus f /. k = (GoB f) * (1,2) by A7, A93, A102, MATRIX_0:50; :: thesis: verum
end;
suppose A103: k = 3 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 2 ; :: thesis: ex j being Nat st
( [2,j] in Indices (GoB f) & f /. k = (GoB f) * (2,j) )
take 2 ; :: thesis: ( [2,2] in Indices (GoB f) & f /. k = (GoB f) * (2,2) )
thus [2,2] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis: f /. k = (GoB f) * (2,2)
thus f /. k = (GoB f) * (2,2) by A10, A93, A103, MATRIX_0:50; :: thesis: verum
end;
suppose A104: k = 4 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 2 ; :: thesis: ex j being Nat st
( [2,j] in Indices (GoB f) & f /. k = (GoB f) * (2,j) )
take 1 ; :: thesis: ( [2,1] in Indices (GoB f) & f /. k = (GoB f) * (2,1) )
thus [2,1] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis: f /. k = (GoB f) * (2,1)
thus f /. k = (GoB f) * (2,1) by A11, A93, A104, MATRIX_0:50; :: thesis: verum
end;
suppose A105: k = 5 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 1 ; :: thesis: ex j being Nat st
( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) )
take 1 ; :: thesis: ( [1,1] in Indices (GoB f) & f /. k = (GoB f) * (1,1) )
thus [1,1] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis: f /. k = (GoB f) * (1,1)
thus f /. k = (GoB f) * (1,1) by A12, A93, A105, MATRIX_0:50; :: thesis: verum
end;
end;
end;
let n be Nat; :: thesis: ( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that
A106: n in dom f and
A107: n + 1 in dom f ; :: thesis: for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 )
let m, k, i, j be Nat; :: thesis: ( not [m,k] in Indices (GoB f) or not [i,j] in Indices (GoB f) or not f /. n = (GoB f) * (m,k) or not f /. (n + 1) = (GoB f) * (i,j) or |.(m - i).| + |.(k - j).| = 1 )
assume that
A108: [m,k] in Indices (GoB f) and
A109: [i,j] in Indices (GoB f) and
A110: f /. n = (GoB f) * (m,k) and
A111: f /. (n + 1) = (GoB f) * (i,j) ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A112: n <> 0 by A106, FINSEQ_3:25;
n + 1 <= 4 + 1 by A3, A107, FINSEQ_3:25;
then not not n = 0 & ... & not n = 4 by NAT_1:60, XREAL_1:6;
per cases then ( n = 1 or n = 2 or n = 3 or n = 4 ) by A112;
suppose A113: n = 1 ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A114: [1,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A115: m = 1 by A94, A108, A110, A113, GOBOARD1:5;
A116: k = 1 by A94, A108, A110, A113, A114, GOBOARD1:5;
A117: [1,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A118: i = 1 by A95, A109, A111, A113, GOBOARD1:5;
j = 1 + 1 by A95, A109, A111, A113, A117, GOBOARD1:5;
then |.(k - j).| = 1 by A116, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A115, A118, SEQM_3:42; :: thesis: verum
end;
suppose A119: n = 2 ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A120: [1,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A121: m = 1 by A95, A108, A110, A119, GOBOARD1:5;
A122: k = 2 by A95, A108, A110, A119, A120, GOBOARD1:5;
A123: [2,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A124: i = 1 + 1 by A96, A109, A111, A119, GOBOARD1:5;
A125: j = 2 by A96, A109, A111, A119, A123, GOBOARD1:5;
|.(m - i).| = 1 by A121, A124, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A122, A125, SEQM_3:42; :: thesis: verum
end;
suppose A126: n = 3 ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A127: [2,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A128: m = 2 by A96, A108, A110, A126, GOBOARD1:5;
A129: k = 1 + 1 by A96, A108, A110, A126, A127, GOBOARD1:5;
A130: [2,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A131: i = 2 by A97, A109, A111, A126, GOBOARD1:5;
j = 1 by A97, A109, A111, A126, A130, GOBOARD1:5;
then |.(k - j).| = 1 by A129, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A128, A131, SEQM_3:42; :: thesis: verum
end;
suppose A132: n = 4 ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A133: [2,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A134: m = 1 + 1 by A97, A108, A110, A132, GOBOARD1:5;
A135: k = 1 by A97, A108, A110, A132, A133, GOBOARD1:5;
A136: [1,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A137: i = 1 by A5, A12, A94, A109, A111, A132, GOBOARD1:5;
A138: j = 1 by A5, A12, A94, A109, A111, A132, A136, GOBOARD1:5;
|.(m - i).| = 1 by A134, A137, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A135, A138, SEQM_3:42; :: thesis: verum
end;
end;