set M = Gauge (C,n);
A1:
Indices (Gauge (C,n)) = [:(dom (Gauge (C,n))),(Seg (width (Gauge (C,n)))):]
by MATRIX_0:def 4;
thus
Gauge (C,n) is Y_increasing-in-line
Gauge (C,n) is X_increasing-in-column proof
let i be
Nat;
GOBOARD1:def 6 ( not i in dom (Gauge (C,n)) or not Y_axis (Line ((Gauge (C,n)),i)) is V57() )
assume A2:
i in dom (Gauge (C,n))
;
Y_axis (Line ((Gauge (C,n)),i)) is V57()
set l =
Line (
(Gauge (C,n)),
i);
set f =
Y_axis (Line ((Gauge (C,n)),i));
let j1,
j2 be
Nat;
SEQM_3:def 1 ( not j1 in K65((Y_axis (Line ((Gauge (C,n)),i)))) or not j2 in K65((Y_axis (Line ((Gauge (C,n)),i)))) or j2 <= j1 or not (Y_axis (Line ((Gauge (C,n)),i))) . j2 <= (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 (Y_axis (Line ((Gauge (C,n)),i))) . j2 <= (Y_axis (Line ((Gauge (C,n)),i))) . j1
len (Line ((Gauge (C,n)),i)) = width (Gauge (C,n))
by MATRIX_0:def 7;
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:16;
then A8:
(Line ((Gauge (C,n)),i)) /. j1 =
(Line ((Gauge (C,n)),i)) . j1
by A3, PARTFUN1:def 6
.=
(Gauge (C,n)) * (
i,
j1)
by A3, A6, A7, MATRIX_0:def 7
;
A9:
[i,j1] in Indices (Gauge (C,n))
by A1, A2, A3, A6, A7, ZFMISC_1:87;
A10:
(Line ((Gauge (C,n)),i)) /. j2 =
(Line ((Gauge (C,n)),i)) . j2
by A4, A7, PARTFUN1:def 6
.=
(Gauge (C,n)) * (
i,
j2)
by A4, A6, A7, MATRIX_0:def 7
;
A11:
[i,j2] in Indices (Gauge (C,n))
by A1, A2, A4, A6, A7, ZFMISC_1:87;
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 2
.=
|[((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:52
;
A13:
(Y_axis (Line ((Gauge (C,n)),i))) . j2 =
((Line ((Gauge (C,n)),i)) /. j2) `2
by A4, GOBOARD1:def 2
.=
|[((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:52
;
N-bound C > S-bound C
by Th9;
then A14:
(N-bound C) - (S-bound C) > 0
by XREAL_1:50;
2
|^ n > 0
by NEWTON:83;
then A15:
((N-bound C) - (S-bound C)) / (2 |^ n) > 0
by A14, XREAL_1:139;
j1 - 2
< j2 - 2
by A5, XREAL_1:9;
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:68;
hence
(Y_axis (Line ((Gauge (C,n)),i))) . j1 < (Y_axis (Line ((Gauge (C,n)),i))) . j2
by A12, A13, XREAL_1:8;
verum
end;
let j be Nat; GOBOARD1:def 7 ( not j in Seg (width (Gauge (C,n))) or not X_axis (Col ((Gauge (C,n)),j)) is V57() )
assume A16:
j in Seg (width (Gauge (C,n)))
; X_axis (Col ((Gauge (C,n)),j)) is V57()
set c = Col ((Gauge (C,n)),j);
set f = X_axis (Col ((Gauge (C,n)),j));
let i1 be Nat; SEQM_3:def 1 for b1 being set holds
( not i1 in K65((X_axis (Col ((Gauge (C,n)),j)))) or not b1 in K65((X_axis (Col ((Gauge (C,n)),j)))) or b1 <= i1 or not (X_axis (Col ((Gauge (C,n)),j))) . b1 <= (X_axis (Col ((Gauge (C,n)),j))) . i1 )
let i2 be Nat; ( not i1 in K65((X_axis (Col ((Gauge (C,n)),j)))) or not i2 in K65((X_axis (Col ((Gauge (C,n)),j)))) or i2 <= i1 or not (X_axis (Col ((Gauge (C,n)),j))) . i2 <= (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 (X_axis (Col ((Gauge (C,n)),j))) . i2 <= (X_axis (Col ((Gauge (C,n)),j))) . i1
len (Col ((Gauge (C,n)),j)) = len (Gauge (C,n))
by MATRIX_0:def 8;
then A20:
dom (Col ((Gauge (C,n)),j)) = dom (Gauge (C,n))
by FINSEQ_3:29;
A21:
dom (X_axis (Col ((Gauge (C,n)),j))) = dom (Col ((Gauge (C,n)),j))
by SPRECT_2:15;
then A22: (Col ((Gauge (C,n)),j)) /. i1 =
(Col ((Gauge (C,n)),j)) . i1
by A17, PARTFUN1:def 6
.=
(Gauge (C,n)) * (i1,j)
by A17, A20, A21, MATRIX_0:def 8
;
A23:
[i1,j] in Indices (Gauge (C,n))
by A1, A16, A17, A20, A21, ZFMISC_1:87;
A24: (Col ((Gauge (C,n)),j)) /. i2 =
(Col ((Gauge (C,n)),j)) . i2
by A18, A21, PARTFUN1:def 6
.=
(Gauge (C,n)) * (i2,j)
by A18, A20, A21, MATRIX_0:def 8
;
A25:
[i2,j] in Indices (Gauge (C,n))
by A1, A16, A18, A20, A21, ZFMISC_1:87;
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 1
.=
|[((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:52
;
A27: (X_axis (Col ((Gauge (C,n)),j))) . i2 =
((Col ((Gauge (C,n)),j)) /. i2) `1
by A18, GOBOARD1:def 1
.=
|[((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:52
;
E-bound C > W-bound C
by Th8;
then A28:
(E-bound C) - (W-bound C) > 0
by XREAL_1:50;
2 |^ n > 0
by NEWTON:83;
then A29:
((E-bound C) - (W-bound C)) / (2 |^ n) > 0
by A28, XREAL_1:139;
i1 - 2 < i2 - 2
by A19, XREAL_1:9;
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:68;
hence
(X_axis (Col ((Gauge (C,n)),j))) . i1 < (X_axis (Col ((Gauge (C,n)),j))) . i2
by A26, A27, XREAL_1:8; verum