Metamath Proof Explorer

Theorem m2detleib

Description: Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018) (Revised by AV, 26-Dec-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses m2detleib.n ⊢ 𝑁 = { 1 , 2 }
m2detleib.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
m2detleib.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
m2detleib.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
m2detleib.m ⊢ − = ( -g ‘ 𝑅 )
m2detleib.t ⊢ · = ( .r ‘ 𝑅 )
Assertion m2detleib ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) − ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 m2detleib.n ⊢ 𝑁 = { 1 , 2 }
2 m2detleib.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
3 m2detleib.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2detleib.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
5 m2detleib.m ⊢ − = ( -g ‘ 𝑅 )
6 m2detleib.t ⊢ · = ( .r ‘ 𝑅 )
7 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
8 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
9 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
10 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11 2 3 4 7 8 9 6 10 mdetleib1 ⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) )
12 11 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
15 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
16 15 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
17 prfi ⊢ { 1 , 2 } ∈ Fin
18 1 17 eqeltri ⊢ 𝑁 ∈ Fin
19 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
20 19 7 symgbasfi ⊢ ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
21 18 20 ax-mp ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin
22 21 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
23 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
24 23 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
25 7 9 8 zrhpsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
26 18 25 mp3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
27 26 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
28 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
29 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
30 29 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑀 ∈ 𝐵 )
31 1 7 3 4 10 m2detleiblem2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
32 24 28 30 31 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
33 13 6 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
34 24 27 32 33 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
35 opex ⊢ ⟨ 1 , 1 ⟩ ∈ V
36 opex ⊢ ⟨ 2 , 2 ⟩ ∈ V
37 35 36 pm3.2i ⊢ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V )
38 opex ⊢ ⟨ 1 , 2 ⟩ ∈ V
39 opex ⊢ ⟨ 2 , 1 ⟩ ∈ V
40 38 39 pm3.2i ⊢ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V )
41 37 40 pm3.2i ⊢ ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) )
42 1ne2 ⊢ 1 ≠ 2
43 42 olci ⊢ ( 1 ≠ 1 ∨ 1 ≠ 2 )
44 1ex ⊢ 1 ∈ V
45 44 44 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ↔ ( 1 ≠ 1 ∨ 1 ≠ 2 ) )
46 43 45 mpbir ⊢ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩
47 42 orci ⊢ ( 1 ≠ 2 ∨ 1 ≠ 1 )
48 44 44 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ↔ ( 1 ≠ 2 ∨ 1 ≠ 1 ) )
49 47 48 mpbir ⊢ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩
50 46 49 pm3.2i ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ )
51 50 orci ⊢ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) )
52 41 51 pm3.2i ⊢ ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) ∧ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) )
53 52 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) ∧ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) ) )
54 prneimg ⊢ ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) → ( ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ≠ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
55 54 imp ⊢ ( ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) ∧ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ≠ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
56 disjsn2 ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ≠ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∩ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ) = ∅ )
57 53 55 56 3syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∩ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ) = ∅ )
58 2nn ⊢ 2 ∈ ℕ
59 19 7 1 symg2bas ⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
60 44 58 59 mp2an ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
61 df-pr ⊢ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } = ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∪ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
62 60 61 eqtri ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∪ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
63 62 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∪ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ) )
64 13 14 16 22 34 57 63 gsummptfidmsplit ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ) )
65 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
66 65 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Mnd )
67 prex ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V
68 67 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V )
69 67 prid1 ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
70 69 60 eleqtrri ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
71 70 a1i ⊢ ( 𝑀 ∈ 𝐵 → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
72 7 9 8 zrhpsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
73 18 72 mp3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
74 71 73 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
75 1 7 3 4 10 m2detleiblem2 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
76 70 75 mp3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
77 13 6 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
78 23 74 76 77 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
79 2fveq3 ⊢ ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) )
80 fveq1 ⊢ ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑘 ‘ 𝑛 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) )
81 80 oveq1d ⊢ ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) = ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) )
82 81 mpteq2dv ⊢ ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) )
83 82 oveq2d ⊢ ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) )
84 79 83 oveq12d ⊢ ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
85 13 84 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V ∧ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
86 66 68 78 85 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
87 prex ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
88 87 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V )
89 87 prid2 ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
90 89 60 eleqtrri ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
91 90 a1i ⊢ ( 𝑀 ∈ 𝐵 → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
92 7 9 8 zrhpsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
93 18 92 mp3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
94 91 93 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
95 1 7 3 4 10 m2detleiblem2 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
96 90 95 mp3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
97 13 6 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
98 23 94 96 97 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
99 2fveq3 ⊢ ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) )
100 fveq1 ⊢ ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑘 ‘ 𝑛 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) )
101 100 oveq1d ⊢ ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) = ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) )
102 101 mpteq2dv ⊢ ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) )
103 102 oveq2d ⊢ ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) )
104 99 103 oveq12d ⊢ ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
105 13 104 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V ∧ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
106 66 88 98 105 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
107 86 106 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) )
108 eqidd ⊢ ( 𝑀 ∈ 𝐵 → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
109 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
110 1 7 8 9 109 m2detleiblem5 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) = ( 1r ‘ 𝑅 ) )
111 108 110 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) = ( 1r ‘ 𝑅 ) )
112 eqidd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
113 10 6 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
114 1 7 3 4 10 113 m2detleiblem3 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
115 23 112 29 114 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
116 111 115 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( 1r ‘ 𝑅 ) · ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ) )
117 44 prid1 ⊢ 1 ∈ { 1 , 2 }
118 117 1 eleqtrri ⊢ 1 ∈ 𝑁
119 118 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ 𝑁 )
120 4 eleq2i ⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
121 120 bilani ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
122 3 13 matecl ⊢ ( ( 1 ∈ 𝑁 ∧ 1 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 1 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
123 119 119 121 122 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 1 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
124 prid2g ⊢ ( 2 ∈ ℕ → 2 ∈ { 1 , 2 } )
125 58 124 ax-mp ⊢ 2 ∈ { 1 , 2 }
126 125 1 eleqtrri ⊢ 2 ∈ 𝑁
127 126 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 2 ∈ 𝑁 )
128 3 13 matecl ⊢ ( ( 2 ∈ 𝑁 ∧ 2 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 2 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
129 127 127 121 128 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 2 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
130 13 6 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 2 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
131 23 123 129 130 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
132 13 6 109 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
133 131 132 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
134 116 133 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
135 eqidd ⊢ ( 𝑀 ∈ 𝐵 → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
136 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
137 1 7 8 9 109 136 m2detleiblem6 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
138 135 137 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
139 eqidd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
140 1 7 3 4 10 113 m2detleiblem4 ⊢ ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )
141 23 139 29 140 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )
142 138 141 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
143 134 142 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) ) )
144 3 13 matecl ⊢ ( ( 2 ∈ 𝑁 ∧ 1 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 2 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
145 127 119 121 144 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 2 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
146 3 13 matecl ⊢ ( ( 1 ∈ 𝑁 ∧ 2 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 1 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
147 119 127 121 146 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 1 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
148 13 6 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 2 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
149 23 145 147 148 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
150 1 7 8 9 109 136 6 5 m2detleiblem7 ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) − ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
151 23 131 149 150 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) − ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
152 107 143 151 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑘 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) − ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
153 12 64 152 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) − ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )