let n be Element of NAT ; :: thesis: for K being Field
for i0 being Element of NAT st 1 <= i0 & i0 <= n holds
( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) )
let K be Field; :: thesis: for i0 being Element of NAT st 1 <= i0 & i0 <= n holds
( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) )
let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 <= n implies ( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) ) )
assume that
A1: 1 <= i0 and
A2: i0 <= n ; :: thesis: ( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) )
A3: 1 <= n by A1, A2, XXREAL_0:2;
set R = (SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0));
A4: Indices ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A5: width ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) = n by MATRIX_0:24;
A6: for i4, j4 being Nat st [i4,j4] in Indices ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) holds
((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4)
proof
let i4, j4 be Nat; :: thesis: ( [i4,j4] in Indices ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) implies ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4) )
reconsider i = i4, j = j4 as Element of NAT by ORDINAL1:def 12;
assume A7: [i4,j4] in Indices ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4)
then A8: [i,j] in Indices (1. (K,n)) by A4, MATRIX_0:24;
j in Seg n by A5, A7, ZFMISC_1:87;
then A9: ( 1 <= j & j <= n ) by FINSEQ_1:1;
A10: i in Seg n by A4, A7, ZFMISC_1:87;
then A11: 1 <= i by FINSEQ_1:1;
A12: i <= n by A10, FINSEQ_1:1;
per cases ( 1 < i or 1 = i ) by A11, XXREAL_0:1;
suppose A13: 1 < i ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4)
now :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
per cases ( i <> i0 or i = i0 ) ;
suppose A14: i <> i0 ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
now :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
per cases ( i = j or i <> j ) ;
suppose A15: i = j ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
A16: now :: thesis: (SwapDiagonal (K,n,i0)) * (i,j) = 1. K
per cases ( i0 <> 1 or i0 = 1 ) ;
suppose i0 <> 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (i,j) = 1. K
hence (SwapDiagonal (K,n,i0)) * (i,j) = 1. K by A1, A2, A12, A13, A14, A15, Th43; :: thesis: verum
end;
suppose i0 = 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (i,j) = 1. K
hence (SwapDiagonal (K,n,i0)) * (i,j) = 1. K by A11, A12, A15, Th44; :: thesis: verum
end;
end;
end;
(1. (K,n)) * (i,j) = 1. K by A8, A15, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A1, A2, A12, A9, A13, A14, A16, Th48; :: thesis: verum
end;
suppose A17: i <> j ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
A18: now :: thesis: (SwapDiagonal (K,n,i0)) * (i,j) = 0. K
per cases ( i0 = 1 or i0 <> 1 ) ;
suppose i0 = 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (i,j) = 0. K
hence (SwapDiagonal (K,n,i0)) * (i,j) = 0. K by A11, A12, A9, A17, Th45; :: thesis: verum
end;
suppose i0 <> 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (i,j) = 0. K
hence (SwapDiagonal (K,n,i0)) * (i,j) = 0. K by A1, A2, A12, A9, A13, A14, A17, Th43; :: thesis: verum
end;
end;
end;
(1. (K,n)) * (i,j) = 0. K by A8, A17, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A1, A2, A12, A9, A13, A14, A18, Th48; :: thesis: verum
end;
end;
end;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum
end;
suppose A19: i = i0 ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
now :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
per cases ( i = j or i <> j ) ;
suppose A20: i = j ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
A21: now :: thesis: (SwapDiagonal (K,n,i0)) * (1,i0) = 1. K
per cases ( i0 = 1 or i0 <> 1 ) ;
suppose i0 = 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (1,i0) = 1. K
hence (SwapDiagonal (K,n,i0)) * (1,i0) = 1. K by A13, A19; :: thesis: verum
end;
suppose i0 <> 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (1,i0) = 1. K
hence (SwapDiagonal (K,n,i0)) * (1,i0) = 1. K by A1, A2, A3, Th43; :: thesis: verum
end;
end;
end;
(1. (K,n)) * (i,j) = 1. K by A8, A20, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A1, A2, A19, A20, A21, Th48; :: thesis: verum
end;
suppose A22: i <> j ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
A23: now :: thesis: (SwapDiagonal (K,n,i0)) * (1,j) = 0. K
now :: thesis: (SwapDiagonal (K,n,i0)) * (1,j) = 0. K
per cases ( j = 1 or j <> 1 ) ;
suppose j = 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (1,j) = 0. K
hence (SwapDiagonal (K,n,i0)) * (1,j) = 0. K by A2, A3, A13, A19, Th43; :: thesis: verum
end;
suppose j <> 1 ; :: thesis: (SwapDiagonal (K,n,i0)) * (1,j) = 0. K
hence (SwapDiagonal (K,n,i0)) * (1,j) = 0. K by A3, A12, A9, A13, A19, A22, Th43; :: thesis: verum
end;
end;
end;
hence (SwapDiagonal (K,n,i0)) * (1,j) = 0. K ; :: thesis: verum
end;
(1. (K,n)) * (i,j) = 0. K by A8, A22, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A11, A12, A9, A19, A23, Th48; :: thesis: verum
end;
end;
end;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum
end;
end;
end;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4) ; :: thesis: verum
end;
suppose A24: 1 = i ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4)
now :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
per cases ( i0 <> 1 or i0 = 1 ) ;
suppose A25: i0 <> 1 ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
per cases ( j <> 1 or j = 1 ) ;
suppose A26: j <> 1 ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
A27: now :: thesis: (SwapDiagonal (K,n,i0)) * (i0,j) = 0. K
per cases ( j = i0 or j <> i0 ) ;
suppose j = i0 ; :: thesis: (SwapDiagonal (K,n,i0)) * (i0,j) = 0. K
hence (SwapDiagonal (K,n,i0)) * (i0,j) = 0. K by A9, A26, Th43; :: thesis: verum
end;
suppose j <> i0 ; :: thesis: (SwapDiagonal (K,n,i0)) * (i0,j) = 0. K
hence (SwapDiagonal (K,n,i0)) * (i0,j) = 0. K by A1, A2, A9, A25, A26, Th43; :: thesis: verum
end;
end;
end;
(1. (K,n)) * (i,j) = 0. K by A8, A24, A26, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A1, A2, A9, A24, A27, Th48; :: thesis: verum
end;
suppose j = 1 ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
then ( (1. (K,n)) * (i,j) = 1. K & (SwapDiagonal (K,n,i0)) * (i0,j) = 1. K ) by A1, A2, A3, A8, A24, A25, Th43, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A1, A2, A9, A24, Th48; :: thesis: verum
end;
end;
end;
suppose A28: i0 = 1 ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
now :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
per cases ( i <> j or i = j ) ;
suppose i <> j ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
then ( (1. (K,n)) * (i,j) = 0. K & (SwapDiagonal (K,n,1)) * (1,j) = 0. K ) by A12, A9, A8, A24, Th45, MATRIX_1:def 3;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A12, A9, A24, A28, Th48; :: thesis: verum
end;
suppose A29: i = j ; :: thesis: ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j)
then A30: (1. (K,n)) * (j,j) = 1. K by A8, MATRIX_1:def 3;
((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (1,j) = (SwapDiagonal (K,n,i0)) * (i0,j) by A1, A2, A9, Th48;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) by A2, A24, A28, A29, A30, Th44; :: thesis: verum
end;
end;
end;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum
end;
end;
end;
hence ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) * (i4,j4) = (1. (K,n)) * (i4,j4) ; :: thesis: verum
end;
end;
end;
width (1. (K,n)) = n by MATRIX_0:24;
then A31: width ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) = width (1. (K,n)) by MATRIX_0:24;
len (1. (K,n)) = n by MATRIX_0:24;
then len ((SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0))) = len (1. (K,n)) by MATRIX_0:24;
then A32: (SwapDiagonal (K,n,i0)) * (SwapDiagonal (K,n,i0)) = 1. (K,n) by A31, A6, MATRIX_0:21;
hence SwapDiagonal (K,n,i0) is invertible by Th19; :: thesis: (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0)
thus (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) by A32, Th18; :: thesis: verum