let K be Field; for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let V1, V2 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let b2 be OrdBasis of V2; for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let f be linear-transformation of V1,V2; for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let W1, W2 be Subspace of V1; for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let U1, U2 be Subspace of V2; ( ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 implies for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K)) )
assume that
A1:
( dim W1 = 0 implies dim U1 = 0 )
and
A2:
( dim W2 = 0 implies dim U2 = 0 )
and
A3:
V2 is_the_direct_sum_of U1,U2
; for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
A4:
U1 /\ U2 = (0). V2
by A3, VECTSP_5:def 4;
let fW1 be linear-transformation of W1,U1; for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let fW2 be linear-transformation of W2,U2; ( fW1 = f | W1 & fW2 = f | W2 implies for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K)) )
assume that
A5:
fW1 = f | W1
and
A6:
fW2 = f | W2
; for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let w1 be OrdBasis of W1; for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let w2 be OrdBasis of W2; for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let u1 be OrdBasis of U1; for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
let u2 be OrdBasis of U2; ( w1 ^ w2 = b1 & u1 ^ u2 = b2 implies AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K)) )
assume that
A7:
w1 ^ w2 = b1
and
A8:
u1 ^ u2 = b2
; AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
A9:
len b1 = (len w1) + (len w2)
by A7, FINSEQ_1:22;
A10:
U1 + U2 = (Omega). V2
by A3, VECTSP_5:def 4;
set A = AutMt (f,b1,b2);
A11:
len b1 = len (AutMt (f,b1,b2))
by MATRLIN:def 8;
set A2 = AutMt (fW2,w2,u2);
A12:
( len w2 = dim W2 & len u2 = dim U2 )
by Th21;
then A13:
len w2 = len (AutMt (fW2,w2,u2))
by A2, MATRIX13:1;
set A1 = AutMt (fW1,w1,u1);
A14:
( len w1 = dim W1 & len u1 = dim U1 )
by Th21;
then A15:
len w1 = len (AutMt (fW1,w1,u1))
by A1, MATRIX13:1;
A16:
len u2 = width (AutMt (fW2,w2,u2))
by A2, A12, MATRIX13:1;
A17:
len u1 = width (AutMt (fW1,w1,u1))
by A1, A14, MATRIX13:1;
A18:
now for i being Nat holds
( ( i in dom (AutMt (fW1,w1,u1)) implies Line ((AutMt (f,b1,b2)),i) = (Line ((AutMt (fW1,w1,u1)),i)) ^ ((width (AutMt (fW2,w2,u2))) |-> (0. K)) ) & ( i in dom (AutMt (fW2,w2,u2)) implies Line ((AutMt (f,b1,b2)),(i + (len (AutMt (fW1,w1,u1))))) = ((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i)) ) )reconsider uu =
u1 ^ u2 as
OrdBasis of
U1 + U2 by A4, Th26;
let i be
Nat;
( ( i in dom (AutMt (fW1,w1,u1)) implies Line ((AutMt (f,b1,b2)),i) = (Line ((AutMt (fW1,w1,u1)),i)) ^ ((width (AutMt (fW2,w2,u2))) |-> (0. K)) ) & ( i in dom (AutMt (fW2,w2,u2)) implies Line ((AutMt (f,b1,b2)),(i + (len (AutMt (fW1,w1,u1))))) = ((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i)) ) )A19:
dom (AutMt (f,b1,b2)) = Seg (len (AutMt (f,b1,b2)))
by FINSEQ_1:def 3;
reconsider fb =
f . (b1 /. i),
fbi =
f . (b1 /. (i + (len (AutMt (fW1,w1,u1))))) as
Vector of
(U1 + U2) by A10;
A20:
dom (AutMt (f,b1,b2)) = dom b1
by A11, FINSEQ_3:29;
A21:
dom (AutMt (fW1,w1,u1)) = dom w1
by A15, FINSEQ_3:29;
A22:
dom fW1 = the
carrier of
W1
by FUNCT_2:def 1;
thus
(
i in dom (AutMt (fW1,w1,u1)) implies
Line (
(AutMt (f,b1,b2)),
i)
= (Line ((AutMt (fW1,w1,u1)),i)) ^ ((width (AutMt (fW2,w2,u2))) |-> (0. K)) )
( i in dom (AutMt (fW2,w2,u2)) implies Line ((AutMt (f,b1,b2)),(i + (len (AutMt (fW1,w1,u1))))) = ((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i)) )proof
assume A23:
i in dom (AutMt (fW1,w1,u1))
;
Line ((AutMt (f,b1,b2)),i) = (Line ((AutMt (fW1,w1,u1)),i)) ^ ((width (AutMt (fW2,w2,u2))) |-> (0. K))
A24:
dom (AutMt (fW1,w1,u1)) = Seg (len (AutMt (fW1,w1,u1)))
by FINSEQ_1:def 3;
then A25:
Line (
(AutMt (fW1,w1,u1)),
i) =
(AutMt (fW1,w1,u1)) . i
by A15, A23, MATRIX_0:52
.=
(AutMt (fW1,w1,u1)) /. i
by A23, PARTFUN1:def 6
.=
(fW1 . (w1 /. i)) |-- u1
by A21, A23, MATRLIN:def 8
;
len (AutMt (fW1,w1,u1)) <= len (AutMt (f,b1,b2))
by A9, A15, A11, NAT_1:11;
then A26:
Seg (len (AutMt (fW1,w1,u1))) c= Seg (len (AutMt (f,b1,b2)))
by FINSEQ_1:5;
then b1 /. i =
b1 . i
by A19, A20, A23, A24, PARTFUN1:def 6
.=
w1 . i
by A7, A21, A23, FINSEQ_1:def 7
.=
w1 /. i
by A21, A23, PARTFUN1:def 6
;
then A27:
fb = fW1 . (w1 /. i)
by A5, A22, FUNCT_1:47;
thus Line (
(AutMt (f,b1,b2)),
i) =
(AutMt (f,b1,b2)) . i
by A11, A23, A24, A26, MATRIX_0:52
.=
(AutMt (f,b1,b2)) /. i
by A19, A23, A24, A26, PARTFUN1:def 6
.=
(f . (b1 /. i)) |-- b2
by A19, A20, A23, A24, A26, MATRLIN:def 8
.=
fb |-- uu
by A10, A8, Th25
.=
(fb + (0. (U1 + U2))) |-- uu
by RLVECT_1:def 4
.=
((fW1 . (w1 /. i)) |-- u1) ^ ((0. U2) |-- u2)
by A4, A27, Th24, VECTSP_4:12
.=
(Line ((AutMt (fW1,w1,u1)),i)) ^ ((width (AutMt (fW2,w2,u2))) |-> (0. K))
by A16, A25, Th20
;
verum
end; A28:
dom (AutMt (fW2,w2,u2)) = dom w2
by A13, FINSEQ_3:29;
A29:
dom fW2 = the
carrier of
W2
by FUNCT_2:def 1;
thus
(
i in dom (AutMt (fW2,w2,u2)) implies
Line (
(AutMt (f,b1,b2)),
(i + (len (AutMt (fW1,w1,u1)))))
= ((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i)) )
verumproof
assume A30:
i in dom (AutMt (fW2,w2,u2))
;
Line ((AutMt (f,b1,b2)),(i + (len (AutMt (fW1,w1,u1))))) = ((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i))
A31:
dom (AutMt (fW2,w2,u2)) = Seg (len (AutMt (fW2,w2,u2)))
by FINSEQ_1:def 3;
then A32:
i + (len (AutMt (fW1,w1,u1))) in dom (AutMt (f,b1,b2))
by A9, A15, A13, A11, A19, A30, FINSEQ_1:60;
b1 /. (i + (len (AutMt (fW1,w1,u1)))) =
b1 . (i + (len (AutMt (fW1,w1,u1))))
by A9, A15, A13, A11, A19, A20, A30, A31, FINSEQ_1:60, PARTFUN1:def 6
.=
w2 . i
by A7, A15, A28, A30, FINSEQ_1:def 7
.=
w2 /. i
by A28, A30, PARTFUN1:def 6
;
then A33:
fbi = fW2 . (w2 /. i)
by A6, A29, FUNCT_1:47;
A34:
Line (
(AutMt (fW2,w2,u2)),
i) =
(AutMt (fW2,w2,u2)) . i
by A13, A30, A31, MATRIX_0:52
.=
(AutMt (fW2,w2,u2)) /. i
by A30, PARTFUN1:def 6
.=
(fW2 . (w2 /. i)) |-- u2
by A28, A30, MATRLIN:def 8
;
thus Line (
(AutMt (f,b1,b2)),
(i + (len (AutMt (fW1,w1,u1))))) =
(AutMt (f,b1,b2)) . (i + (len (AutMt (fW1,w1,u1))))
by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1:60, MATRIX_0:52
.=
(AutMt (f,b1,b2)) /. (i + (len (AutMt (fW1,w1,u1))))
by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1:60, PARTFUN1:def 6
.=
(f . (b1 /. (i + (len (AutMt (fW1,w1,u1)))))) |-- b2
by A20, A32, MATRLIN:def 8
.=
fbi |-- uu
by A10, A8, Th25
.=
((0. (U1 + U2)) + fbi) |-- uu
by RLVECT_1:def 4
.=
((0. U1) |-- u1) ^ ((fW2 . (w2 /. i)) |-- u2)
by A4, A33, Th24, VECTSP_4:12
.=
((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i))
by A17, A34, Th20
;
verum
end; end;
set A12 = <*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>;
A35:
( Sum (Len <*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>) = (len (AutMt (fW1,w1,u1))) + (len (AutMt (fW2,w2,u2))) & Sum (Width <*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>) = (width (AutMt (fW1,w1,u1))) + (width (AutMt (fW2,w2,u2))) )
by MATRIXJ1:16, MATRIXJ1:20;
len b2 = (len u1) + (len u2)
by A8, FINSEQ_1:22;
hence
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
by A9, A15, A13, A17, A16, A35, A18, MATRIXJ1:23; verum