let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Rotation (i,j,n,0) = 1. (F_Real,n) )

set O = Rotation (i,j,n,0);

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Rotation (i,j,n,0) = 1. (F_Real,n)

A2: for k, m being Nat st [k,m] in Indices (Rotation (i,j,n,0)) & k <> m holds

(Rotation (i,j,n,0)) * (k,m) = 0. F_Real

(Rotation (i,j,n,0)) * (k,k) = 1. F_Real

set O = Rotation (i,j,n,0);

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Rotation (i,j,n,0) = 1. (F_Real,n)

A2: for k, m being Nat st [k,m] in Indices (Rotation (i,j,n,0)) & k <> m holds

(Rotation (i,j,n,0)) * (k,m) = 0. F_Real

proof

for k being Nat st [k,k] in Indices (Rotation (i,j,n,0)) holds
let k, m be Nat; :: thesis: ( [k,m] in Indices (Rotation (i,j,n,0)) & k <> m implies (Rotation (i,j,n,0)) * (k,m) = 0. F_Real )

assume that

A3: [k,m] in Indices (Rotation (i,j,n,0)) and

A4: k <> m ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

end;assume that

A3: [k,m] in Indices (Rotation (i,j,n,0)) and

A4: k <> m ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

per cases
( ( k = i & m = j ) or ( k = j & m = i ) or ( k = i & m <> j ) or ( k = j & m <> i ) or ( m = i & k <> j ) or ( m = j & k <> i ) or ( k <> i & k <> j & m <> i & m <> j ) )
;

end;

suppose
( ( k = i & m = j ) or ( k = j & m = i ) )
; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then
( (Rotation (i,j,n,0)) * (k,m) = sin 0 or (Rotation (i,j,n,0)) * (k,m) = - (sin 0) )
by A1, Def3;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by SIN_COS:31; :: thesis: verum

end;hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by SIN_COS:31; :: thesis: verum

suppose
( k = i & m <> j )
; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then
not m in {i,j}
by A4, TARSKI:def 2;

then {k,m} <> {i,j} by TARSKI:def 2;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;then {k,m} <> {i,j} by TARSKI:def 2;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

suppose
( k = j & m <> i )
; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then
not m in {i,j}
by A4, TARSKI:def 2;

then {k,m} <> {i,j} by TARSKI:def 2;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;then {k,m} <> {i,j} by TARSKI:def 2;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

suppose
( m = i & k <> j )
; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then
not k in {i,j}
by A4, TARSKI:def 2;

then {k,m} <> {i,j} by TARSKI:def 2;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;then {k,m} <> {i,j} by TARSKI:def 2;

hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

(Rotation (i,j,n,0)) * (k,k) = 1. F_Real

proof

hence
Rotation (i,j,n,0) = 1. (F_Real,n)
by A2, MATRIX_1:def 3; :: thesis: verum
let k be Nat; :: thesis: ( [k,k] in Indices (Rotation (i,j,n,0)) implies (Rotation (i,j,n,0)) * (k,k) = 1. F_Real )

assume A5: [k,k] in Indices (Rotation (i,j,n,0)) ; :: thesis: (Rotation (i,j,n,0)) * (k,k) = 1. F_Real

( k = i or k = j or ( k <> i & k <> j ) ) ;

hence (Rotation (i,j,n,0)) * (k,k) = 1. F_Real by A1, A5, Def3, SIN_COS:31; :: thesis: verum

end;assume A5: [k,k] in Indices (Rotation (i,j,n,0)) ; :: thesis: (Rotation (i,j,n,0)) * (k,k) = 1. F_Real

( k = i or k = j or ( k <> i & k <> j ) ) ;

hence (Rotation (i,j,n,0)) * (k,k) = 1. F_Real by A1, A5, Def3, SIN_COS:31; :: thesis: verum