let n be Nat; for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
let K be Field; for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
let A, B be Matrix of K; for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
let nt be Element of n -tuples_on NAT; ( rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) implies Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) )
assume that
A1:
rng nt c= dom A
and
A2:
dom A = dom B
and
A3:
n > 0
and
A4:
for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) )
; Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
set SB = Segm (B,nt,(Sgm (Seg (width B))));
set SA = Segm (A,nt,(Sgm (Seg (width A))));
A5:
Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) c= Solutions_of (A,B)
proof
A6:
Seg (len A) = dom B
by A2, FINSEQ_1:def 3;
A7:
width (Segm (B,nt,(Sgm (Seg (width B))))) = card (Seg (width B))
by A3, MATRIX_0:23;
then A8:
width (Segm (B,nt,(Sgm (Seg (width B))))) = width B
by FINSEQ_1:57;
let x be
object ;
TARSKI:def 3 ( not x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) or x in Solutions_of (A,B) )
assume
x in Solutions_of (
(Segm (A,nt,(Sgm (Seg (width A))))),
(Segm (B,nt,(Sgm (Seg (width B))))))
;
x in Solutions_of (A,B)
then consider X being
Matrix of
K such that A9:
x = X
and A10:
len X = width (Segm (A,nt,(Sgm (Seg (width A)))))
and A11:
width X = width (Segm (B,nt,(Sgm (Seg (width B)))))
and A12:
(Segm (A,nt,(Sgm (Seg (width A))))) * X = Segm (
B,
nt,
(Sgm (Seg (width B))))
;
set AX =
A * X;
width (Segm (A,nt,(Sgm (Seg (width A))))) = card (Seg (width A))
by A3, MATRIX_0:23;
then A13:
width (Segm (A,nt,(Sgm (Seg (width A))))) = width A
by FINSEQ_1:57;
then A14:
width (A * X) = width X
by A10, MATRIX_3:def 4;
A15:
len (A * X) = len A
by A10, A13, MATRIX_3:def 4;
A16:
now for j, k being Nat st [j,k] in Indices (A * X) holds
(A * X) * (j,k) = B * (j,k)A17:
dom (A * X) = Seg (len A)
by A15, FINSEQ_1:def 3;
let j,
k be
Nat;
( [j,k] in Indices (A * X) implies (A * X) * (j,k) = B * (j,k) )assume A18:
[j,k] in Indices (A * X)
;
(A * X) * (j,k) = B * (j,k)A19:
k in Seg (width (A * X))
by A18, ZFMISC_1:87;
reconsider j9 =
j,
k9 =
k as
Element of
NAT by ORDINAL1:def 12;
A20:
j in dom (A * X)
by A18, ZFMISC_1:87;
now (A * X) * (j,k) = B * (j,k)per cases
( j9 in rng nt or not j9 in rng nt )
;
suppose A21:
j9 in rng nt
;
(A * X) * (j,k) = B * (j,k)A22:
dom nt = Seg n
by FINSEQ_2:124;
Sgm (Seg (width B)) = idseq (width B)
by FINSEQ_3:48;
then A23:
(Sgm (Seg (width B))) . k9 = k
by A11, A8, A14, A19, FINSEQ_2:49;
consider p being
object such that A24:
p in dom nt
and A25:
nt . p = j9
by A21, FUNCT_1:def 3;
reconsider p =
p as
Element of
NAT by A24;
Indices (Segm (B,nt,(Sgm (Seg (width B))))) = [:(Seg n),(Seg (card (Seg (width B)))):]
by A3, MATRIX_0:23;
then A26:
[p,k] in Indices (Segm (B,nt,(Sgm (Seg (width B)))))
by A11, A7, A14, A19, A24, A22, ZFMISC_1:87;
Line (
(Segm (A,nt,(Sgm (Seg (width A))))),
p)
= Line (
A,
j9)
by A24, A25, A22, Lm6;
hence (A * X) * (
j,
k) =
(Line ((Segm (A,nt,(Sgm (Seg (width A))))),p)) "*" (Col (X,k))
by A10, A13, A18, MATRIX_3:def 4
.=
(Segm (B,nt,(Sgm (Seg (width B))))) * (
p,
k9)
by A10, A12, A26, MATRIX_3:def 4
.=
B * (
j,
k)
by A25, A26, A23, MATRIX13:def 1
;
verum end; suppose
not
j9 in rng nt
;
(A * X) * (j,k) = B * (j,k)then A27:
j9 in (dom A) \ (rng nt)
by A2, A6, A20, A17, XBOOLE_0:def 5;
then A28:
Line (
B,
j)
= (width B) |-> (0. K)
by A4;
Line (
A,
j)
= (width A) |-> (0. K)
by A4, A27;
hence (A * X) * (
j,
k) =
((width A) |-> (0. K)) "*" (Col (X,k))
by A10, A13, A18, MATRIX_3:def 4
.=
Sum ((0. K) * (Col (X,k)))
by A10, A13, FVSUM_1:66
.=
(0. K) * (Sum (Col (X,k)))
by FVSUM_1:73
.=
0. K
.=
(Line (B,j)) . k
by A11, A8, A14, A19, A28, FINSEQ_2:57
.=
B * (
j,
k)
by A11, A8, A14, A19, MATRIX_0:def 7
;
verum end; end; end; hence
(A * X) * (
j,
k)
= B * (
j,
k)
;
verum end;
len (A * X) = len B
by A15, A6, FINSEQ_1:def 3;
then
A * X = B
by A11, A7, A14, A16, FINSEQ_1:57, MATRIX_0:21;
hence
x in Solutions_of (
A,
B)
by A9, A10, A11, A13, A8;
verum
end;
Solutions_of (A,B) c= Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
by A1, A3, Th42;
hence
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
by A5; verum