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 A1: ( 1 <= i0 & i0 <= n ) ; :: thesis: ( SwapDiagonal K,n,i0 is invertible & (SwapDiagonal K,n,i0) ~ = SwapDiagonal K,n,i0 )
A51: 1 <= n by A1, XXREAL_0:2;
set R = (SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0);
A10: ( len ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = n & width ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = n & Indices ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A11: ( len (1. K,n) = n & width (1. K,n) = n & Indices (1. K,n) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A5: ( len ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = len (1. K,n) & width ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) = width (1. K,n) ) by A11, MATRIX_1:25;
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 )
assume B1: [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
reconsider i = i4, j = j4 as Element of NAT by ORDINAL1:def 13;
B15: ( i in Seg n & j in Seg n ) by B1, A10, ZFMISC_1:106;
B2: ( 1 <= i & i <= n & 1 <= j & j <= n ) by B15, FINSEQ_1:3;
B77: [i,j] in Indices (1. K,n) by A10, B1, MATRIX_1:25;

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

suppose C0: 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 D0: 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 E0: i = j ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

E1: (1. K,n) * i,j = 1. K by B77, E0, MATRIX_1:def 12;

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 XA, A1, D0, E0, C0, B2; :: 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 E0, XB, B2; :: thesis: verum

end;

end;

end;

hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by AA4100, A1, C0, B2, D0, E1; :: thesis: verum

end;

suppose E0: i <> j ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

E1: (1. K,n) * i,j = 0. K by B77, E0, MATRIX_1:def 12;

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 XC, E0, B2; :: 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 XA, A1, D0, E0, C0, B2; :: thesis: verum

end;

end;

end;

hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by E1, AA4100, A1, C0, B2, D0; :: 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 D0: 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 E0: i = j ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

then E1: (1. K,n) * i,j = 1. K by B77, MATRIX_1:def 12;

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 D0, C0; :: 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 XA, A1, A51; :: thesis: verum

end;

end;

end;

hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by E1, E0, D0, AA4100, A1; :: thesis: verum

end;

suppose E0: i <> j ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

then E1: (1. K,n) * i,j = 0. K by B77, MATRIX_1:def 12;

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 D0, C0; :: 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 XA, A1, D0, C0, A51; :: 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 XA, D0, E0, C0, B2, A51; :: thesis: verum

end;

end;

end;

hence (SwapDiagonal K,n,i0) * 1,j = 0. K ; :: thesis: verum

end;

end;

end;

hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by E1, D0, B2, AA4100; :: 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 C0: 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 D0: 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 E0: j <> 1 ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

then E1: (1. K,n) * i,j = 0. K by C0, B77, MATRIX_1:def 12;

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 XA, E0, B2; :: 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, XA, D0, E0, B2; :: thesis: verum

end;

end;

end;

hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by C0, E1, AA4100, A1, B2; :: thesis: verum

end;

suppose E0: j = 1 ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

then E1: (1. K,n) * i,j = 1. K by B77, C0, MATRIX_1:def 12;
(SwapDiagonal K,n,i0) * i0,j = 1. K by XA, A1, D0, E0, A51;
hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by C0, E1, AA4100, A1, B2; :: thesis: verum

end;

end;

end;

suppose D0: 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 E0: i <> j ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

then E1: (1. K,n) * i,j = 0. K by B77, MATRIX_1:def 12;
(SwapDiagonal K,n,1) * 1,j = 0. K by XC, E0, C0, B2;
hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by C0, E1, AA4100, B2, D0; :: thesis: verum

end;

suppose E0: i = j ; :: thesis: ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j

E1: (1. K,n) * j,j = 1. K by B77, E0, MATRIX_1:def 12;
((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * 1,j = (SwapDiagonal K,n,i0) * i0,j by AA4100, A1, B2;
hence ((SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0)) * i,j = (1. K,n) * i,j by XB, A1, D0, E0, C0, E1; :: 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;

then A88: (SwapDiagonal K,n,i0) * (SwapDiagonal K,n,i0) = 1. K,n by A5, MATRIX_1:21;
hence SwapDiagonal K,n,i0 is invertible by AA4145; :: thesis: (SwapDiagonal K,n,i0) ~ = SwapDiagonal K,n,i0
thus (SwapDiagonal K,n,i0) ~ = SwapDiagonal K,n,i0 by AA4140, A88; :: thesis: verum