let i, n be Nat; :: thesis: ( i in Seg n implies ( AxialSymmetry (i,n) is diagonal & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) ) )
set S = Seg n;
set A = AxialSymmetry (i,n);
set ONE = 1. (F_Real,n);
set AA = (AxialSymmetry (i,n)) * (AxialSymmetry (i,n));
assume A1: i in Seg n ; :: thesis: ( AxialSymmetry (i,n) is diagonal & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) )
for k, m being Nat st [k,m] in Indices (AxialSymmetry (i,n)) & (AxialSymmetry (i,n)) * (k,m) <> 0. F_Real holds
k = m by A1, Def2;
hence AxialSymmetry (i,n) is diagonal by MATRIX_1:def 6; :: thesis: (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n)
for k, m being Nat st [k,m] in Indices ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) holds
((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

proof

let k, m be Nat; :: thesis: ( [k,m] in Indices ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) implies ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m) )
assume A2: [k,m] in Indices ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)
A3: width (AxialSymmetry (i,n)) = n by MATRIX_0:24;
then len (@ (Line ((AxialSymmetry (i,n)),k))) = n by CARD_1:def 7;
then reconsider L = @ (Line ((AxialSymmetry (i,n)),k)) as Element of (TOP-REAL n) by TOPREAL3:46;
len (AxialSymmetry (i,n)) = n by MATRIX_0:25;
then A4: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (@ L) "*" (Col ((AxialSymmetry (i,n)),m)) by A2, A3, MATRIX_3:def 4;
A5: Indices ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A6: m in Seg n by A2, ZFMISC_1:87;
then A7: (Line ((AxialSymmetry (i,n)),k)) . m = (AxialSymmetry (i,n)) * (k,m) by A3, MATRIX_0:def 7;
A8: Indices (AxialSymmetry (i,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A9: Indices (1. (F_Real,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;

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

suppose A10: m <> i ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

then A11: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (AxialSymmetry (i,n)) * (k,m) by A1, A4, A6, A7, Th5;

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

suppose A12: k <> m ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

then (1. (F_Real,n)) * (k,m) = 0. F_Real by A2, A5, A9, MATRIX_1:def 3;
hence ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m) by A1, A2, A5, A8, A11, A12, Def2; :: thesis: verum

end;

suppose A13: k = m ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

then (1. (F_Real,n)) * (k,m) = 1. F_Real by A2, A5, A9, MATRIX_1:def 3;
hence ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m) by A1, A2, A5, A8, A10, A11, A13, Def2; :: thesis: verum

end;

end;

end;

suppose A14: m = i ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

then A15: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = - ((AxialSymmetry (i,n)) * (k,m)) by A4, A6, A7, Th6;

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

suppose A16: k <> m ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

then (AxialSymmetry (i,n)) * (k,m) = 0. F_Real by A1, A2, A5, A8, Def2;
hence ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m) by A2, A5, A9, A15, A16, MATRIX_1:def 3; :: thesis: verum

end;

suppose A17: k = m ; :: thesis: ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m)

then ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = - (- (1. F_Real)) by A1, A14, A15, Def2;
hence ((AxialSymmetry (i,n)) * (AxialSymmetry (i,n))) * (k,m) = (1. (F_Real,n)) * (k,m) by A2, A5, A9, A17, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

end;

end;

then (AxialSymmetry (i,n)) * (AxialSymmetry (i,n)) = 1. (F_Real,n) by MATRIX_0:27;
then AxialSymmetry (i,n) is_reverse_of AxialSymmetry (i,n) by MATRIX_6:def 2;
hence (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) by MATRIX_6:def 4; :: thesis: verum