let i, n be Nat; ( i in Seg n implies ( AxialSymmetry (i,n) is V254( F_Real ) & (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
; ( AxialSymmetry (i,n) is V254( F_Real ) & (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 V254( F_Real )
by MATRIX_1:def 6; (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;
( [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)))
;
((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
;
((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
;
((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;
verum end; suppose A13:
k = m
;
((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;
verum end; end; suppose A14:
m = i
;
((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
;
((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;
verum end; suppose A17:
k = m
;
((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;
verum 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; verum