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 ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetdiag.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetdiag.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion m1detdiag ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐼 𝑀 𝐼 ) )

Proof

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