Metamath Proof Explorer


Theorem m1detdiag

Description: The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypotheses mdetdiag.d
|- D = ( N maDet R )
mdetdiag.a
|- A = ( N Mat R )
mdetdiag.b
|- B = ( Base ` A )
Assertion m1detdiag
|- ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( D ` M ) = ( I M I ) )

Proof

Step Hyp Ref Expression
1 mdetdiag.d
 |-  D = ( N maDet R )
2 mdetdiag.a
 |-  A = ( N Mat R )
3 mdetdiag.b
 |-  B = ( Base ` A )
4 eqid
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
5 eqid
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
6 eqid
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
7 eqid
 |-  ( .r ` R ) = ( .r ` R )
8 eqid
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 1 2 3 4 5 6 7 8 mdetleib
 |-  ( M e. B -> ( D ` M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )
10 9 3ad2ant3
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( D ` M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )
11 2fveq3
 |-  ( N = { I } -> ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` { I } ) ) )
12 11 adantr
 |-  ( ( N = { I } /\ I e. V ) -> ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` { I } ) ) )
13 12 3ad2ant2
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` { I } ) ) )
14 simp2r
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> I e. V )
15 eqid
 |-  ( SymGrp ` { I } ) = ( SymGrp ` { I } )
16 eqid
 |-  ( Base ` ( SymGrp ` { I } ) ) = ( Base ` ( SymGrp ` { I } ) )
17 eqid
 |-  { I } = { I }
18 15 16 17 symg1bas
 |-  ( I e. V -> ( Base ` ( SymGrp ` { I } ) ) = { { <. I , I >. } } )
19 14 18 syl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Base ` ( SymGrp ` { I } ) ) = { { <. I , I >. } } )
20 13 19 eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Base ` ( SymGrp ` N ) ) = { { <. I , I >. } } )
21 20 mpteq1d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) = ( p e. { { <. I , I >. } } |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) )
22 snex
 |-  { <. I , I >. } e. _V
23 22 a1i
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { <. I , I >. } e. _V )
24 ovex
 |-  ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) e. _V
25 fveq2
 |-  ( p = { <. I , I >. } -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) )
26 fveq1
 |-  ( p = { <. I , I >. } -> ( p ` x ) = ( { <. I , I >. } ` x ) )
27 26 oveq1d
 |-  ( p = { <. I , I >. } -> ( ( p ` x ) M x ) = ( ( { <. I , I >. } ` x ) M x ) )
28 27 mpteq2dv
 |-  ( p = { <. I , I >. } -> ( x e. N |-> ( ( p ` x ) M x ) ) = ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) )
29 28 oveq2d
 |-  ( p = { <. I , I >. } -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) = ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) )
30 25 29 oveq12d
 |-  ( p = { <. I , I >. } -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) )
31 30 fmptsng
 |-  ( ( { <. I , I >. } e. _V /\ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) e. _V ) -> { <. { <. I , I >. } , ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) >. } = ( p e. { { <. I , I >. } } |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) )
32 31 eqcomd
 |-  ( ( { <. I , I >. } e. _V /\ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) e. _V ) -> ( p e. { { <. I , I >. } } |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) = { <. { <. I , I >. } , ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) >. } )
33 23 24 32 sylancl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( p e. { { <. I , I >. } } |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) = { <. { <. I , I >. } , ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) >. } )
34 eqid
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
35 eqid
 |-  { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin } = { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin }
36 34 4 35 6 psgnfn
 |-  ( pmSgn ` N ) Fn { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin }
37 18 adantl
 |-  ( ( N = { I } /\ I e. V ) -> ( Base ` ( SymGrp ` { I } ) ) = { { <. I , I >. } } )
38 12 37 eqtrd
 |-  ( ( N = { I } /\ I e. V ) -> ( Base ` ( SymGrp ` N ) ) = { { <. I , I >. } } )
39 38 3ad2ant2
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Base ` ( SymGrp ` N ) ) = { { <. I , I >. } } )
40 rabeq
 |-  ( ( Base ` ( SymGrp ` N ) ) = { { <. I , I >. } } -> { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin } = { b e. { { <. I , I >. } } | dom ( b \ _I ) e. Fin } )
