let K be Field; for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))
let a1, a2, b1, b2, c1, c2, d1, d2 be Element of K; ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))
reconsider A = (a1,b1) ][ (c1,d1) as Matrix of 2,K ;
reconsider B = (a2,b2) ][ (c2,d2) as Matrix of 2,K ;
reconsider D = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))) as Matrix of 2,K ;
A1:
width A = 2
by MATRIX_0:24;
2 in {1,2}
by TARSKI:def 2;
then A2: (Line (A,2)) . 2 =
A * (2,2)
by A1, FINSEQ_1:2, MATRIX_0:def 7
.=
d1
by MATRIX_0:50
;
A3: len (Line (A,2)) =
width A
by MATRIX_0:def 7
.=
2
by MATRIX_0:24
;
1 in {1,2}
by TARSKI:def 2;
then (Line (A,2)) . 1 =
A * (2,1)
by A1, FINSEQ_1:2, MATRIX_0:def 7
.=
c1
by MATRIX_0:50
;
then A4:
Line (A,2) = <*c1,d1*>
by A3, A2, FINSEQ_1:44;
2 in {1,2}
by TARSKI:def 2;
then A5: (Line (A,1)) . 2 =
A * (1,2)
by A1, FINSEQ_1:2, MATRIX_0:def 7
.=
b1
by MATRIX_0:50
;
A6: len (Line (A,1)) =
width A
by MATRIX_0:def 7
.=
2
by MATRIX_0:24
;
1 in {1,2}
by TARSKI:def 2;
then (Line (A,1)) . 1 =
A * (1,1)
by A1, FINSEQ_1:2, MATRIX_0:def 7
.=
a1
by MATRIX_0:50
;
then A7:
Line (A,1) = <*a1,b1*>
by A6, A5, FINSEQ_1:44;
A8: len (Col (B,2)) =
len B
by MATRIX_0:def 8
.=
2
by MATRIX_0:24
;
A9: len (Col (B,1)) =
len B
by MATRIX_0:def 8
.=
2
by MATRIX_0:24
;
reconsider C = A * B as Matrix of K ;
A10:
len B = 2
by MATRIX_0:24;
width B = 2
by MATRIX_0:24;
then A11:
width C = 2
by A1, A10, Def4;
len A = 2
by MATRIX_0:24;
then A12:
len C = 2
by A1, A10, Def4;
then reconsider C = C as Matrix of 2,K by A11, MATRIX_0:51;
A13:
Seg (len B) = dom B
by FINSEQ_1:def 3;
2 in {1,2}
by TARSKI:def 2;
then A14: (Col (B,2)) . 2 =
B * (2,2)
by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.=
d2
by MATRIX_0:50
;
1 in {1,2}
by TARSKI:def 2;
then (Col (B,2)) . 1 =
B * (1,2)
by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.=
b2
by MATRIX_0:50
;
then A15:
Col (B,2) = <*b2,d2*>
by A8, A14, FINSEQ_1:44;
2 in {1,2}
by TARSKI:def 2;
then A16: (Col (B,1)) . 2 =
B * (2,1)
by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.=
c2
by MATRIX_0:50
;
1 in {1,2}
by TARSKI:def 2;
then (Col (B,1)) . 1 =
B * (1,1)
by A10, A13, FINSEQ_1:2, MATRIX_0:def 8
.=
a2
by MATRIX_0:50
;
then A17:
Col (B,1) = <*a2,c2*>
by A9, A16, FINSEQ_1:44;
dom C = Seg (len C)
by FINSEQ_1:def 3;
then A18:
Indices C = [:(Seg 2),(Seg 2):]
by A12, A11;
now for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = D * (i,j)let i,
j be
Nat;
( [i,j] in Indices C implies C * (i,j) = D * (i,j) )assume A19:
[i,j] in Indices C
;
C * (i,j) = D * (i,j)then A20:
(
i in Seg 2 &
j in Seg 2 )
by A18, ZFMISC_1:87;
now ( ( i = 1 & j = 1 & C * (1,1) = D * (1,1) ) or ( i = 1 & j = 2 & C * (1,2) = D * (1,2) ) or ( i = 2 & j = 1 & C * (2,1) = D * (2,1) ) or ( i = 2 & j = 2 & C * (2,2) = D * (2,2) ) )per cases
( ( i = 1 & j = 1 ) or ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) or ( i = 2 & j = 2 ) )
by A20, FINSEQ_1:2, TARSKI:def 2;
case
(
i = 1 &
j = 1 )
;
C * (1,1) = D * (1,1)end; case
(
i = 1 &
j = 2 )
;
C * (1,2) = D * (1,2)end; case
(
i = 2 &
j = 1 )
;
C * (2,1) = D * (2,1)end; case
(
i = 2 &
j = 2 )
;
C * (2,2) = D * (2,2)end; hence
C * (
i,
j)
= D * (
i,
j)
;
verum end;
hence
((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))
by MATRIX_0:27; verum