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_1:25;
A5: width ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = n by MATRIX_1:25;
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 13;
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_1:25;
j in Seg n by A5, A7, ZFMISC_1:106;
then A9: ( 1 <= j & j <= n ) by FINSEQ_1:3;
A10: i in Seg n by A4, A7, ZFMISC_1:106;
then A11: 1 <= i by FINSEQ_1:3;
A12: i <= n by A10, FINSEQ_1:3;
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
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
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
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 12;
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
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 12;
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
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
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 12;
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
per cases ( i0 = 1 or i0 <> 1 ) ;
suppose i0 = 1 ; :: thesis: (SwapDiagonal K,n,i0) * 1,j = 0. K
hence (SwapDiagonal K,n,i0) * 1,j = 0. K by A13, A19; :: thesis: verum
end;
suppose i0 <> 1 ; :: thesis: (SwapDiagonal K,n,i0) * 1,j = 0. K
now
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;
end;
end;
(1. K,n) * i,j = 0. K by A8, A22, MATRIX_1:def 12;
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
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
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 12;
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 12;
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
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 12;
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 12;
((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_1:25;
then A31: width ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = width (1. K,n) by MATRIX_1:25;
len (1. K,n) = n by MATRIX_1:25;
then len ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = len (1. K,n) by MATRIX_1:25;
then A32: (SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0) = 1. K,n by A31, A6, MATRIX_1: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