41 39 40 syl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin } = { b e. { { <. I , I >. } } | dom ( b \ _I ) e. Fin } )
42 difeq1
 |-  ( b = { <. I , I >. } -> ( b \ _I ) = ( { <. I , I >. } \ _I ) )
43 42 dmeqd
 |-  ( b = { <. I , I >. } -> dom ( b \ _I ) = dom ( { <. I , I >. } \ _I ) )
44 43 eleq1d
 |-  ( b = { <. I , I >. } -> ( dom ( b \ _I ) e. Fin <-> dom ( { <. I , I >. } \ _I ) e. Fin ) )
45 44 rabsnif
 |-  { b e. { { <. I , I >. } } | dom ( b \ _I ) e. Fin } = if ( dom ( { <. I , I >. } \ _I ) e. Fin , { { <. I , I >. } } , (/) )
46 45 a1i
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { b e. { { <. I , I >. } } | dom ( b \ _I ) e. Fin } = if ( dom ( { <. I , I >. } \ _I ) e. Fin , { { <. I , I >. } } , (/) ) )
47 restidsing
 |-  ( _I |` { I } ) = ( { I } X. { I } )
48 xpsng
 |-  ( ( I e. V /\ I e. V ) -> ( { I } X. { I } ) = { <. I , I >. } )
49 48 anidms
 |-  ( I e. V -> ( { I } X. { I } ) = { <. I , I >. } )
50 47 49 eqtr2id
 |-  ( I e. V -> { <. I , I >. } = ( _I |` { I } ) )
51 fnsng
 |-  ( ( I e. V /\ I e. V ) -> { <. I , I >. } Fn { I } )
52 51 anidms
 |-  ( I e. V -> { <. I , I >. } Fn { I } )
53 fnnfpeq0
 |-  ( { <. I , I >. } Fn { I } -> ( dom ( { <. I , I >. } \ _I ) = (/) <-> { <. I , I >. } = ( _I |` { I } ) ) )
54 52 53 syl
 |-  ( I e. V -> ( dom ( { <. I , I >. } \ _I ) = (/) <-> { <. I , I >. } = ( _I |` { I } ) ) )
55 50 54 mpbird
 |-  ( I e. V -> dom ( { <. I , I >. } \ _I ) = (/) )
56 0fin
 |-  (/) e. Fin
57 55 56 eqeltrdi
 |-  ( I e. V -> dom ( { <. I , I >. } \ _I ) e. Fin )
58 57 adantl
 |-  ( ( N = { I } /\ I e. V ) -> dom ( { <. I , I >. } \ _I ) e. Fin )
59 58 3ad2ant2
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> dom ( { <. I , I >. } \ _I ) e. Fin )
60 59 iftrued
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> if ( dom ( { <. I , I >. } \ _I ) e. Fin , { { <. I , I >. } } , (/) ) = { { <. I , I >. } } )
61 41 46 60 3eqtrrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { { <. I , I >. } } = { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin } )
62 61 fneq2d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( pmSgn ` N ) Fn { { <. I , I >. } } <-> ( pmSgn ` N ) Fn { b e. ( Base ` ( SymGrp ` N ) ) | dom ( b \ _I ) e. Fin } ) )
63 36 62 mpbiri
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( pmSgn ` N ) Fn { { <. I , I >. } } )
64 22 snid
 |-  { <. I , I >. } e. { { <. I , I >. } }
65 fvco2
 |-  ( ( ( pmSgn ` N ) Fn { { <. I , I >. } } /\ { <. I , I >. } e. { { <. I , I >. } } ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) = ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. I , I >. } ) ) )
66 63 64 65 sylancl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) = ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. I , I >. } ) ) )
67 fveq2
 |-  ( N = { I } -> ( pmSgn ` N ) = ( pmSgn ` { I } ) )
68 67 adantr
 |-  ( ( N = { I } /\ I e. V ) -> ( pmSgn ` N ) = ( pmSgn ` { I } ) )
69 68 3ad2ant2
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( pmSgn ` N ) = ( pmSgn ` { I } ) )
70 69 fveq1d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( pmSgn ` N ) ` { <. I , I >. } ) = ( ( pmSgn ` { I } ) ` { <. I , I >. } ) )
71 snidg
 |-  ( { <. I , I >. } e. _V -> { <. I , I >. } e. { { <. I , I >. } } )
