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 0fin ∅ ∈ 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 ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼𝑉 ) ∧ 𝑀𝐵 ) → ( 𝐷𝑀 ) = ( 𝐼 𝑀 𝐼 ) )