let n be Element of NAT ; :: thesis: for K being Field
for a being Element of K
for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * 1,1 = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq K,n,i ) & Q * 1,1 = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * 1,j = - (a * (P * 1,j)) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq K,n,i ) holds
( P is invertible & Q = P ~ )
let K be Field; :: thesis: for a being Element of K
for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * 1,1 = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq K,n,i ) & Q * 1,1 = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * 1,j = - (a * (P * 1,j)) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq K,n,i ) holds
( P is invertible & Q = P ~ )
let a be Element of K; :: thesis: for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * 1,1 = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq K,n,i ) & Q * 1,1 = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * 1,j = - (a * (P * 1,j)) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq K,n,i ) holds
( P is invertible & Q = P ~ )
let P, Q be Matrix of n,K; :: thesis: ( n > 0 & a <> 0. K & P * 1,1 = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq K,n,i ) & Q * 1,1 = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * 1,j = - (a * (P * 1,j)) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq K,n,i ) implies ( P is invertible & Q = P ~ ) )
assume A1: ( n > 0 & a <> 0. K & P * 1,1 = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq K,n,i ) & Q * 1,1 = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * 1,j = - (a * (P * 1,j)) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq K,n,i ) ) ; :: thesis: ( P is invertible & Q = P ~ )
then A40: 0 + 1 <= n by NAT_1:13;
A1b: for j being Element of NAT st 1 < j & j <= n holds
P * 1,j = - ((a " ) * (Q * 1,j))

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies P * 1,j = - ((a " ) * (Q * 1,j)) )
assume B1: ( 1 < j & j <= n ) ; :: thesis: P * 1,j = - ((a " ) * (Q * 1,j))
D3: - ((a " ) * (Q * 1,j)) = - ((a " ) * (- (a * (P * 1,j)))) by A1, B1;
D4: - ((a " ) * (Q * 1,j)) = - ((a " ) * ((- a) * (P * 1,j))) by D3, VECTSP_1:41;
D5: - ((a " ) * (Q * 1,j)) = (- (a " )) * ((- a) * (P * 1,j)) by D4, VECTSP_1:41;
D6: - ((a " ) * (Q * 1,j)) = ((- (a " )) * (- a)) * (P * 1,j) by D5, GROUP_1:def 4;
D8: - ((a " ) * (Q * 1,j)) = (a * (a " )) * (P * 1,j) by D6, VECTSP_1:42;
- ((a " ) * (Q * 1,j)) = (1. K) * (P * 1,j) by A1, D8, VECTSP_1:def 22;
hence P * 1,j = - ((a " ) * (Q * 1,j)) by VECTSP_1:def 16; :: thesis: verum

end;

A2d: ( len Q = n & width Q = n ) by MATRIX_1:25;
A2a: ( len P = n & width P = n ) by MATRIX_1:25;
A2: len (Line P,1) = n by A2a, MATRIX_1:def 8;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A20: len (Col Q,1) = len Q by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
A21: len (a * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
for k being Nat st 1 <= k & k <= n holds
(Col Q,1) . k = (a * (Base_FinSeq K,n,1)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Col Q,1) . k = (a * (Base_FinSeq K,n,1)) . k )
assume B1: ( 1 <= k & k <= n ) ; :: thesis: (Col Q,1) . k = (a * (Base_FinSeq K,n,1)) . k
B: k in NAT by ORDINAL1:def 13;
B2: k in Seg n by B1, FINSEQ_1:3;
B3: k in dom Q by A2d, B2, FINSEQ_1:def 3;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by B1, A2b, FINSEQ_4:24;
A13a: 1 <= n by B1, XXREAL_0:2;
B11: 1 in dom Q by A2d, A13a, FINSEQ_3:27;
B92: k in dom (a * (Base_FinSeq K,n,1)) by A21, B1, FINSEQ_3:27;

B5: now

assume C0: k <> 1 ; :: thesis: (a * (Base_FinSeq K,n,1)) . k = 0. K
thus (a * (Base_FinSeq K,n,1)) . k = a * ((Base_FinSeq K,n,1) /. k) by B92, A13, FVSUM_1:62
.= a * (0. K) by A13, AA1120, B1, C0, A13a
.= 0. K by VECTSP_1:36 ; :: thesis: verum

end;

B6: now

assume C0: k = 1 ; :: thesis: (a * (Base_FinSeq K,n,1)) . k = a
thus (a * (Base_FinSeq K,n,1)) . k = a * ((Base_FinSeq K,n,1) /. k) by B92, A13, FVSUM_1:62
.= a * (1. K) by AA1110, C0, B1, A13
.= a by VECTSP_1:def 16 ; :: thesis: verum

end;

now

assume B20: k <> 1 ; :: thesis: (Col Q,1) . k = 0. K
then B19: 1 < k by B1, XXREAL_0:1;
[k,1] in Indices Q by B1, A40, MATRIX_1:38;
then consider p being FinSequence of K such that
C3: ( p = Q . k & Q * k,1 = p . 1 ) by MATRIX_1:def 6;
Q * k,1 = (Base_FinSeq K,n,k) . 1 by C3, B19, B1, A1, B
.= 0. K by B20, B1, A40, AA1120 ;
hence (Col Q,1) . k = 0. K by B3, MATRIX_1:def 9; :: thesis: verum

end;

hence (Col Q,1) . k = (a * (Base_FinSeq K,n,1)) . k by B5, B6, B11, A1, MATRIX_1:def 9; :: thesis: verum

end;

then A3: Col Q,1 = a * (Base_FinSeq K,n,1) by A20, A21, FINSEQ_1:18;
A4: 0 + 1 <= n by A1, NAT_1:13;
then A10: 1 in Seg (width P) by A2a, FINSEQ_1:3;
A11: 1 in Seg (len P) by A2a, A4, FINSEQ_1:3;
K1: 1 in dom P by A11, FINSEQ_1:def 3;
K3: len (a * (Line P,1)) = len (Line P,1) by MATRIXR1:16
.= n by A2a, MATRIX_1:def 8 ;
K4: 1 in dom (Line P,1) by A11, A2a, A2, FINSEQ_1:def 3;
A8d: Indices Q = [:(Seg n),(Seg n):] by MATRIX_1:25;
A8: Indices P = [:(Seg n),(Seg n):] by MATRIX_1:25;
A12: [1,1] in Indices P by A4, MATRIX_1:38;
A18: Indices (P * Q) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A13: (P * Q) * 1,1 = |((Line P,1),(Col Q,1))| by A12, A8, A2d, A2a, MATRIX_3:def 4
.= a * |((Line P,1),(Base_FinSeq K,n,1))| by A3, BB246, A2, A2b
.= a * ((Line P,1) /. 1) by AA2627, A2, A4
.= (a * (Line P,1)) /. 1 by K4, POLYNOM1:def 2
.= (a * (Line P,1)) . 1 by K3, A4, FINSEQ_4:24
.= a * (P * 1,1) by K1, A10, MATRIX12:3
.= 1. K by A1, VECTSP_1:def 22 ;
A14: for j being Element of NAT st 1 < j & j <= n holds
(P * Q) * 1,j = 0. K

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies (P * Q) * 1,j = 0. K )
assume B1: ( 1 < j & j <= n ) ; :: thesis: (P * Q) * 1,j = 0. K
then B20: j in Seg n by FINSEQ_1:3;
A22: [1,j] in Indices (P * Q) by B1, A4, MATRIX_1:38;
B3: len (Col Q,j) = len Q by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) = len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
reconsider p = Col Q,j, q = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
A21b: len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
A4: 0 + 1 <= n by C0, NAT_1:13;
B92: k in dom ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) by A21b, C0, FINSEQ_3:27;
C12: k in dom Q by C0, A2d, FINSEQ_3:27;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by B92, A13, FVSUM_1:62 ;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

D2: p . k = Q * 1,j by C12, D0, MATRIX_1:def 9
.= - (a * (P * 1,j)) by A1, B1 ;
D1: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (a * (P * 1,j))) * (1_ K) by D0, AA1110, C0, E1, C4
.= - (a * (P * 1,j)) by GROUP_1:def 5 ;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0 ;
K1a: q . k = ((- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k) + (0. K) by BB120, B4, B5b, C0, K1;
q . k = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k by K1a, RLVECT_1:10;
hence p . k = q . k by D2, D1, B4, C0, FINSEQ_4:24; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices Q by B1, C0, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = Q . k & Q * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = p2 . j by D3, C12, MATRIX_1:def 9
.= (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B ;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

(- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, B4, C0, FINSEQ_4:24
.= (- (a * (P * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1
.= 0. K by VECTSP_1:36 ;
then q . k = (0. K) + ((Base_FinSeq K,n,j) /. k) by BB120, B4, B5b, C0
.= (Base_FinSeq K,n,j) /. k by RLVECT_1:10
.= (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
hence p . k = q . k by D2, AA1120, B1, C0, E0; :: thesis: verum

end;

suppose E0: k = j ; :: thesis: p . k = q . k

(- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, B4, C0, FINSEQ_4:24
.= (- (a * (P * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1
.= 0. K by VECTSP_1:36 ;
then q . k = (0. K) + ((Base_FinSeq K,n,j) /. k) by BB120, B4, B5b, C0
.= (Base_FinSeq K,n,j) /. k by RLVECT_1:10
.= (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 1. K by AA1110, C0, E0 ;
hence p . k = q . k by D2, AA1110, C0, E0; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then B7: Col Q,j = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
A2a: ( len P = n & width P = n ) by MATRIX_1:25;
K2: len (Line P,1) = n by A2a, MATRIX_1:def 8;
K3: (Line P,1) /. j = (Line P,1) . j by K2, B1, FINSEQ_4:24
.= P * 1,j by B20, A2a, MATRIX_1:def 8 ;
K0: (Line P,1) /. 1 = (Line P,1) . 1 by K2, A4, FINSEQ_4:24
.= a " by A1, A10, MATRIX_1:def 8 ;
(P * Q) * 1,j = |((Line P,1),(Col Q,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line P,1),(- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line P,1),(Base_FinSeq K,n,j))| by BB248, B4, A2, B7, B5b
.= |((Line P,1),((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line P,1),(Base_FinSeq K,n,j))| by BB200
.= ((- (a * (P * 1,j))) * |((Line P,1),(Base_FinSeq K,n,1))|) + |((Line P,1),(Base_FinSeq K,n,j))| by BB246, A2, A2b
.= ((- (a * (P * 1,j))) * (a " )) + |((Line P,1),(Base_FinSeq K,n,j))| by K0, AA2627, A2, A4
.= (- ((a * (P * 1,j)) * (a " ))) + |((Line P,1),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((P * 1,j) * (a * (a " )))) + |((Line P,1),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((P * 1,j) * (1_ K))) + |((Line P,1),(Base_FinSeq K,n,j))| by A1, VECTSP_1:def 22
.= (- ((P * 1,j) * (1. K))) + ((Line P,1) /. j) by AA2627, B1, A2
.= (- (P * 1,j)) + (P * 1,j) by K3, VECTSP_1:def 16
.= 0. K by RLVECT_1:16 ;
hence (P * Q) * 1,j = 0. K ; :: thesis: verum

end;

A15: for i, j being Element of NAT st 1 < i & i <= n & 1 <= j & j <= n & i <> j holds
(P * Q) * i,j = 0. K

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & 1 <= j & j <= n & i <> j implies (P * Q) * i,j = 0. K )
assume B1: ( 1 < i & i <= n & 1 <= j & j <= n & i <> j ) ; :: thesis: (P * Q) * i,j = 0. K
then B20: ( i in Seg n & j in Seg n ) by FINSEQ_1:3;
B2: [i,j] in Indices P by B1, MATRIX_1:38;
A22: [i,j] in Indices (P * Q) by B1, MATRIX_1:38;
A23b: [i,1] in Indices P by B1, A40, MATRIX_1:38;
B3: len (Col Q,j) = len Q by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) = len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
B4b: len (a * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;

now

per cases ( j > 1 or j <= 1 ) ;

suppose F0: j > 1 ; :: thesis: (P * Q) * i,j = 0. K

reconsider p = Col Q,j, q = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
C10a: len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B92b: k in dom ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) by C0, C10a, FINSEQ_3:27;
C12: k in dom Q by C0, A2d, FINSEQ_3:27;
C2: p . k = Q * k,j by C12, MATRIX_1:def 9;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by B92b, A13, FVSUM_1:62 ;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

K3: ( 1 <= k & k <= len (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) ) by C0, C10a, BB200;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0, F0 ;
K2: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, K3, FINSEQ_4:24
.= (- (a * (P * 1,j))) * (1. K) by D0, AA1110, A4, E1 ;
q . k = ((- (a * (P * 1,j))) * (1. K)) + (0. K) by BB120, B4, B5b, C0, K2, K1
.= (- (a * (P * 1,j))) * (1_ K) by RLVECT_1:10
.= - (a * (P * 1,j)) by GROUP_1:def 5 ;
hence p . k = q . k by A1, B1, F0, C2, D0; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices Q by C0, B1, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = Q . k & Q * k,j = p2 . j ) by MATRIX_1:def 6;
K3: ( 1 <= k & k <= len (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) ) by C0, C10a, BB200;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B, C2;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

E4: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (a * (P * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1, C4
.= 0. K by VECTSP_1:36 ;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
K2: q . k = ((- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k) + (0. K) by BB120, B4, B5b, C0, K1;
q . k = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k by K2, RLVECT_1:10
.= (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k by K3, FINSEQ_4:24 ;
hence p . k = q . k by D2, AA1120, B1, C0, E0, E4; :: thesis: verum

end;

suppose E0: k = j ; :: thesis: p . k = q . k

then E2: p . k = 1. K by D2, AA1110, C0;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 1. K by AA1110, C0, E0 ;
K2: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (a * (P * 1,j))) * (0. K) by D0, AA1120, A4, C0, A13, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (1. K) by E3, BB120, B4, B5b, C0, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then B7: Col Q,j = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
A2a: ( len P = n & width P = n ) by MATRIX_1:25;
K2: len (Line P,i) = n by A2a, MATRIX_1:def 8;
K3: (Line P,i) /. j = (Line P,i) . j by K2, B1, FINSEQ_4:24
.= P * i,j by B20, A2a, MATRIX_1:def 8 ;
K0: (Line P,i) /. 1 = (Line P,i) . 1 by K2, A4, FINSEQ_4:24
.= P * i,1 by A10, MATRIX_1:def 8 ;
B18: 1 <= n by B1, XXREAL_0:2;
B28: (P * Q) * i,j = |((Line P,i),(Col Q,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line P,i),(- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line P,i),(Base_FinSeq K,n,j))| by BB248, B4, K2, B7, B5b
.= |((Line P,i),((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line P,i),(Base_FinSeq K,n,j))| by BB200
.= ((- (a * (P * 1,j))) * |((Line P,i),(Base_FinSeq K,n,1))|) + |((Line P,i),(Base_FinSeq K,n,j))| by BB246, K2, A2b
.= ((- (a * (P * 1,j))) * (P * i,1)) + |((Line P,i),(Base_FinSeq K,n,j))| by K0, AA2627, K2, A4
.= (- ((a * (P * 1,j)) * (P * i,1))) + |((Line P,i),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((P * 1,j) * (a * (P * i,1)))) + |((Line P,i),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((P * 1,j) * (a * (P * i,1)))) + (P * i,j) by K3, AA2627, B1, K2 ;
consider p1 being FinSequence of K such that
A97: ( p1 = P . i & P * i,j = p1 . j ) by B2, MATRIX_1:def 6;
p1 = Base_FinSeq K,n,i by A1, A97, B1;
then A98: p1 . j = 0. K by AA1120, B1;
consider p2 being FinSequence of K such that
A99: ( p2 = P . i & P * i,1 = p2 . 1 ) by A23b, MATRIX_1:def 6;
K2: p2 = Base_FinSeq K,n,i by A1, A99, B1;
(P * Q) * i,j = (- ((P * 1,j) * (a * (0. K)))) + (P * i,j) by B28, A99, AA1120, B18, B1, K2
.= (- ((P * 1,j) * (0. K))) + (P * i,j) by VECTSP_1:36
.= (- (0. K)) + (P * i,j) by VECTSP_1:36
.= (0. K) + (0. K) by A97, A98, RLVECT_1:25
.= 0. K by RLVECT_1:10 ;
hence (P * Q) * i,j = 0. K ; :: thesis: verum

end;

suppose F1: j <= 1 ; :: thesis: (P * Q) * i,j = 0. K

reconsider p = Col Q,j, q = a * (Base_FinSeq K,n,1) as FinSequence of K ;
F2: for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
B92: k in dom (a * (Base_FinSeq K,n,1)) by A21, C0, FINSEQ_3:27;
C12: k in dom Q by C0, A2d, FINSEQ_3:27;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (a * (Base_FinSeq K,n,1)) . k = a * ((Base_FinSeq K,n,1) /. k) by B92, A13, FVSUM_1:62;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

D2: p . k = Q * 1,j by C12, D0, MATRIX_1:def 9
.= a by A1, F1, B1, XXREAL_0:1 ;
q . k = a * (1. K) by C4, D0, AA1110, C0, A13
.= a by VECTSP_1:def 16 ;
hence p . k = q . k by D2; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices Q by B1, C0, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = Q . k & Q * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = Q * k,j by C12, MATRIX_1:def 9
.= (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B ;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
A13a: 1 <= n by C0, XXREAL_0:2;
a * ((Base_FinSeq K,n,1) /. k) = a * (0. K) by A13, AA1120, D0, C0, A13a
.= 0. K by VECTSP_1:36 ;
hence p . k = q . k by E0, D2, AA1120, B1, C0, C4; :: thesis: verum

end;

suppose k = j ; :: thesis: p . k = q . k

hence p . k = q . k by F1, D0; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

A2x: len (Line P,i) = n by A2a, MATRIX_1:def 8;
K0: (Line P,i) /. 1 = (Line P,i) . 1 by A2x, A4, FINSEQ_4:24
.= P * i,1 by A10, MATRIX_1:def 8 ;
B18: 1 <= n by B1, XXREAL_0:2;
B28: (P * Q) * i,j = |((Line P,i),(Col Q,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line P,i),(a * (Base_FinSeq K,n,1)))| by F2, B3, B4b, FINSEQ_1:18
.= a * |((Line P,i),(Base_FinSeq K,n,1))| by BB246, A2x, A2b
.= a * (P * i,1) by K0, AA2627, A2x, A4 ;
consider p2 being FinSequence of K such that
A99: ( p2 = P . i & P * i,1 = p2 . 1 ) by A23b, MATRIX_1:def 6;
p2 = Base_FinSeq K,n,i by A1, A99, B1;
hence (P * Q) * i,j = a * (0. K) by B28, A99, AA1120, B18, B1
.= 0. K by VECTSP_1:36 ;
:: thesis: verum

end;

end;

end;

hence (P * Q) * i,j = 0. K ; :: thesis: verum

end;

A85: for i, j being Element of NAT st 1 < i & i <= n & i = j holds
(P * Q) * i,j = 1. K

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & i = j implies (P * Q) * i,j = 1. K )
assume B1: ( 1 < i & i <= n & i = j ) ; :: thesis: (P * Q) * i,j = 1. K
then B20: ( i in Seg n & j in Seg n ) by FINSEQ_1:3;
B2: [i,j] in Indices P by B1, MATRIX_1:38;
A22: [i,j] in Indices (P * Q) by B1, MATRIX_1:38;
A23b: [i,1] in Indices P by B1, A40, MATRIX_1:38;
B3: len (Col Q,j) = len Q by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) = len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
reconsider p = Col Q,j, q = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
then C10: k in Seg n by FINSEQ_1:3;
C10a: len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
A21b: len ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B92b: k in dom ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) by A21b, C0, FINSEQ_3:27;
C12: k in dom Q by C0, A2d, FINSEQ_3:27;
C2: p . k = Q * k,j by C12, MATRIX_1:def 9;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by B92b, A13, FVSUM_1:62 ;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

K3: ( 1 <= k & k <= len (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) ) by C0, C10a, BB200;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0 ;
K2: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (a * (P * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, K3, FINSEQ_4:24
.= (- (a * (P * 1,j))) * (1. K) by D0, AA1110, A4, E1 ;
q . k = ((- (a * (P * 1,j))) * (1. K)) + (0. K) by BB120, B4, B5b, C0, K2, K1
.= (- (a * (P * 1,j))) * (1. K) by RLVECT_1:10
.= - (a * (P * 1,j)) by VECTSP_1:def 16 ;
hence p . k = q . k by A1, B1, C2, D0; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices Q by A8d, B20, C10, ZFMISC_1:106;
then consider p2 being FinSequence of K such that
D3: ( p2 = Q . k & Q * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B, C2;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

then E2: p . k = 0. K by D2, AA1120, B1, C0;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
K2: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (a * (P * 1,j))) * (0. K) by D0, AA1120, A4, C0, A13, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (0. K) by E3, BB120, B4, B5b, C0, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

suppose E0: k = j ; :: thesis: p . k = q . k

then E2: p . k = 1. K by D2, AA1110, C0;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 1. K by B1, AA1110, E0 ;
K2: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (a * (P * 1,j))) * (0. K) by D0, AA1120, A4, C0, A13, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (1. K) by E3, BB120, B4, B5b, C0, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then B7: Col Q,j = (- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
A2a: ( len P = n & width P = n ) by MATRIX_1:25;
K2: len (Line P,i) = n by A2a, MATRIX_1:def 8;
K0: (Line P,i) /. j = (Line P,i) . j by K2, B1, FINSEQ_4:24
.= P * i,j by B20, A2a, MATRIX_1:def 8 ;
K3: (Line P,i) /. 1 = (Line P,i) . 1 by K2, A4, FINSEQ_4:24
.= P * i,1 by A10, MATRIX_1:def 8 ;
B18: 1 <= n by B1, XXREAL_0:2;
B28: (P * Q) * i,j = |((Line P,i),(Col Q,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line P,i),(- ((a * (P * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line P,i),(Base_FinSeq K,n,j))| by BB248, B4, K2, B7, B5b
.= |((Line P,i),((- (a * (P * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line P,i),(Base_FinSeq K,n,j))| by BB200
.= ((- (a * (P * 1,j))) * |((Line P,i),(Base_FinSeq K,n,1))|) + |((Line P,i),(Base_FinSeq K,n,j))| by BB246, K2, A2b
.= ((- (a * (P * 1,j))) * (P * i,1)) + |((Line P,i),(Base_FinSeq K,n,j))| by K3, AA2627, K2, A4
.= (- ((a * (P * 1,j)) * (P * i,1))) + |((Line P,i),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((P * 1,j) * (a * (P * i,1)))) + |((Line P,i),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((P * 1,j) * (a * (P * i,1)))) + (P * i,j) by K0, AA2627, B1, K2 ;
consider p1 being FinSequence of K such that
A97: ( p1 = P . i & P * i,j = p1 . j ) by B2, MATRIX_1:def 6;
p1 = Base_FinSeq K,n,i by A1, A97, B1;
then A98: p1 . j = 1. K by AA1110, B1;
consider p2 being FinSequence of K such that
A99: ( p2 = P . i & P * i,1 = p2 . 1 ) by A23b, MATRIX_1:def 6;
p2 = Base_FinSeq K,n,i by A1, A99, B1;
hence (P * Q) * i,j = (- ((P * 1,j) * (a * (0. K)))) + (P * i,j) by A99, B28, AA1120, B18, B1
.= (- ((P * 1,j) * (0. K))) + (P * i,j) by VECTSP_1:36
.= (- (0. K)) + (P * i,j) by VECTSP_1:36
.= (0. K) + (1. K) by A97, A98, RLVECT_1:25
.= 1. K by RLVECT_1:10 ;
:: thesis: verum

end;

for i, j being Nat st [i,j] in Indices (P * Q) holds
(P * Q) * i,j = (1. K,n) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (P * Q) implies (P * Q) * i,j = (1. K,n) * i,j )
assume [i,j] in Indices (P * Q) ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j
then B2: ( i in Seg n & j in Seg n ) by A18, ZFMISC_1:106;
then B3: ( 1 <= i & i <= n ) by FINSEQ_1:3;
B4: ( 1 <= j & j <= n ) by B2, FINSEQ_1:3;
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 13;

per cases ( 1 < i or 1 = i ) by B3, XXREAL_0:1;

suppose C0: 1 < i ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j

now

per cases ( i <> j or i = j ) ;

suppose D0: i <> j ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j

D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 0. K by AA1120, D0, B3, B4 ;
thus (P * Q) * i,j = (P * Q) * i0,j0
.= (1. K,n) * i,j by D1, C0, B3, B4, A15, D0 ; :: thesis: verum

end;

suppose D0: i = j ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j

D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 1. K by AA1110, D0, B4 ;
thus (P * Q) * i,j = (P * Q) * i0,j0
.= (1. K,n) * i,j by D1, C0, B4, A85, D0 ; :: thesis: verum

end;

end;

end;

hence (P * Q) * i,j = (1. K,n) * i,j ; :: thesis: verum

end;

suppose C0: 1 = i ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j

now

per cases ( i < j or i >= j ) ;

suppose D0: i < j ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j

D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 0. K by AA1120, B3, B4, D0 ;
thus (P * Q) * i,j = (P * Q) * i0,j0
.= (1. K,n) * i,j by D1, C0, B4, A14, D0 ; :: thesis: verum

end;

suppose D9: i >= j ; :: thesis: (P * Q) * i,j = (1. K,n) * i,j

then D0: i = j by B4, C0, XXREAL_0:1;
D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 1. K by D0, AA1110, B4 ;
thus (P * Q) * i,j = (1. K,n) * i,j by D1, C0, A13, D9, B4, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence (P * Q) * i,j = (1. K,n) * i,j ; :: thesis: verum

end;

end;

end;

then A5: P * Q = 1. K,n by MATRIX_1:28;
A2d: ( len P = n & width P = n ) by MATRIX_1:25;
A2a: ( len Q = n & width Q = n ) by MATRIX_1:25;
A2: len (Line Q,1) = n by A2a, MATRIX_1:def 8;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A20: len (Col P,1) = len P by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
A21: len ((a " ) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
for k being Nat st 1 <= k & k <= n holds
(Col P,1) . k = ((a " ) * (Base_FinSeq K,n,1)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Col P,1) . k = ((a " ) * (Base_FinSeq K,n,1)) . k )
B: k in NAT by ORDINAL1:def 13;
assume B1: ( 1 <= k & k <= n ) ; :: thesis: (Col P,1) . k = ((a " ) * (Base_FinSeq K,n,1)) . k
then B32: k in Seg n by FINSEQ_1:3;
then B3: k in dom P by A2d, FINSEQ_1:def 3;
B92: k in dom ((a " ) * (Base_FinSeq K,n,1)) by A21, B1, FINSEQ_3:27;
1 <= n by B1, XXREAL_0:2;
then B11: 1 in dom P by A2d, FINSEQ_3:27;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by B1, A2b, FINSEQ_4:24;
A13a: 1 <= n by B1, XXREAL_0:2;

B5: now

assume C0: k <> 1 ; :: thesis: ((a " ) * (Base_FinSeq K,n,1)) . k = 0. K
thus ((a " ) * (Base_FinSeq K,n,1)) . k = (a " ) * ((Base_FinSeq K,n,1) /. k) by B92, A13, FVSUM_1:62
.= (a " ) * (0. K) by A13, AA1120, B1, C0, A13a
.= 0. K by VECTSP_1:36 ; :: thesis: verum

end;

B6: now

assume C0: k = 1 ; :: thesis: ((a " ) * (Base_FinSeq K,n,1)) . k = a "
k in dom ((a " ) * (Base_FinSeq K,n,1)) by B32, A21, FINSEQ_1:def 3;
hence ((a " ) * (Base_FinSeq K,n,1)) . k = (a " ) * ((Base_FinSeq K,n,1) /. k) by A13, FVSUM_1:62
.= (a " ) * (1. K) by AA1110, C0, B1, A13
.= a " by VECTSP_1:def 16 ;
:: thesis: verum

end;

now

assume B20: k <> 1 ; :: thesis: (Col P,1) . k = 0. K
then B19: 1 < k by B1, XXREAL_0:1;
[k,1] in Indices P by B1, A40, MATRIX_1:38;
then consider p being FinSequence of K such that
C3: ( p = P . k & P * k,1 = p . 1 ) by MATRIX_1:def 6;
P * k,1 = (Base_FinSeq K,n,k) . 1 by C3, B19, B1, A1, B
.= 0. K by B20, B1, A40, AA1120 ;
hence (Col P,1) . k = 0. K by B3, MATRIX_1:def 9; :: thesis: verum

end;

hence (Col P,1) . k = ((a " ) * (Base_FinSeq K,n,1)) . k by B5, B6, B11, A1, MATRIX_1:def 9; :: thesis: verum

end;

then A3: Col P,1 = (a " ) * (Base_FinSeq K,n,1) by A20, A21, FINSEQ_1:18;
A4: 0 + 1 <= n by A1, NAT_1:13;
then A10: 1 in Seg (width Q) by A2a, FINSEQ_1:3;
A11: 1 in Seg (len Q) by A2a, A4, FINSEQ_1:3;
K1: 1 in dom Q by A11, FINSEQ_1:def 3;
K3: len ((a " ) * (Line Q,1)) = len (Line Q,1) by MATRIXR1:16
.= n by A2a, MATRIX_1:def 8 ;
K4: 1 in dom (Line Q,1) by A11, A2a, A2, FINSEQ_1:def 3;
A8d: Indices P = [:(Seg n),(Seg n):] by MATRIX_1:25;
A8: Indices Q = [:(Seg n),(Seg n):] by MATRIX_1:25;
A12: [1,1] in Indices Q by A4, MATRIX_1:38;
A18: Indices (Q * P) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A13: (Q * P) * 1,1 = |((Line Q,1),(Col P,1))| by A12, A8, A2d, A2a, MATRIX_3:def 4
.= (a " ) * |((Line Q,1),(Base_FinSeq K,n,1))| by A3, BB246, A2, A2b
.= (a " ) * ((Line Q,1) /. 1) by AA2627, A2, A4
.= ((a " ) * (Line Q,1)) /. 1 by K4, POLYNOM1:def 2
.= ((a " ) * (Line Q,1)) . 1 by K3, A4, FINSEQ_4:24
.= (a " ) * (Q * 1,1) by K1, A10, MATRIX12:3
.= 1. K by A1, VECTSP_1:def 22 ;
A14: for j being Element of NAT st 1 < j & j <= n holds
(Q * P) * 1,j = 0. K

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies (Q * P) * 1,j = 0. K )
assume B1: ( 1 < j & j <= n ) ; :: thesis: (Q * P) * 1,j = 0. K
then B20: j in Seg n by FINSEQ_1:3;
A22: [1,j] in Indices (Q * P) by B1, A4, MATRIX_1:38;
B3: len (Col P,j) = len P by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) = len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B4d: len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
reconsider p = Col P,j, q = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
then C10b: k in dom ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) by B4d, FINSEQ_3:27;
C10a: len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
C12: k in dom P by C0, A2d, FINSEQ_3:27;
C2: p . k = P * k,j by C12, MATRIX_1:def 9;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C10b, A13, FVSUM_1:62 ;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

then D2: p . 1 = - ((a " ) * (Q * 1,j)) by A1b, B1, C2;
K3: 1 <= len (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) by C0, C10a, BB200, D0;
K1: (Base_FinSeq K,n,j) /. 1 = (Base_FinSeq K,n,j) . 1 by B5b, C0, D0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0 ;
D1: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. 1 = (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. 1) by C4, K3, D0, FINSEQ_4:24
.= (- ((a " ) * (Q * 1,j))) * (1. K) by D0, AA1110, A4, A13
.= - ((a " ) * (Q * 1,j)) by VECTSP_1:def 16 ;
q . 1 = (- ((a " ) * (Q * 1,j))) + (0. K) by D1, BB120, B4, B5b, C0, K1, D0;
hence p . k = q . k by D2, D0, RLVECT_1:10; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices P by C0, B1, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = P . k & P * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B, C2;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

then E2: p . k = 0. K by D2, AA1120, B1, C0;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
K2: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = (- ((a " ) * (Q * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (0. K) by E3, BB120, B4, B5b, C0, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

suppose E0: k = j ; :: thesis: p . k = q . k

then E2: p . k = 1. K by D2, AA1110, C0;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
K1: (Base_FinSeq K,n,k) /. k = (Base_FinSeq K,n,k) . k by B5b, C0, E0, FINSEQ_4:24
.= 1. K by B1, AA1110, E0 ;
K2: (- (((a " ) * (Q * 1,k)) * (Base_FinSeq K,n,1))) /. k = (- (((a " ) * (Q * 1,k)) * (Base_FinSeq K,n,1))) . k by B4, C0, E0, FINSEQ_4:24;
E3: (- (((a " ) * (Q * 1,k)) * (Base_FinSeq K,n,1))) . k = (- ((a " ) * (Q * 1,k))) * (0. K) by D0, AA1120, A4, C0, E1, C4, E0
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (1. K) by BB120, B4, B5b, C0, E3, K1, K2, E0;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then B7: Col P,j = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
K1: 1 <= n by B1, XXREAL_0:2;
B8: 1 in Seg (width Q) by A2a, K1, FINSEQ_1:3;
K2: (Line Q,1) /. 1 = (Line Q,1) . 1 by K1, A2, FINSEQ_4:24
.= a by A1, B8, MATRIX_1:def 8 ;
K2a: len (Line Q,1) = n by A2a, MATRIX_1:def 8;
K3: (Line Q,1) /. j = (Line Q,1) . j by K2a, B1, FINSEQ_4:24;
(Q * P) * 1,j = |((Line Q,1),(Col P,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line Q,1),(- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line Q,1),(Base_FinSeq K,n,j))| by BB248, B4, A2, B7, B5b
.= |((Line Q,1),((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line Q,1),(Base_FinSeq K,n,j))| by BB200
.= ((- ((a " ) * (Q * 1,j))) * |((Line Q,1),(Base_FinSeq K,n,1))|) + |((Line Q,1),(Base_FinSeq K,n,j))| by BB246, A2, A2b
.= ((- ((a " ) * (Q * 1,j))) * a) + |((Line Q,1),(Base_FinSeq K,n,j))| by K2, AA2627, A2, A4
.= (- (((a " ) * (Q * 1,j)) * a)) + |((Line Q,1),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((Q * 1,j) * ((a " ) * a))) + |((Line Q,1),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((Q * 1,j) * (1. K))) + |((Line Q,1),(Base_FinSeq K,n,j))| by A1, VECTSP_1:def 22
.= (- ((Q * 1,j) * (1. K))) + ((Line Q,1) /. j) by AA2627, A2, B1
.= (- (Q * 1,j)) + ((Line Q,1) /. j) by VECTSP_1:def 16
.= (- (Q * 1,j)) + (Q * 1,j) by A2a, B20, K3, MATRIX_1:def 8
.= 0. K by RLVECT_1:16 ;
hence (Q * P) * 1,j = 0. K ; :: thesis: verum

end;

A15: for i, j being Element of NAT st 1 < i & i <= n & 1 <= j & j <= n & i <> j holds
(Q * P) * i,j = 0. K

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & 1 <= j & j <= n & i <> j implies (Q * P) * i,j = 0. K )
assume B1: ( 1 < i & i <= n & 1 <= j & j <= n & i <> j ) ; :: thesis: (Q * P) * i,j = 0. K
then B20: ( i in Seg n & j in Seg n ) by FINSEQ_1:3;
B2: [i,j] in Indices Q by B1, MATRIX_1:38;
A22: [i,j] in Indices (Q * P) by B1, MATRIX_1:38;
A23b: [i,1] in Indices Q by B1, A4, MATRIX_1:38;
B3: len (Col P,j) = len P by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) = len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B4d: len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
B4b: len ((a " ) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;

now

per cases ( j > 1 or j <= 1 ) ;

suppose F0: j > 1 ; :: thesis: (Q * P) * i,j = 0. K

reconsider p = Col P,j, q = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
then k in Seg n by FINSEQ_1:3;
then C10b: k in dom ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) by B4d, FINSEQ_1:def 3;
C12: k in dom P by C0, A2d, FINSEQ_3:27;
C2: p . k = P * k,j by C12, MATRIX_1:def 9;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C10b, A13, FVSUM_1:62 ;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0, F0 ;
K2: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
D1: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = (- ((a " ) * (Q * 1,j))) * (1. K) by D0, AA1110, A4, A13, C4;
q . k = ((- ((a " ) * (Q * 1,j))) * (1. K)) + (0. K) by BB120, B4, B5b, C0, D1, K1, K2
.= (- ((a " ) * (Q * 1,j))) * (1. K) by RLVECT_1:10
.= - ((a " ) * (Q * 1,j)) by VECTSP_1:def 16 ;
hence p . k = q . k by A1b, B1, F0, C2, D0; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices P by B1, C0, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = P . k & P * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B, C2;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

(- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, B4, C0, FINSEQ_4:24
.= (- ((a " ) * (Q * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1
.= 0. K by VECTSP_1:36 ;
then q . k = (0. K) + ((Base_FinSeq K,n,j) /. k) by BB120, B4, B5b, C0
.= (Base_FinSeq K,n,j) /. k by RLVECT_1:10
.= (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
hence p . k = q . k by D2, AA1120, B1, C0, E0; :: thesis: verum

end;

suppose E0: k = j ; :: thesis: p . k = q . k

(- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, B4, C0, FINSEQ_4:24
.= (- ((a " ) * (Q * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1
.= 0. K by VECTSP_1:36 ;
then q . k = (0. K) + ((Base_FinSeq K,n,j) /. k) by BB120, B4, B5b, C0
.= (Base_FinSeq K,n,j) /. k by RLVECT_1:10
.= (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 1. K by B1, AA1110, E0 ;
hence p . k = q . k by D2, AA1110, C0, E0; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then B7: Col P,j = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
A2a: ( len Q = n & width Q = n ) by MATRIX_1:25;
K2: len (Line Q,i) = n by A2a, MATRIX_1:def 8;
K3: (Line Q,i) /. j = (Line Q,i) . j by K2, B1, FINSEQ_4:24
.= Q * i,j by B20, A2a, MATRIX_1:def 8 ;
K0: (Line Q,i) /. 1 = (Line Q,i) . 1 by K2, A4, FINSEQ_4:24
.= Q * i,1 by A10, MATRIX_1:def 8 ;
B18: 1 <= n by B1, XXREAL_0:2;
B28: (Q * P) * i,j = |((Line Q,i),(Col P,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line Q,i),(- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line Q,i),(Base_FinSeq K,n,j))| by BB248, B4, K2, B7, B5b
.= |((Line Q,i),((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line Q,i),(Base_FinSeq K,n,j))| by BB200
.= ((- ((a " ) * (Q * 1,j))) * |((Line Q,i),(Base_FinSeq K,n,1))|) + |((Line Q,i),(Base_FinSeq K,n,j))| by BB246, K2, A2b
.= ((- ((a " ) * (Q * 1,j))) * (Q * i,1)) + |((Line Q,i),(Base_FinSeq K,n,j))| by K0, AA2627, K2, A4
.= (- (((Q * 1,j) * (a " )) * (Q * i,1))) + |((Line Q,i),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((Q * 1,j) * ((a " ) * (Q * i,1)))) + |((Line Q,i),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((Q * 1,j) * ((a " ) * (Q * i,1)))) + (Q * i,j) by K3, AA2627, B1, K2 ;
consider p1 being FinSequence of K such that
A97: ( p1 = Q . i & Q * i,j = p1 . j ) by B2, MATRIX_1:def 6;
p1 = Base_FinSeq K,n,i by A1, A97, B1;
then A98: p1 . j = 0. K by AA1120, B1;
consider p2 being FinSequence of K such that
A99: ( p2 = Q . i & Q * i,1 = p2 . 1 ) by A23b, MATRIX_1:def 6;
p2 = Base_FinSeq K,n,i by A1, A99, B1;
hence (Q * P) * i,j = (- ((Q * 1,j) * ((a " ) * (0. K)))) + (Q * i,j) by B28, A99, AA1120, B18, B1
.= (- ((Q * 1,j) * (0. K))) + (Q * i,j) by VECTSP_1:36
.= (- (0. K)) + (Q * i,j) by VECTSP_1:36
.= (0. K) + (0. K) by A97, A98, RLVECT_1:25
.= 0. K by RLVECT_1:10 ;
:: thesis: verum

end;

suppose F1: j <= 1 ; :: thesis: (Q * P) * i,j = 0. K

reconsider p = Col P,j, q = (a " ) * (Base_FinSeq K,n,1) as FinSequence of K ;
F2: for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
then C10: k in Seg n by FINSEQ_1:3;
then C10b: k in dom ((a " ) * (Base_FinSeq K,n,1)) by B4b, FINSEQ_1:def 3;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
C12: k in dom P by C0, A2d, FINSEQ_3:27;
C2: p . k = P * k,j by C12, MATRIX_1:def 9;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: ((a " ) * (Base_FinSeq K,n,1)) . k = (a " ) * ((Base_FinSeq K,n,1) /. k) by C10b, A13, FVSUM_1:62;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

q . k = (a " ) * (1. K) by C4, D0, AA1110, C0, A13
.= a " by VECTSP_1:def 16 ;
hence p . k = q . k by A1, F1, B1, C2, D0, XXREAL_0:1; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices P by A8d, B20, C10, ZFMISC_1:106;
then consider p2 being FinSequence of K such that
D3: ( p2 = P . k & P * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B, C2;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
A13a: 1 <= n by C0, XXREAL_0:2;
(a " ) * ((Base_FinSeq K,n,1) /. k) = (a " ) * (0. K) by A13, AA1120, D0, C0, A13a
.= 0. K by VECTSP_1:36 ;
hence p . k = q . k by E0, D2, AA1120, B1, C0, C4; :: thesis: verum

end;

suppose k = j ; :: thesis: p . k = q . k

hence p . k = q . k by F1, D0; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

A2a: ( len Q = n & width Q = n ) by MATRIX_1:25;
K2: len (Line Q,i) = n by A2a, MATRIX_1:def 8;
K0: (Line Q,i) /. 1 = (Line Q,i) . 1 by K2, A4, FINSEQ_4:24
.= Q * i,1 by A10, MATRIX_1:def 8 ;
B18: 1 <= n by B1, XXREAL_0:2;
B28: (Q * P) * i,j = |((Line Q,i),(Col P,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line Q,i),((a " ) * (Base_FinSeq K,n,1)))| by F2, B3, B4b, FINSEQ_1:18
.= (a " ) * |((Line Q,i),(Base_FinSeq K,n,1))| by BB246, K2, A2b
.= (a " ) * (Q * i,1) by K0, AA2627, K2, A4 ;
consider p2 being FinSequence of K such that
A99: ( p2 = Q . i & Q * i,1 = p2 . 1 ) by A23b, MATRIX_1:def 6;
p2 = Base_FinSeq K,n,i by A1, A99, B1;
hence (Q * P) * i,j = (a " ) * (0. K) by B28, A99, AA1120, B18, B1
.= 0. K by VECTSP_1:36 ;
:: thesis: verum

end;

end;

end;

hence (Q * P) * i,j = 0. K ; :: thesis: verum

end;

A85: for i, j being Element of NAT st 1 < i & i <= n & i = j holds
(Q * P) * i,j = 1. K

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & i = j implies (Q * P) * i,j = 1. K )
assume B1: ( 1 < i & i <= n & i = j ) ; :: thesis: (Q * P) * i,j = 1. K
then B20: ( i in Seg n & j in Seg n ) by FINSEQ_1:3;
B2: [i,j] in Indices Q by B1, MATRIX_1:38;
A22: [i,j] in Indices (Q * P) by B1, MATRIX_1:38;
A23b: [i,1] in Indices Q by B1, A40, MATRIX_1:38;
B3: len (Col P,j) = len P by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) = len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B4d: len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
reconsider p = Col P,j, q = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
then k in Seg n by FINSEQ_1:3;
then C10b: k in dom ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) by B4d, FINSEQ_1:def 3;
C10a: len ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
C12: k in dom P by C0, A2d, FINSEQ_3:27;
C2: p . k = P * k,j by C12, MATRIX_1:def 9;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C10b, A13, FVSUM_1:62 ;

per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;

suppose D0: 1 = k ; :: thesis: p . k = q . k

D2: p . k = - ((a " ) * (Q * 1,j)) by A1b, B1, C2, D0;
K3: ( 1 <= k & k <= len (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) ) by C0, C10a, BB200;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0 ;
D1: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((a " ) * (Q * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, K3, FINSEQ_4:24
.= (- ((a " ) * (Q * 1,j))) * (1. K) by D0, AA1110, A4, A13
.= - ((a " ) * (Q * 1,j)) by VECTSP_1:def 16 ;
q . k = (- ((a " ) * (Q * 1,j))) + (0. K) by D1, BB120, B4, B5b, C0, K1;
hence p . k = q . k by D2, RLVECT_1:10; :: thesis: verum

end;

suppose D0: 1 < k ; :: thesis: p . k = q . k

[k,j] in Indices P by B1, C0, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = P . k & P * k,j = p2 . j ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A1, D0, C0, D3, B, C2;

now

per cases ( k <> j or k = j ) ;

suppose E0: k <> j ; :: thesis: p . k = q . k

then E2: p . k = 0. K by D2, AA1120, B1, C0;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
K2: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = (- ((a " ) * (Q * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (0. K) by E3, BB120, B4, B5b, C0, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

suppose E0: k = j ; :: thesis: p . k = q . k

then E2: p . k = 1. K by D2, AA1110, C0;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 1. K by AA1110, C0, E0 ;
K2: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) . k = (- ((a " ) * (Q * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (1. K) by BB120, B4, B5b, C0, E3, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then B7: Col P,j = (- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
K2: len (Line Q,i) = n by A2a, MATRIX_1:def 8;
A2a: ( len Q = n & width Q = n ) by MATRIX_1:25;
K3: (Line Q,i) /. j = (Line Q,i) . j by K2, B1, FINSEQ_4:24
.= Q * i,j by B20, A2a, MATRIX_1:def 8 ;
K0: (Line Q,i) /. 1 = (Line Q,i) . 1 by K2, A4, FINSEQ_4:24
.= Q * i,1 by A10, MATRIX_1:def 8 ;
B18: 1 <= n by B1, XXREAL_0:2;
B28: (Q * P) * i,j = |((Line Q,i),(Col P,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line Q,i),(- (((a " ) * (Q * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line Q,i),(Base_FinSeq K,n,j))| by BB248, B4, K2, B7, B5b
.= |((Line Q,i),((- ((a " ) * (Q * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line Q,i),(Base_FinSeq K,n,j))| by BB200
.= ((- ((a " ) * (Q * 1,j))) * |((Line Q,i),(Base_FinSeq K,n,1))|) + |((Line Q,i),(Base_FinSeq K,n,j))| by BB246, K2, A2b
.= ((- ((a " ) * (Q * 1,j))) * (Q * i,1)) + |((Line Q,i),(Base_FinSeq K,n,j))| by K0, AA2627, K2, A4
.= (- (((Q * 1,j) * (a " )) * (Q * i,1))) + |((Line Q,i),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((Q * 1,j) * ((a " ) * (Q * i,1)))) + |((Line Q,i),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((Q * 1,j) * ((a " ) * (Q * i,1)))) + (Q * i,j) by K3, AA2627, B1, K2 ;
consider p1 being FinSequence of K such that
A97: ( p1 = Q . i & Q * i,j = p1 . j ) by B2, MATRIX_1:def 6;
p1 = Base_FinSeq K,n,i by A1, A97, B1;
then A98: p1 . j = 1. K by AA1110, B1;
consider p2 being FinSequence of K such that
A99: ( p2 = Q . i & Q * i,1 = p2 . 1 ) by A23b, MATRIX_1:def 6;
p2 = Base_FinSeq K,n,i by A1, A99, B1;
hence (Q * P) * i,j = (- ((Q * 1,j) * ((a " ) * (0. K)))) + (Q * i,j) by B28, A99, AA1120, B18, B1
.= (- ((Q * 1,j) * (0. K))) + (Q * i,j) by VECTSP_1:36
.= (- (0. K)) + (Q * i,j) by VECTSP_1:36
.= (0. K) + (1. K) by A97, A98, RLVECT_1:25
.= 1. K by RLVECT_1:10 ;
:: thesis: verum

end;

KK1: for i, j being Nat st [i,j] in Indices (Q * P) holds
(Q * P) * i,j = (1. K,n) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (Q * P) implies (Q * P) * i,j = (1. K,n) * i,j )
assume [i,j] in Indices (Q * P) ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j
then B2: ( i in Seg n & j in Seg n ) by A18, ZFMISC_1:106;
then B3: ( 1 <= i & i <= n ) by FINSEQ_1:3;
B4: ( 1 <= j & j <= n ) by B2, FINSEQ_1:3;
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 13;

per cases ( 1 < i or 1 = i ) by B3, XXREAL_0:1;

suppose C0: 1 < i ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j

now

per cases ( i <> j or i = j ) ;

suppose D0: i <> j ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j

D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 0. K by AA1120, D0, B3, B4 ;
thus (Q * P) * i,j = (Q * P) * i0,j0
.= (1. K,n) * i,j by D1, C0, B3, B4, A15, D0 ; :: thesis: verum

end;

suppose D0: i = j ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j

D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 1. K by AA1110, D0, B4 ;
thus (Q * P) * i,j = (Q * P) * i0,j0
.= (1. K,n) * i,j by D1, C0, B4, A85, D0 ; :: thesis: verum

end;

end;

end;

hence (Q * P) * i,j = (1. K,n) * i,j ; :: thesis: verum

end;

suppose C0: 1 = i ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j

now

per cases ( i < j or i >= j ) ;

suppose D0: i < j ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j

D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 0. K by AA1120, B3, B4, D0 ;
thus (Q * P) * i,j = (Q * P) * i0,j0
.= (1. K,n) * i,j by D1, C0, B4, A14, D0 ; :: thesis: verum

end;

suppose D9: i >= j ; :: thesis: (Q * P) * i,j = (1. K,n) * i,j

then D0: i = j by B4, C0, XXREAL_0:1;
D1: (1. K,n) * i,j = (Base_FinSeq K,n,i0) . j0 by BB300, B3, B4
.= 1. K by D0, AA1110, B4 ;
thus (Q * P) * i,j = (1. K,n) * i,j by D1, C0, A13, D9, B4, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence (Q * P) * i,j = (1. K,n) * i,j ; :: thesis: verum

end;

end;

end;

A25: Q * P = 1. K,n by KK1, MATRIX_1:28;
hence P is invertible by AA4145, A5; :: thesis: Q = P ~
thus Q = P ~ by AA4140, A5, A25; :: thesis: verum