72 22 71 mp1i
 |-  ( I e. V -> { <. I , I >. } e. { { <. I , I >. } } )
73 72 18 eleqtrrd
 |-  ( I e. V -> { <. I , I >. } e. ( Base ` ( SymGrp ` { I } ) ) )
74 73 ancli
 |-  ( I e. V -> ( I e. V /\ { <. I , I >. } e. ( Base ` ( SymGrp ` { I } ) ) ) )
75 74 adantl
 |-  ( ( N = { I } /\ I e. V ) -> ( I e. V /\ { <. I , I >. } e. ( Base ` ( SymGrp ` { I } ) ) ) )
76 75 3ad2ant2
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I e. V /\ { <. I , I >. } e. ( Base ` ( SymGrp ` { I } ) ) ) )
77 eqid
 |-  ( pmSgn ` { I } ) = ( pmSgn ` { I } )
78 17 15 16 77 psgnsn
 |-  ( ( I e. V /\ { <. I , I >. } e. ( Base ` ( SymGrp ` { I } ) ) ) -> ( ( pmSgn ` { I } ) ` { <. I , I >. } ) = 1 )
79 76 78 syl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( pmSgn ` { I } ) ` { <. I , I >. } ) = 1 )
80 70 79 eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( pmSgn ` N ) ` { <. I , I >. } ) = 1 )
81 80 fveq2d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ZRHom ` R ) ` ( ( pmSgn ` N ) ` { <. I , I >. } ) ) = ( ( ZRHom ` R ) ` 1 ) )
82 crngring
 |-  ( R e. CRing -> R e. Ring )
83 82 3ad2ant1
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> R e. Ring )
84 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
85 5 84 zrh1
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 1 ) = ( 1r ` R ) )
86 83 85 syl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ZRHom ` R ) ` 1 ) = ( 1r ` R ) )
87 66 81 86 3eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) = ( 1r ` R ) )
88 simp2l
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> N = { I } )
89 88 mpteq1d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) = ( x e. { I } |-> ( ( { <. I , I >. } ` x ) M x ) ) )
90 89 oveq2d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) = ( ( mulGrp ` R ) gsum ( x e. { I } |-> ( ( { <. I , I >. } ` x ) M x ) ) ) )
91 8 ringmgp
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
92 82 91 syl
 |-  ( R e. CRing -> ( mulGrp ` R ) e. Mnd )
93 92 3ad2ant1
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( mulGrp ` R ) e. Mnd )
94 snidg
 |-  ( I e. V -> I e. { I } )
95 94 adantl
 |-  ( ( N = { I } /\ I e. V ) -> I e. { I } )
96 eleq2
 |-  ( N = { I } -> ( I e. N <-> I e. { I } ) )
97 96 adantr
 |-  ( ( N = { I } /\ I e. V ) -> ( I e. N <-> I e. { I } ) )
98 95 97 mpbird
 |-  ( ( N = { I } /\ I e. V ) -> I e. N )
99 3 eleq2i
 |-  ( M e. B <-> M e. ( Base ` A ) )
100 99 biimpi
 |-  ( M e. B -> M e. ( Base ` A ) )
101 simpl
 |-  ( ( I e. N /\ M e. ( Base ` A ) ) -> I e. N )
102 simpr
 |-  ( ( I e. N /\ M e. ( Base ` A ) ) -> M e. ( Base ` A ) )
103 101 101 102 3jca
 |-  ( ( I e. N /\ M e. ( Base ` A ) ) -> ( I e. N /\ I e. N /\ M e. ( Base ` A ) ) )
104 98 100 103 syl2an
 |-  ( ( ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I e. N /\ I e. N /\ M e. ( Base ` A ) ) )
