Metamath Proof Explorer

Theorem mdet0pr

Description: The determinant function for 0-dimensional matrices on a given ring is the function mapping the empty set to the unit of that ring. (Contributed by AV, 28-Feb-2019)

Ref Expression
Assertion mdet0pr ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ∅ maDet 𝑅 ) = ( ∅ maDet 𝑅 )
2 eqid ⊢ ( ∅ Mat 𝑅 ) = ( ∅ Mat 𝑅 )
3 eqid ⊢ ( Base ‘ ( ∅ Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
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 mdetfval ⊢ ( ∅ maDet 𝑅 ) = ( 𝑚 ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
10 9 a1i ⊢ ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) = ( 𝑚 ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
11 mat0dimbas0 ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
12 11 mpteq1d ⊢ ( 𝑅 ∈ Ring → ( 𝑚 ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ { ∅ } ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
13 0ex ⊢ ∅ ∈ V
14 13 a1i ⊢ ( 𝑅 ∈ Ring → ∅ ∈ V )
15 ovex ⊢ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) ∈ V
16 oveq ⊢ ( 𝑚 = ∅ → ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) = ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) )
17 16 mpteq2dv ⊢ ( 𝑚 = ∅ → ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) )
18 17 oveq2d ⊢ ( 𝑚 = ∅ → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) )
19 18 oveq2d ⊢ ( 𝑚 = ∅ → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) )
20 19 mpteq2dv ⊢ ( 𝑚 = ∅ → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) )
21 20 oveq2d ⊢ ( 𝑚 = ∅ → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) )
22 21 fmptsng ⊢ ( ( ∅ ∈ V ∧ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) ∈ V ) → { ⟨ ∅ , ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) ⟩ } = ( 𝑚 ∈ { ∅ } ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
23 14 15 22 sylancl ⊢ ( 𝑅 ∈ Ring → { ⟨ ∅ , ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) ⟩ } = ( 𝑚 ∈ { ∅ } ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
24 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) = ∅
25 24 a1i ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) = ∅ )
26 25 oveq2d ⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ∅ ) )
27 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
28 27 gsum0 ⊢ ( ( mulGrp ‘ 𝑅 ) Σg ∅ ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
29 26 28 eqtrdi ⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
30 29 oveq2d ⊢ ( 𝑅 ∈ Ring → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) )
31 30 mpteq2dv ⊢ ( 𝑅 ∈ Ring → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) ) )
32 31 oveq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) ) ) )
33 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
34 8 33 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
35 34 eqcomi ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 )
36 35 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
37 36 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
38 0fin ⊢ ∅ ∈ Fin
39 4 6 5 zrhcopsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ ∅ ∈ Fin ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) )
40 38 39 mp3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) )
41 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42 41 7 33 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) )
43 40 42 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) )
44 37 43 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) )
45 44 mpteq2dva ⊢ ( 𝑅 ∈ Ring → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ) )
46 45 oveq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ) ) )
47 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → 𝑅 ∈ Ring )
48 38 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ∅ ∈ Fin )
49 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) )
50 elsni ⊢ ( 𝑝 ∈ { ∅ } → 𝑝 = ∅ )
51 fveq2 ⊢ ( 𝑝 = ∅ → ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = ( ( pmSgn ‘ ∅ ) ‘ ∅ ) )
52 psgn0fv0 ⊢ ( ( pmSgn ‘ ∅ ) ‘ ∅ ) = 1
53 51 52 eqtrdi ⊢ ( 𝑝 = ∅ → ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = 1 )
54 50 53 syl ⊢ ( 𝑝 ∈ { ∅ } → ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = 1 )
55 symgbas0 ⊢ ( Base ‘ ( SymGrp ‘ ∅ ) ) = { ∅ }
56 54 55 eleq2s ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) → ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = 1 )
57 56 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = 1 )
58 eqid ⊢ ( SymGrp ‘ ∅ ) = ( SymGrp ‘ ∅ )
59 58 4 6 psgnevpmb ⊢ ( ∅ ∈ Fin → ( 𝑝 ∈ ( pmEven ‘ ∅ ) ↔ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ∧ ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = 1 ) ) )
60 48 59 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( 𝑝 ∈ ( pmEven ‘ ∅ ) ↔ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ∧ ( ( pmSgn ‘ ∅ ) ‘ 𝑝 ) = 1 ) ) )
61 49 57 60 mpbir2and ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → 𝑝 ∈ ( pmEven ‘ ∅ ) )
62 5 6 33 zrhpsgnevpm ⊢ ( ( 𝑅 ∈ Ring ∧ ∅ ∈ Fin ∧ 𝑝 ∈ ( pmEven ‘ ∅ ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) = ( 1r ‘ 𝑅 ) )
63 47 48 61 62 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) = ( 1r ‘ 𝑅 ) )
64 63 mpteq2dva ⊢ ( 𝑅 ∈ Ring → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( 1r ‘ 𝑅 ) ) )
65 64 oveq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( 1r ‘ 𝑅 ) ) ) )
66 55 a1i ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( SymGrp ‘ ∅ ) ) = { ∅ } )
67 66 mpteq1d ⊢ ( 𝑅 ∈ Ring → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( 1r ‘ 𝑅 ) ) = ( 𝑝 ∈ { ∅ } ↦ ( 1r ‘ 𝑅 ) ) )
68 67 oveq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( 1r ‘ 𝑅 ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ { ∅ } ↦ ( 1r ‘ 𝑅 ) ) ) )
69 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
70 41 33 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
71 eqidd ⊢ ( 𝑝 = ∅ → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
72 41 71 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ ∅ ∈ V ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑝 ∈ { ∅ } ↦ ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
73 69 14 70 72 syl3anc ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ { ∅ } ↦ ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
74 65 68 73 3eqtrd ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ) ) = ( 1r ‘ 𝑅 ) )
75 32 46 74 3eqtrd ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) = ( 1r ‘ 𝑅 ) )
76 75 opeq2d ⊢ ( 𝑅 ∈ Ring → ⟨ ∅ , ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) ⟩ = ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ )
77 76 sneqd ⊢ ( 𝑅 ∈ Ring → { ⟨ ∅ , ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) ∅ 𝑥 ) ) ) ) ) ) ⟩ } = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } )
78 23 77 eqtr3d ⊢ ( 𝑅 ∈ Ring → ( 𝑚 ∈ { ∅ } ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ∅ ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ∅ ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } )
79 10 12 78 3eqtrd ⊢ ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } )