Step |
Hyp |
Ref |
Expression |
1 |
|
lmat22.m |
|- M = ( litMat ` <" <" A B "> <" C D "> "> ) |
2 |
|
lmat22.a |
|- ( ph -> A e. V ) |
3 |
|
lmat22.b |
|- ( ph -> B e. V ) |
4 |
|
lmat22.c |
|- ( ph -> C e. V ) |
5 |
|
lmat22.d |
|- ( ph -> D e. V ) |
6 |
|
lmat22det.t |
|- .x. = ( .r ` R ) |
7 |
|
lmat22det.s |
|- .- = ( -g ` R ) |
8 |
|
lmat22det.v |
|- V = ( Base ` R ) |
9 |
|
lmat22det.j |
|- J = ( ( 1 ... 2 ) maDet R ) |
10 |
|
lmat22det.r |
|- ( ph -> R e. Ring ) |
11 |
|
2nn |
|- 2 e. NN |
12 |
11
|
a1i |
|- ( ph -> 2 e. NN ) |
13 |
2 3
|
s2cld |
|- ( ph -> <" A B "> e. Word V ) |
14 |
4 5
|
s2cld |
|- ( ph -> <" C D "> e. Word V ) |
15 |
13 14
|
s2cld |
|- ( ph -> <" <" A B "> <" C D "> "> e. Word Word V ) |
16 |
|
s2len |
|- ( # ` <" <" A B "> <" C D "> "> ) = 2 |
17 |
16
|
a1i |
|- ( ph -> ( # ` <" <" A B "> <" C D "> "> ) = 2 ) |
18 |
1 2 3 4 5
|
lmat22lem |
|- ( ( ph /\ i e. ( 0 ..^ 2 ) ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 ) |
19 |
|
eqid |
|- ( ( 1 ... 2 ) Mat R ) = ( ( 1 ... 2 ) Mat R ) |
20 |
|
eqid |
|- ( Base ` ( ( 1 ... 2 ) Mat R ) ) = ( Base ` ( ( 1 ... 2 ) Mat R ) ) |
21 |
1 12 15 17 18 8 19 20 10
|
lmatcl |
|- ( ph -> M e. ( Base ` ( ( 1 ... 2 ) Mat R ) ) ) |
22 |
|
2z |
|- 2 e. ZZ |
23 |
|
fzval3 |
|- ( 2 e. ZZ -> ( 1 ... 2 ) = ( 1 ..^ ( 2 + 1 ) ) ) |
24 |
22 23
|
ax-mp |
|- ( 1 ... 2 ) = ( 1 ..^ ( 2 + 1 ) ) |
25 |
|
2p1e3 |
|- ( 2 + 1 ) = 3 |
26 |
25
|
oveq2i |
|- ( 1 ..^ ( 2 + 1 ) ) = ( 1 ..^ 3 ) |
27 |
|
fzo13pr |
|- ( 1 ..^ 3 ) = { 1 , 2 } |
28 |
24 26 27
|
3eqtri |
|- ( 1 ... 2 ) = { 1 , 2 } |
29 |
28 9 19 20 7 6
|
m2detleib |
|- ( ( R e. Ring /\ M e. ( Base ` ( ( 1 ... 2 ) Mat R ) ) ) -> ( J ` M ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) ) |
30 |
10 21 29
|
syl2anc |
|- ( ph -> ( J ` M ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) ) |
31 |
1 2 3 4 5
|
lmat22e11 |
|- ( ph -> ( 1 M 1 ) = A ) |
32 |
1 2 3 4 5
|
lmat22e22 |
|- ( ph -> ( 2 M 2 ) = D ) |
33 |
31 32
|
oveq12d |
|- ( ph -> ( ( 1 M 1 ) .x. ( 2 M 2 ) ) = ( A .x. D ) ) |
34 |
1 2 3 4 5
|
lmat22e21 |
|- ( ph -> ( 2 M 1 ) = C ) |
35 |
1 2 3 4 5
|
lmat22e12 |
|- ( ph -> ( 1 M 2 ) = B ) |
36 |
34 35
|
oveq12d |
|- ( ph -> ( ( 2 M 1 ) .x. ( 1 M 2 ) ) = ( C .x. B ) ) |
37 |
33 36
|
oveq12d |
|- ( ph -> ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) = ( ( A .x. D ) .- ( C .x. B ) ) ) |
38 |
30 37
|
eqtrd |
|- ( ph -> ( J ` M ) = ( ( A .x. D ) .- ( C .x. B ) ) ) |