set M = Gauge C,n;
A1:
Indices (Gauge C,n) = [:(dom (Gauge C,n)),(Seg (width (Gauge C,n))):]
by MATRIX_1:def 5;
thus
Gauge C,n is Y_increasing-in-line
Gauge C,n is X_increasing-in-column proof
let i be
Element of
NAT ;
GOBOARD1:def 8 ( not i in dom (Gauge C,n) or not Y_axis (Line (Gauge C,n),i) is V74() )
assume A2:
i in dom (Gauge C,n)
;
Y_axis (Line (Gauge C,n),i) is V74()
set l =
Line (Gauge C,n),
i;
set f =
Y_axis (Line (Gauge C,n),i);
let j1,
j2 be
Element of
NAT ;
SEQM_3:def 1 ( not j1 in K1((Y_axis (Line (Gauge C,n),i))) or not j2 in K1((Y_axis (Line (Gauge C,n),i))) or j2 <= j1 or not K394((Y_axis (Line (Gauge C,n),i)),j2) <= K394((Y_axis (Line (Gauge C,n),i)),j1) )
assume that A3:
j1 in dom (Y_axis (Line (Gauge C,n),i))
and A4:
j2 in dom (Y_axis (Line (Gauge C,n),i))
and A5:
j1 < j2
;
not K394((Y_axis (Line (Gauge C,n),i)),j2) <= K394((Y_axis (Line (Gauge C,n),i)),j1)
len (Line (Gauge C,n),i) = width (Gauge C,n)
by MATRIX_1:def 8;
then A6:
dom (Line (Gauge C,n),i) = Seg (width (Gauge C,n))
by FINSEQ_1:def 3;
A7:
dom (Y_axis (Line (Gauge C,n),i)) = dom (Line (Gauge C,n),i)
by SPRECT_2:20;
then A8:
(Line (Gauge C,n),i) /. j1 =
(Line (Gauge C,n),i) . j1
by A3, PARTFUN1:def 8
.=
(Gauge C,n) * i,
j1
by A3, A6, A7, MATRIX_1:def 8
;
A9:
[i,j1] in Indices (Gauge C,n)
by A1, A2, A3, A6, A7, ZFMISC_1:106;
A10:
(Line (Gauge C,n),i) /. j2 =
(Line (Gauge C,n),i) . j2
by A4, A7, PARTFUN1:def 8
.=
(Gauge C,n) * i,
j2
by A4, A6, A7, MATRIX_1:def 8
;
A11:
[i,j2] in Indices (Gauge C,n)
by A1, A2, A4, A6, A7, ZFMISC_1:106;
set x =
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2));
set d =
((N-bound C) - (S-bound C)) / (2 |^ n);
A12:
(Y_axis (Line (Gauge C,n),i)) . j1 =
((Line (Gauge C,n),i) /. j1) `2
by A3, GOBOARD1:def 4
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2)))]| `2
by A8, A9, Def1
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2))
by EUCLID:56
;
A13:
(Y_axis (Line (Gauge C,n),i)) . j2 =
((Line (Gauge C,n),i) /. j2) `2
by A4, GOBOARD1:def 4
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)))]| `2
by A10, A11, Def1
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2))
by EUCLID:56
;
N-bound C > S-bound C
by Th12;
then A14:
(N-bound C) - (S-bound C) > 0
by XREAL_1:52;
2
|^ n > 0
by NEWTON:102;
then A15:
((N-bound C) - (S-bound C)) / (2 |^ n) > 0
by A14, XREAL_1:141;
j1 - 2
< j2 - 2
by A5, XREAL_1:11;
then
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2) < (((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)
by A15, XREAL_1:70;
hence
(Y_axis (Line (Gauge C,n),i)) . j1 < (Y_axis (Line (Gauge C,n),i)) . j2
by A12, A13, XREAL_1:10;
verum
end;
let j be Element of NAT ; GOBOARD1:def 9 ( not j in Seg (width (Gauge C,n)) or not X_axis (Col (Gauge C,n),j) is V74() )
assume A16:
j in Seg (width (Gauge C,n))
; X_axis (Col (Gauge C,n),j) is V74()
set c = Col (Gauge C,n),j;
set f = X_axis (Col (Gauge C,n),j);
let i1 be Element of NAT ; SEQM_3:def 1 for b1 being Element of NAT holds
( not i1 in K1((X_axis (Col (Gauge C,n),j))) or not b1 in K1((X_axis (Col (Gauge C,n),j))) or b1 <= i1 or not K394((X_axis (Col (Gauge C,n),j)),b1) <= K394((X_axis (Col (Gauge C,n),j)),i1) )
let i2 be Element of NAT ; ( not i1 in K1((X_axis (Col (Gauge C,n),j))) or not i2 in K1((X_axis (Col (Gauge C,n),j))) or i2 <= i1 or not K394((X_axis (Col (Gauge C,n),j)),i2) <= K394((X_axis (Col (Gauge C,n),j)),i1) )
assume that
A17:
i1 in dom (X_axis (Col (Gauge C,n),j))
and
A18:
i2 in dom (X_axis (Col (Gauge C,n),j))
and
A19:
i1 < i2
; not K394((X_axis (Col (Gauge C,n),j)),i2) <= K394((X_axis (Col (Gauge C,n),j)),i1)
len (Col (Gauge C,n),j) = len (Gauge C,n)
by MATRIX_1:def 9;
then A20:
dom (Col (Gauge C,n),j) = dom (Gauge C,n)
by FINSEQ_3:31;
A21:
dom (X_axis (Col (Gauge C,n),j)) = dom (Col (Gauge C,n),j)
by SPRECT_2:19;
then A22: (Col (Gauge C,n),j) /. i1 =
(Col (Gauge C,n),j) . i1
by A17, PARTFUN1:def 8
.=
(Gauge C,n) * i1,j
by A17, A20, A21, MATRIX_1:def 9
;
A23:
[i1,j] in Indices (Gauge C,n)
by A1, A16, A17, A20, A21, ZFMISC_1:106;
A24: (Col (Gauge C,n),j) /. i2 =
(Col (Gauge C,n),j) . i2
by A18, A21, PARTFUN1:def 8
.=
(Gauge C,n) * i2,j
by A18, A20, A21, MATRIX_1:def 9
;
A25:
[i2,j] in Indices (Gauge C,n)
by A1, A16, A18, A20, A21, ZFMISC_1:106;
set y = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2));
set d = ((E-bound C) - (W-bound C)) / (2 |^ n);
A26: (X_axis (Col (Gauge C,n),j)) . i1 =
((Col (Gauge C,n),j) /. i1) `1
by A17, GOBOARD1:def 3
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `1
by A22, A23, Def1
.=
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))
by EUCLID:56
;
A27: (X_axis (Col (Gauge C,n),j)) . i2 =
((Col (Gauge C,n),j) /. i2) `1
by A18, GOBOARD1:def 3
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `1
by A24, A25, Def1
.=
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))
by EUCLID:56
;
E-bound C > W-bound C
by Th11;
then A28:
(E-bound C) - (W-bound C) > 0
by XREAL_1:52;
2 |^ n > 0
by NEWTON:102;
then A29:
((E-bound C) - (W-bound C)) / (2 |^ n) > 0
by A28, XREAL_1:141;
i1 - 2 < i2 - 2
by A19, XREAL_1:11;
then
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2) < (((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2)
by A29, XREAL_1:70;
hence
(X_axis (Col (Gauge C,n),j)) . i1 < (X_axis (Col (Gauge C,n),j)) . i2
by A26, A27, XREAL_1:10; verum