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 syl5req 
 |-  ( 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 ) )