105 104 3adant1
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I e. N /\ I e. N /\ M e. ( Base ` A ) ) )
106 eqid
 |-  ( Base ` R ) = ( Base ` R )
107 2 106 matecl
 |-  ( ( I e. N /\ I e. N /\ M e. ( Base ` A ) ) -> ( I M I ) e. ( Base ` R ) )
108 105 107 syl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I M I ) e. ( Base ` R ) )
109 8 106 mgpbas
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
110 108 109 eleqtrdi
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I M I ) e. ( Base ` ( mulGrp ` R ) ) )
111 eqid
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
112 fveq2
 |-  ( x = I -> ( { <. I , I >. } ` x ) = ( { <. I , I >. } ` I ) )
113 eqvisset
 |-  ( x = I -> I e. _V )
114 fvsng
 |-  ( ( I e. _V /\ I e. _V ) -> ( { <. I , I >. } ` I ) = I )
115 113 113 114 syl2anc
 |-  ( x = I -> ( { <. I , I >. } ` I ) = I )
116 112 115 eqtrd
 |-  ( x = I -> ( { <. I , I >. } ` x ) = I )
117 id
 |-  ( x = I -> x = I )
118 116 117 oveq12d
 |-  ( x = I -> ( ( { <. I , I >. } ` x ) M x ) = ( I M I ) )
119 111 118 gsumsn
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. V /\ ( I M I ) e. ( Base ` ( mulGrp ` R ) ) ) -> ( ( mulGrp ` R ) gsum ( x e. { I } |-> ( ( { <. I , I >. } ` x ) M x ) ) ) = ( I M I ) )
120 93 14 110 119 syl3anc
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( x e. { I } |-> ( ( { <. I , I >. } ` x ) M x ) ) ) = ( I M I ) )
121 90 120 eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) = ( I M I ) )
122 87 121 oveq12d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) = ( ( 1r ` R ) ( .r ` R ) ( I M I ) ) )
123 98 3ad2ant2
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> I e. N )
124 100 3ad2ant3
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> M e. ( Base ` A ) )
125 123 123 124 107 syl3anc
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I M I ) e. ( Base ` R ) )
126 106 7 84 ringlidm
 |-  ( ( R e. Ring /\ ( I M I ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( I M I ) ) = ( I M I ) )
127 83 125 126 syl2anc
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( 1r ` R ) ( .r ` R ) ( I M I ) ) = ( I M I ) )
128 122 127 eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) = ( I M I ) )
129 128 opeq2d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> <. { <. I , I >. } , ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) >. = <. { <. I , I >. } , ( I M I ) >. )
130 129 sneqd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { <. { <. I , I >. } , ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) >. } = { <. { <. I , I >. } , ( I M I ) >. } )
131 ovex
 |-  ( I M I ) e. _V
132 eqidd
 |-  ( y = { <. I , I >. } -> ( I M I ) = ( I M I ) )
133 132 fmptsng
 |-  ( ( { <. I , I >. } e. _V /\ ( I M I ) e. _V ) -> { <. { <. I , I >. } , ( I M I ) >. } = ( y e. { { <. I , I >. } } |-> ( I M I ) ) )
134 23 131 133 sylancl
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { <. { <. I , I >. } , ( I M I ) >. } = ( y e. { { <. I , I >. } } |-> ( I M I ) ) )
135 130 134 eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> { <. { <. I , I >. } , ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` { <. I , I >. } ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( { <. I , I >. } ` x ) M x ) ) ) ) >. } = ( y e. { { <. I , I >. } } |-> ( I M I ) ) )
136 21 33 135 3eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) = ( y e. { { <. I , I >. } } |-> ( I M I ) ) )
137 136 oveq2d
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) = ( R gsum ( y e. { { <. I , I >. } } |-> ( I M I ) ) ) )
138 ringmnd
 |-  ( R e. Ring -> R e. Mnd )
139 82 138 syl
 |-  ( R e. CRing -> R e. Mnd )
140 139 3ad2ant1
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> R e. Mnd )
141 106 132 gsumsn
 |-  ( ( R e. Mnd /\ { <. I , I >. } e. _V /\ ( I M I ) e. ( Base ` R ) ) -> ( R gsum ( y e. { { <. I , I >. } } |-> ( I M I ) ) ) = ( I M I ) )
142 140 23 125 141 syl3anc
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( R gsum ( y e. { { <. I , I >. } } |-> ( I M I ) ) ) = ( I M I ) )
143 10 137 142 3eqtrd
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( D ` M ) = ( I M I ) )