# Metamath Proof Explorer

## Theorem m2detleib

Description: Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018) (Revised by AV, 26-Dec-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses m2detleib.n
`|- N = { 1 , 2 }`
m2detleib.d
`|- D = ( N maDet R )`
m2detleib.a
`|- A = ( N Mat R )`
m2detleib.b
`|- B = ( Base ` A )`
m2detleib.m
`|- .- = ( -g ` R )`
m2detleib.t
`|- .x. = ( .r ` R )`
Assertion m2detleib
`|- ( ( R e. Ring /\ M e. B ) -> ( D ` M ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )`

### Proof

Step Hyp Ref Expression
1 m2detleib.n
` |-  N = { 1 , 2 }`
2 m2detleib.d
` |-  D = ( N maDet R )`
3 m2detleib.a
` |-  A = ( N Mat R )`
4 m2detleib.b
` |-  B = ( Base ` A )`
5 m2detleib.m
` |-  .- = ( -g ` R )`
6 m2detleib.t
` |-  .x. = ( .r ` R )`
7 eqid
` |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )`
8 eqid
` |-  ( ZRHom ` R ) = ( ZRHom ` R )`
9 eqid
` |-  ( pmSgn ` N ) = ( pmSgn ` N )`
10 eqid
` |-  ( mulGrp ` R ) = ( mulGrp ` R )`
11 2 3 4 7 8 9 6 10 mdetleib1
` |-  ( M e. B -> ( D ` M ) = ( R gsum ( k e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) )`
` |-  ( ( R e. Ring /\ M e. B ) -> ( D ` M ) = ( R gsum ( k e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) )`
13 eqid
` |-  ( Base ` R ) = ( Base ` R )`
14 eqid
` |-  ( +g ` R ) = ( +g ` R )`
15 ringcmn
` |-  ( R e. Ring -> R e. CMnd )`
` |-  ( ( R e. Ring /\ M e. B ) -> R e. CMnd )`
17 prfi
` |-  { 1 , 2 } e. Fin`
18 1 17 eqeltri
` |-  N e. Fin`
19 eqid
` |-  ( SymGrp ` N ) = ( SymGrp ` N )`
20 19 7 symgbasfi
` |-  ( N e. Fin -> ( Base ` ( SymGrp ` N ) ) e. Fin )`
21 18 20 ax-mp
` |-  ( Base ` ( SymGrp ` N ) ) e. Fin`
22 21 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> ( Base ` ( SymGrp ` N ) ) e. Fin )`
23 simpl
` |-  ( ( R e. Ring /\ M e. B ) -> R e. Ring )`
` |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> R e. Ring )`
25 7 9 8 zrhpsgnelbas
` |-  ( ( R e. Ring /\ N e. Fin /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) e. ( Base ` R ) )`
26 18 25 mp3an2
` |-  ( ( R e. Ring /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) e. ( Base ` R ) )`
` |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) e. ( Base ` R ) )`
28 simpr
` |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> k e. ( Base ` ( SymGrp ` N ) ) )`
29 simpr
` |-  ( ( R e. Ring /\ M e. B ) -> M e. B )`
` |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> M e. B )`
31 1 7 3 4 10 m2detleiblem2
` |-  ( ( R e. Ring /\ k e. ( Base ` ( SymGrp ` N ) ) /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) e. ( Base ` R ) )`
32 24 28 30 31 syl3anc
` |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) e. ( Base ` R ) )`
33 13 6 ringcl
` |-  ( ( R e. Ring /\ ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) e. ( Base ` R ) ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) e. ( Base ` R ) )`
34 24 27 32 33 syl3anc
` |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) e. ( Base ` R ) )`
35 opex
` |-  <. 1 , 1 >. e. _V`
36 opex
` |-  <. 2 , 2 >. e. _V`
37 35 36 pm3.2i
` |-  ( <. 1 , 1 >. e. _V /\ <. 2 , 2 >. e. _V )`
38 opex
` |-  <. 1 , 2 >. e. _V`
39 opex
` |-  <. 2 , 1 >. e. _V`
40 38 39 pm3.2i
` |-  ( <. 1 , 2 >. e. _V /\ <. 2 , 1 >. e. _V )`
41 37 40 pm3.2i
` |-  ( ( <. 1 , 1 >. e. _V /\ <. 2 , 2 >. e. _V ) /\ ( <. 1 , 2 >. e. _V /\ <. 2 , 1 >. e. _V ) )`
42 1ne2
` |-  1 =/= 2`
43 42 olci
` |-  ( 1 =/= 1 \/ 1 =/= 2 )`
44 1ex
` |-  1 e. _V`
45 44 44 opthne
` |-  ( <. 1 , 1 >. =/= <. 1 , 2 >. <-> ( 1 =/= 1 \/ 1 =/= 2 ) )`
46 43 45 mpbir
` |-  <. 1 , 1 >. =/= <. 1 , 2 >.`
47 42 orci
` |-  ( 1 =/= 2 \/ 1 =/= 1 )`
48 44 44 opthne
` |-  ( <. 1 , 1 >. =/= <. 2 , 1 >. <-> ( 1 =/= 2 \/ 1 =/= 1 ) )`
49 47 48 mpbir
` |-  <. 1 , 1 >. =/= <. 2 , 1 >.`
50 46 49 pm3.2i
` |-  ( <. 1 , 1 >. =/= <. 1 , 2 >. /\ <. 1 , 1 >. =/= <. 2 , 1 >. )`
51 50 orci
` |-  ( ( <. 1 , 1 >. =/= <. 1 , 2 >. /\ <. 1 , 1 >. =/= <. 2 , 1 >. ) \/ ( <. 2 , 2 >. =/= <. 1 , 2 >. /\ <. 2 , 2 >. =/= <. 2 , 1 >. ) )`
52 41 51 pm3.2i
` |-  ( ( ( <. 1 , 1 >. e. _V /\ <. 2 , 2 >. e. _V ) /\ ( <. 1 , 2 >. e. _V /\ <. 2 , 1 >. e. _V ) ) /\ ( ( <. 1 , 1 >. =/= <. 1 , 2 >. /\ <. 1 , 1 >. =/= <. 2 , 1 >. ) \/ ( <. 2 , 2 >. =/= <. 1 , 2 >. /\ <. 2 , 2 >. =/= <. 2 , 1 >. ) ) )`
53 52 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( <. 1 , 1 >. e. _V /\ <. 2 , 2 >. e. _V ) /\ ( <. 1 , 2 >. e. _V /\ <. 2 , 1 >. e. _V ) ) /\ ( ( <. 1 , 1 >. =/= <. 1 , 2 >. /\ <. 1 , 1 >. =/= <. 2 , 1 >. ) \/ ( <. 2 , 2 >. =/= <. 1 , 2 >. /\ <. 2 , 2 >. =/= <. 2 , 1 >. ) ) ) )`
54 prneimg
` |-  ( ( ( <. 1 , 1 >. e. _V /\ <. 2 , 2 >. e. _V ) /\ ( <. 1 , 2 >. e. _V /\ <. 2 , 1 >. e. _V ) ) -> ( ( ( <. 1 , 1 >. =/= <. 1 , 2 >. /\ <. 1 , 1 >. =/= <. 2 , 1 >. ) \/ ( <. 2 , 2 >. =/= <. 1 , 2 >. /\ <. 2 , 2 >. =/= <. 2 , 1 >. ) ) -> { <. 1 , 1 >. , <. 2 , 2 >. } =/= { <. 1 , 2 >. , <. 2 , 1 >. } ) )`
55 54 imp
` |-  ( ( ( ( <. 1 , 1 >. e. _V /\ <. 2 , 2 >. e. _V ) /\ ( <. 1 , 2 >. e. _V /\ <. 2 , 1 >. e. _V ) ) /\ ( ( <. 1 , 1 >. =/= <. 1 , 2 >. /\ <. 1 , 1 >. =/= <. 2 , 1 >. ) \/ ( <. 2 , 2 >. =/= <. 1 , 2 >. /\ <. 2 , 2 >. =/= <. 2 , 1 >. ) ) ) -> { <. 1 , 1 >. , <. 2 , 2 >. } =/= { <. 1 , 2 >. , <. 2 , 1 >. } )`
56 disjsn2
` |-  ( { <. 1 , 1 >. , <. 2 , 2 >. } =/= { <. 1 , 2 >. , <. 2 , 1 >. } -> ( { { <. 1 , 1 >. , <. 2 , 2 >. } } i^i { { <. 1 , 2 >. , <. 2 , 1 >. } } ) = (/) )`
57 53 55 56 3syl
` |-  ( ( R e. Ring /\ M e. B ) -> ( { { <. 1 , 1 >. , <. 2 , 2 >. } } i^i { { <. 1 , 2 >. , <. 2 , 1 >. } } ) = (/) )`
58 2nn
` |-  2 e. NN`
59 19 7 1 symg2bas
` |-  ( ( 1 e. _V /\ 2 e. NN ) -> ( Base ` ( SymGrp ` N ) ) = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )`
60 44 58 59 mp2an
` |-  ( Base ` ( SymGrp ` N ) ) = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }`
61 df-pr
` |-  { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } = ( { { <. 1 , 1 >. , <. 2 , 2 >. } } u. { { <. 1 , 2 >. , <. 2 , 1 >. } } )`
62 60 61 eqtri
` |-  ( Base ` ( SymGrp ` N ) ) = ( { { <. 1 , 1 >. , <. 2 , 2 >. } } u. { { <. 1 , 2 >. , <. 2 , 1 >. } } )`
63 62 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> ( Base ` ( SymGrp ` N ) ) = ( { { <. 1 , 1 >. , <. 2 , 2 >. } } u. { { <. 1 , 2 >. , <. 2 , 1 >. } } ) )`
64 13 14 16 22 34 57 63 gsummptfidmsplit
` |-  ( ( R e. Ring /\ M e. B ) -> ( R gsum ( k e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) = ( ( R gsum ( k e. { { <. 1 , 1 >. , <. 2 , 2 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) ( +g ` R ) ( R gsum ( k e. { { <. 1 , 2 >. , <. 2 , 1 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) ) )`
65 ringmnd
` |-  ( R e. Ring -> R e. Mnd )`
` |-  ( ( R e. Ring /\ M e. B ) -> R e. Mnd )`
67 prex
` |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. _V`
68 67 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> { <. 1 , 1 >. , <. 2 , 2 >. } e. _V )`
69 67 prid1
` |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }`
70 69 60 eleqtrri
` |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. ( Base ` ( SymGrp ` N ) )`
71 70 a1i
` |-  ( M e. B -> { <. 1 , 1 >. , <. 2 , 2 >. } e. ( Base ` ( SymGrp ` N ) ) )`
72 7 9 8 zrhpsgnelbas
` |-  ( ( R e. Ring /\ N e. Fin /\ { <. 1 , 1 >. , <. 2 , 2 >. } e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) e. ( Base ` R ) )`
73 18 72 mp3an2
` |-  ( ( R e. Ring /\ { <. 1 , 1 >. , <. 2 , 2 >. } e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) e. ( Base ` R ) )`
74 71 73 sylan2
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) e. ( Base ` R ) )`
75 1 7 3 4 10 m2detleiblem2
` |-  ( ( R e. Ring /\ { <. 1 , 1 >. , <. 2 , 2 >. } e. ( Base ` ( SymGrp ` N ) ) /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) e. ( Base ` R ) )`
76 70 75 mp3an2
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) e. ( Base ` R ) )`
77 13 6 ringcl
` |-  ( ( R e. Ring /\ ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) e. ( Base ` R ) ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) e. ( Base ` R ) )`
78 23 74 76 77 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) e. ( Base ` R ) )`
79 2fveq3
` |-  ( k = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) = ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) )`
80 fveq1
` |-  ( k = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( k ` n ) = ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) )`
81 80 oveq1d
` |-  ( k = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( ( k ` n ) M n ) = ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) )`
82 81 mpteq2dv
` |-  ( k = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( n e. N |-> ( ( k ` n ) M n ) ) = ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) )`
83 82 oveq2d
` |-  ( k = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) = ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) )`
84 79 83 oveq12d
` |-  ( k = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) = ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) )`
85 13 84 gsumsn
` |-  ( ( R e. Mnd /\ { <. 1 , 1 >. , <. 2 , 2 >. } e. _V /\ ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) e. ( Base ` R ) ) -> ( R gsum ( k e. { { <. 1 , 1 >. , <. 2 , 2 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) = ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) )`
86 66 68 78 85 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( R gsum ( k e. { { <. 1 , 1 >. , <. 2 , 2 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) = ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) )`
87 prex
` |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. _V`
88 87 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> { <. 1 , 2 >. , <. 2 , 1 >. } e. _V )`
89 87 prid2
` |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }`
90 89 60 eleqtrri
` |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. ( Base ` ( SymGrp ` N ) )`
91 90 a1i
` |-  ( M e. B -> { <. 1 , 2 >. , <. 2 , 1 >. } e. ( Base ` ( SymGrp ` N ) ) )`
92 7 9 8 zrhpsgnelbas
` |-  ( ( R e. Ring /\ N e. Fin /\ { <. 1 , 2 >. , <. 2 , 1 >. } e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) e. ( Base ` R ) )`
93 18 92 mp3an2
` |-  ( ( R e. Ring /\ { <. 1 , 2 >. , <. 2 , 1 >. } e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) e. ( Base ` R ) )`
94 91 93 sylan2
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) e. ( Base ` R ) )`
95 1 7 3 4 10 m2detleiblem2
` |-  ( ( R e. Ring /\ { <. 1 , 2 >. , <. 2 , 1 >. } e. ( Base ` ( SymGrp ` N ) ) /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) e. ( Base ` R ) )`
96 90 95 mp3an2
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) e. ( Base ` R ) )`
97 13 6 ringcl
` |-  ( ( R e. Ring /\ ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) e. ( Base ` R ) ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) e. ( Base ` R ) )`
98 23 94 96 97 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) e. ( Base ` R ) )`
99 2fveq3
` |-  ( k = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) = ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) )`
100 fveq1
` |-  ( k = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( k ` n ) = ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) )`
101 100 oveq1d
` |-  ( k = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( ( k ` n ) M n ) = ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) )`
102 101 mpteq2dv
` |-  ( k = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( n e. N |-> ( ( k ` n ) M n ) ) = ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) )`
103 102 oveq2d
` |-  ( k = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) = ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) )`
104 99 103 oveq12d
` |-  ( k = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) = ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) )`
105 13 104 gsumsn
` |-  ( ( R e. Mnd /\ { <. 1 , 2 >. , <. 2 , 1 >. } e. _V /\ ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) e. ( Base ` R ) ) -> ( R gsum ( k e. { { <. 1 , 2 >. , <. 2 , 1 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) = ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) )`
106 66 88 98 105 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( R gsum ( k e. { { <. 1 , 2 >. , <. 2 , 1 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) = ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) )`
107 86 106 oveq12d
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( R gsum ( k e. { { <. 1 , 1 >. , <. 2 , 2 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) ( +g ` R ) ( R gsum ( k e. { { <. 1 , 2 >. , <. 2 , 1 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) ) = ( ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) ( +g ` R ) ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) ) )`
108 eqidd
` |-  ( M e. B -> { <. 1 , 1 >. , <. 2 , 2 >. } = { <. 1 , 1 >. , <. 2 , 2 >. } )`
109 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
110 1 7 8 9 109 m2detleiblem5
` |-  ( ( R e. Ring /\ { <. 1 , 1 >. , <. 2 , 2 >. } = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) = ( 1r ` R ) )`
111 108 110 sylan2
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) = ( 1r ` R ) )`
112 eqidd
` |-  ( ( R e. Ring /\ M e. B ) -> { <. 1 , 1 >. , <. 2 , 2 >. } = { <. 1 , 1 >. , <. 2 , 2 >. } )`
113 10 6 mgpplusg
` |-  .x. = ( +g ` ( mulGrp ` R ) )`
114 1 7 3 4 10 113 m2detleiblem3
` |-  ( ( R e. Ring /\ { <. 1 , 1 >. , <. 2 , 2 >. } = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`
115 23 112 29 114 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`
116 111 115 oveq12d
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) = ( ( 1r ` R ) .x. ( ( 1 M 1 ) .x. ( 2 M 2 ) ) ) )`
117 44 prid1
` |-  1 e. { 1 , 2 }`
118 117 1 eleqtrri
` |-  1 e. N`
119 118 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> 1 e. N )`
120 4 eleq2i
` |-  ( M e. B <-> M e. ( Base ` A ) )`
121 120 biimpi
` |-  ( M e. B -> M e. ( Base ` A ) )`
` |-  ( ( R e. Ring /\ M e. B ) -> M e. ( Base ` A ) )`
123 3 13 matecl
` |-  ( ( 1 e. N /\ 1 e. N /\ M e. ( Base ` A ) ) -> ( 1 M 1 ) e. ( Base ` R ) )`
124 119 119 122 123 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( 1 M 1 ) e. ( Base ` R ) )`
125 prid2g
` |-  ( 2 e. NN -> 2 e. { 1 , 2 } )`
126 58 125 ax-mp
` |-  2 e. { 1 , 2 }`
127 126 1 eleqtrri
` |-  2 e. N`
128 127 a1i
` |-  ( ( R e. Ring /\ M e. B ) -> 2 e. N )`
129 3 13 matecl
` |-  ( ( 2 e. N /\ 2 e. N /\ M e. ( Base ` A ) ) -> ( 2 M 2 ) e. ( Base ` R ) )`
130 128 128 122 129 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( 2 M 2 ) e. ( Base ` R ) )`
131 13 6 ringcl
` |-  ( ( R e. Ring /\ ( 1 M 1 ) e. ( Base ` R ) /\ ( 2 M 2 ) e. ( Base ` R ) ) -> ( ( 1 M 1 ) .x. ( 2 M 2 ) ) e. ( Base ` R ) )`
132 23 124 130 131 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( 1 M 1 ) .x. ( 2 M 2 ) ) e. ( Base ` R ) )`
133 13 6 109 ringlidm
` |-  ( ( R e. Ring /\ ( ( 1 M 1 ) .x. ( 2 M 2 ) ) e. ( Base ` R ) ) -> ( ( 1r ` R ) .x. ( ( 1 M 1 ) .x. ( 2 M 2 ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`
134 132 133 syldan
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( 1r ` R ) .x. ( ( 1 M 1 ) .x. ( 2 M 2 ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`
135 116 134 eqtrd
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`
136 eqidd
` |-  ( M e. B -> { <. 1 , 2 >. , <. 2 , 1 >. } = { <. 1 , 2 >. , <. 2 , 1 >. } )`
137 eqid
` |-  ( invg ` R ) = ( invg ` R )`
138 1 7 8 9 109 137 m2detleiblem6
` |-  ( ( R e. Ring /\ { <. 1 , 2 >. , <. 2 , 1 >. } = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )`
139 136 138 sylan2
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )`
140 eqidd
` |-  ( ( R e. Ring /\ M e. B ) -> { <. 1 , 2 >. , <. 2 , 1 >. } = { <. 1 , 2 >. , <. 2 , 1 >. } )`
141 1 7 3 4 10 113 m2detleiblem4
` |-  ( ( R e. Ring /\ { <. 1 , 2 >. , <. 2 , 1 >. } = { <. 1 , 2 >. , <. 2 , 1 >. } /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) = ( ( 2 M 1 ) .x. ( 1 M 2 ) ) )`
142 23 140 29 141 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) = ( ( 2 M 1 ) .x. ( 1 M 2 ) ) )`
143 139 142 oveq12d
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) = ( ( ( invg ` R ) ` ( 1r ` R ) ) .x. ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )`
144 135 143 oveq12d
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 1 >. , <. 2 , 2 >. } ` n ) M n ) ) ) ) ( +g ` R ) ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( { <. 1 , 2 >. , <. 2 , 1 >. } ` n ) M n ) ) ) ) ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) ( +g ` R ) ( ( ( invg ` R ) ` ( 1r ` R ) ) .x. ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) ) )`
145 3 13 matecl
` |-  ( ( 2 e. N /\ 1 e. N /\ M e. ( Base ` A ) ) -> ( 2 M 1 ) e. ( Base ` R ) )`
146 128 119 122 145 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( 2 M 1 ) e. ( Base ` R ) )`
147 3 13 matecl
` |-  ( ( 1 e. N /\ 2 e. N /\ M e. ( Base ` A ) ) -> ( 1 M 2 ) e. ( Base ` R ) )`
148 119 128 122 147 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( 1 M 2 ) e. ( Base ` R ) )`
149 13 6 ringcl
` |-  ( ( R e. Ring /\ ( 2 M 1 ) e. ( Base ` R ) /\ ( 1 M 2 ) e. ( Base ` R ) ) -> ( ( 2 M 1 ) .x. ( 1 M 2 ) ) e. ( Base ` R ) )`
150 23 146 148 149 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( 2 M 1 ) .x. ( 1 M 2 ) ) e. ( Base ` R ) )`
151 1 7 8 9 109 137 6 5 m2detleiblem7
` |-  ( ( R e. Ring /\ ( ( 1 M 1 ) .x. ( 2 M 2 ) ) e. ( Base ` R ) /\ ( ( 2 M 1 ) .x. ( 1 M 2 ) ) e. ( Base ` R ) ) -> ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) ( +g ` R ) ( ( ( invg ` R ) ` ( 1r ` R ) ) .x. ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )`
152 23 132 150 151 syl3anc
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) ( +g ` R ) ( ( ( invg ` R ) ` ( 1r ` R ) ) .x. ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )`
153 107 144 152 3eqtrd
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( R gsum ( k e. { { <. 1 , 1 >. , <. 2 , 2 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) ( +g ` R ) ( R gsum ( k e. { { <. 1 , 2 >. , <. 2 , 1 >. } } |-> ( ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` k ) ) .x. ( ( mulGrp ` R ) gsum ( n e. N |-> ( ( k ` n ) M n ) ) ) ) ) ) ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )`
154 12 64 153 3eqtrd
` |-  ( ( R e. Ring /\ M e. B ) -> ( D ` M ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )`