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 ) ) ) ) ) ) )
12 11 adantl 
 |-  ( ( 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 )
16 15 adantr 
 |-  ( ( 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 )
24 23 adantr 
 |-  ( ( ( 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 ) )
27 26 adantlr 
 |-  ( ( ( 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 )
30 29 adantr 
 |-  ( ( ( 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 )
66 65 adantr 
 |-  ( ( 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 ) )
122 121 adantl 
 |-  ( ( 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 ) ) ) )